Proof of Theorem dochnoncon
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑈) =
(Base‘𝑈) |
2 | | dochnoncon.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑈) |
3 | 1, 2 | lssss 18758 |
. . . . 5
⊢ (𝑋 ∈ 𝑆 → 𝑋 ⊆ (Base‘𝑈)) |
4 | | dochnoncon.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | dochnoncon.u |
. . . . . 6
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
6 | | dochnoncon.o |
. . . . . 6
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
7 | 4, 5, 1, 6 | dochocss 35673 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘𝑈)) → 𝑋 ⊆ ( ⊥ ‘( ⊥
‘𝑋))) |
8 | 3, 7 | sylan2 490 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝑋 ⊆ ( ⊥ ‘( ⊥
‘𝑋))) |
9 | | ssrin 3800 |
. . . 4
⊢ (𝑋 ⊆ ( ⊥ ‘( ⊥
‘𝑋)) → (𝑋 ∩ ( ⊥ ‘𝑋)) ⊆ (( ⊥ ‘( ⊥
‘𝑋)) ∩ ( ⊥
‘𝑋))) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ⊆ (( ⊥ ‘( ⊥
‘𝑋)) ∩ ( ⊥
‘𝑋))) |
11 | | simpl 472 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
12 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) |
13 | | eqid 2610 |
. . . . . . . . . 10
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
14 | | eqid 2610 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
15 | 12, 4, 13, 5, 14 | dihf11 35574 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈)) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈)) |
17 | | f1f1orn 6061 |
. . . . . . . 8
⊢
(((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊)) |
19 | 4, 13, 5, 1, 6 | dochcl 35660 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
20 | 3, 19 | sylan2 490 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
21 | 4, 5, 13, 14 | dihrnlss 35584 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘𝑋) ∈ (LSubSp‘𝑈)) |
22 | 20, 21 | syldan 486 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ∈ (LSubSp‘𝑈)) |
23 | 1, 14 | lssss 18758 |
. . . . . . . . 9
⊢ (( ⊥
‘𝑋) ∈
(LSubSp‘𝑈) → (
⊥
‘𝑋) ⊆
(Base‘𝑈)) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ⊆ (Base‘𝑈)) |
25 | 4, 13, 5, 1, 6 | dochcl 35660 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ⊆ (Base‘𝑈)) → ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
26 | 24, 25 | syldan 486 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
27 | | f1ocnvdm 6440 |
. . . . . . 7
⊢
((((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) |
28 | 18, 26, 27 | syl2anc 691 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) |
29 | | hlop 33667 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
30 | 29 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝐾 ∈ OP) |
31 | | eqid 2610 |
. . . . . . . 8
⊢
(oc‘𝐾) =
(oc‘𝐾) |
32 | 12, 31 | opoccl 33499 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) →
((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∈
(Base‘𝐾)) |
33 | 30, 28, 32 | syl2anc 691 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∈
(Base‘𝐾)) |
34 | | eqid 2610 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
35 | 12, 34, 4, 13 | dihmeet 35650 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾) ∧
((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∈
(Base‘𝐾)) →
(((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))))) |
36 | 11, 28, 33, 35 | syl3anc 1318 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))))) |
37 | | eqid 2610 |
. . . . . . . 8
⊢
(0.‘𝐾) =
(0.‘𝐾) |
38 | 12, 31, 34, 37 | opnoncon 33513 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) →
((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))) =
(0.‘𝐾)) |
39 | 30, 28, 38 | syl2anc 691 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))) =
(0.‘𝐾)) |
40 | 39 | fveq2d 6107 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
(((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾))) |
41 | 36, 40 | eqtr3d 2646 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
(((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾))) |
42 | 4, 13 | dihcnvid2 35580 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) = ( ⊥
‘( ⊥ ‘𝑋))) |
43 | 26, 42 | syldan 486 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) = ( ⊥
‘( ⊥ ‘𝑋))) |
44 | 31, 4, 13, 6 | dochvalr 35664 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) |
45 | 26, 44 | syldan 486 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) |
46 | 4, 13, 6 | dochoc 35674 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = ( ⊥ ‘𝑋)) |
47 | 20, 46 | syldan 486 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = ( ⊥ ‘𝑋)) |
48 | 45, 47 | eqtr3d 2646 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))) = ( ⊥
‘𝑋)) |
49 | 43, 48 | ineq12d 3777 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) = (( ⊥
‘( ⊥ ‘𝑋)) ∩ ( ⊥ ‘𝑋))) |
50 | | dochnoncon.z |
. . . . . 6
⊢ 0 =
(0g‘𝑈) |
51 | 37, 4, 13, 5, 50 | dih0 35587 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾)) = { 0 }) |
52 | 51 | adantr 480 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾)) = { 0 }) |
53 | 41, 49, 52 | 3eqtr3d 2652 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (( ⊥ ‘( ⊥
‘𝑋)) ∩ ( ⊥
‘𝑋)) = { 0
}) |
54 | 10, 53 | sseqtrd 3604 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ⊆ { 0 }) |
55 | 4, 5, 11 | dvhlmod 35417 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝑈 ∈ LMod) |
56 | | simpr 476 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆) |
57 | 4, 5, 13, 2 | dihrnlss 35584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘𝑋) ∈ 𝑆) |
58 | 20, 57 | syldan 486 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ∈ 𝑆) |
59 | 2 | lssincl 18786 |
. . . 4
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ ( ⊥ ‘𝑋) ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ∈ 𝑆) |
60 | 55, 56, 58, 59 | syl3anc 1318 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ∈ 𝑆) |
61 | 50, 2 | lss0ss 18770 |
. . 3
⊢ ((𝑈 ∈ LMod ∧ (𝑋 ∩ ( ⊥ ‘𝑋)) ∈ 𝑆) → { 0 } ⊆ (𝑋 ∩ ( ⊥ ‘𝑋))) |
62 | 55, 60, 61 | syl2anc 691 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → { 0 } ⊆ (𝑋 ∩ ( ⊥ ‘𝑋))) |
63 | 54, 62 | eqssd 3585 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) = { 0 }) |