Proof of Theorem dochnoncon
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑈) =
(Base‘𝑈) |
2 | | dochnoncon.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑈) |
3 | 1, 2 | lssss 20198 |
. . . . 5
⊢ (𝑋 ∈ 𝑆 → 𝑋 ⊆ (Base‘𝑈)) |
4 | | dochnoncon.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | dochnoncon.u |
. . . . . 6
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
6 | | dochnoncon.o |
. . . . . 6
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
7 | 4, 5, 1, 6 | dochocss 39380 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘𝑈)) → 𝑋 ⊆ ( ⊥ ‘( ⊥
‘𝑋))) |
8 | 3, 7 | sylan2 593 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝑋 ⊆ ( ⊥ ‘( ⊥
‘𝑋))) |
9 | 8 | ssrind 4169 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ⊆ (( ⊥ ‘( ⊥
‘𝑋)) ∩ ( ⊥
‘𝑋))) |
10 | | simpl 483 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
11 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) |
12 | | eqid 2738 |
. . . . . . . . . 10
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
13 | | eqid 2738 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
14 | 11, 4, 12, 5, 13 | dihf11 39281 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈)) |
15 | 14 | adantr 481 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈)) |
16 | | f1f1orn 6727 |
. . . . . . . 8
⊢
(((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1→(LSubSp‘𝑈) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊)) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊)) |
18 | 4, 12, 5, 1, 6 | dochcl 39367 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
19 | 3, 18 | sylan2 593 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
20 | 4, 5, 12, 13 | dihrnlss 39291 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘𝑋) ∈ (LSubSp‘𝑈)) |
21 | 19, 20 | syldan 591 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ∈ (LSubSp‘𝑈)) |
22 | 1, 13 | lssss 20198 |
. . . . . . . . 9
⊢ (( ⊥
‘𝑋) ∈
(LSubSp‘𝑈) → (
⊥
‘𝑋) ⊆
(Base‘𝑈)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ⊆ (Base‘𝑈)) |
24 | 4, 12, 5, 1, 6 | dochcl 39367 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ⊆ (Base‘𝑈)) → ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
25 | 23, 24 | syldan 591 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
26 | | f1ocnvdm 7157 |
. . . . . . 7
⊢
((((DIsoH‘𝐾)‘𝑊):(Base‘𝐾)–1-1-onto→ran
((DIsoH‘𝐾)‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) |
27 | 17, 25, 26 | syl2anc 584 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) |
28 | | hlop 37376 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
29 | 28 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝐾 ∈ OP) |
30 | | eqid 2738 |
. . . . . . . 8
⊢
(oc‘𝐾) =
(oc‘𝐾) |
31 | 11, 30 | opoccl 37208 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) →
((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∈
(Base‘𝐾)) |
32 | 29, 27, 31 | syl2anc 584 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∈
(Base‘𝐾)) |
33 | | eqid 2738 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
34 | 11, 33, 4, 12 | dihmeet 39357 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾) ∧
((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∈
(Base‘𝐾)) →
(((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))))) |
35 | 10, 27, 32, 34 | syl3anc 1370 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))))) |
36 | | eqid 2738 |
. . . . . . . 8
⊢
(0.‘𝐾) =
(0.‘𝐾) |
37 | 11, 30, 33, 36 | opnoncon 37222 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ (◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))) ∈
(Base‘𝐾)) →
((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))) =
(0.‘𝐾)) |
38 | 29, 27, 37 | syl2anc 584 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))) =
(0.‘𝐾)) |
39 | 38 | fveq2d 6778 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))(meet‘𝐾)((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
(((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾))) |
40 | 35, 39 | eqtr3d 2780 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) =
(((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾))) |
41 | 4, 12 | dihcnvid2 39287 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) = ( ⊥
‘( ⊥ ‘𝑋))) |
42 | 25, 41 | syldan 591 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) = ( ⊥
‘( ⊥ ‘𝑋))) |
43 | 30, 4, 12, 6 | dochvalr 39371 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘( ⊥
‘𝑋)) ∈ ran
((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) |
44 | 25, 43 | syldan 591 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) |
45 | 4, 12, 6 | dochoc 39381 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = ( ⊥ ‘𝑋)) |
46 | 19, 45 | syldan 591 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘( ⊥
‘( ⊥ ‘𝑋))) = ( ⊥ ‘𝑋)) |
47 | 44, 46 | eqtr3d 2780 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋))))) = ( ⊥
‘𝑋)) |
48 | 42, 47 | ineq12d 4147 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ((((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))) ∩
(((DIsoH‘𝐾)‘𝑊)‘((oc‘𝐾)‘(◡((DIsoH‘𝐾)‘𝑊)‘( ⊥ ‘( ⊥
‘𝑋)))))) = (( ⊥
‘( ⊥ ‘𝑋)) ∩ ( ⊥ ‘𝑋))) |
49 | | dochnoncon.z |
. . . . . 6
⊢ 0 =
(0g‘𝑈) |
50 | 36, 4, 12, 5, 49 | dih0 39294 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾)) = { 0 }) |
51 | 50 | adantr 481 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (((DIsoH‘𝐾)‘𝑊)‘(0.‘𝐾)) = { 0 }) |
52 | 40, 48, 51 | 3eqtr3d 2786 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (( ⊥ ‘( ⊥
‘𝑋)) ∩ ( ⊥
‘𝑋)) = { 0
}) |
53 | 9, 52 | sseqtrd 3961 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ⊆ { 0 }) |
54 | 4, 5, 10 | dvhlmod 39124 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝑈 ∈ LMod) |
55 | | simpr 485 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆) |
56 | 4, 5, 12, 2 | dihrnlss 39291 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘𝑋) ∈ 𝑆) |
57 | 19, 56 | syldan 591 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → ( ⊥ ‘𝑋) ∈ 𝑆) |
58 | 2 | lssincl 20227 |
. . . 4
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ ( ⊥ ‘𝑋) ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ∈ 𝑆) |
59 | 54, 55, 57, 58 | syl3anc 1370 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) ∈ 𝑆) |
60 | 49, 2 | lss0ss 20210 |
. . 3
⊢ ((𝑈 ∈ LMod ∧ (𝑋 ∩ ( ⊥ ‘𝑋)) ∈ 𝑆) → { 0 } ⊆ (𝑋 ∩ ( ⊥ ‘𝑋))) |
61 | 54, 59, 60 | syl2anc 584 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → { 0 } ⊆ (𝑋 ∩ ( ⊥ ‘𝑋))) |
62 | 53, 61 | eqssd 3938 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) = { 0 }) |