Proof of Theorem dochsat
Step | Hyp | Ref
| Expression |
1 | | dochsat.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | dochsat.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | dochsat.k |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
4 | 1, 2, 3 | dvhlmod 38861 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
5 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑈 ∈ LMod) |
6 | | dochsat.q |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ 𝑆) |
7 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑄 ∈ 𝑆) |
8 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝑈) = (0g‘𝑈) |
9 | | dochsat.s |
. . . . . . . 8
⊢ 𝑆 = (LSubSp‘𝑈) |
10 | 8, 9 | lss0ss 19985 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑄 ∈ 𝑆) → {(0g‘𝑈)} ⊆ 𝑄) |
11 | 5, 7, 10 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) →
{(0g‘𝑈)}
⊆ 𝑄) |
12 | | dochsat.a |
. . . . . . . . 9
⊢ 𝐴 = (LSAtoms‘𝑈) |
13 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) |
14 | 8, 12, 5, 13 | lsatn0 36750 |
. . . . . . . 8
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → ( ⊥ ‘( ⊥
‘𝑄)) ≠
{(0g‘𝑈)}) |
15 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) ∧ 𝑄 = {(0g‘𝑈)}) → 𝑄 = {(0g‘𝑈)}) |
16 | 15 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) ∧ 𝑄 = {(0g‘𝑈)}) → ( ⊥ ‘𝑄) = ( ⊥
‘{(0g‘𝑈)})) |
17 | 16 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) ∧ 𝑄 = {(0g‘𝑈)}) → ( ⊥ ‘( ⊥
‘𝑄)) = ( ⊥
‘( ⊥
‘{(0g‘𝑈)}))) |
18 | | dochsat.o |
. . . . . . . . . . . . . 14
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
19 | 1, 2, 18, 8, 3 | dochoc0 39111 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘{(0g‘𝑈)})) = {(0g‘𝑈)}) |
20 | 19 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → ( ⊥ ‘( ⊥
‘{(0g‘𝑈)})) = {(0g‘𝑈)}) |
21 | 20 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) ∧ 𝑄 = {(0g‘𝑈)}) → ( ⊥ ‘( ⊥
‘{(0g‘𝑈)})) = {(0g‘𝑈)}) |
22 | 17, 21 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) ∧ 𝑄 = {(0g‘𝑈)}) → ( ⊥ ‘( ⊥
‘𝑄)) =
{(0g‘𝑈)}) |
23 | 22 | ex 416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → (𝑄 = {(0g‘𝑈)} → ( ⊥ ‘( ⊥
‘𝑄)) =
{(0g‘𝑈)})) |
24 | 23 | necon3d 2961 |
. . . . . . . 8
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → (( ⊥ ‘( ⊥
‘𝑄)) ≠
{(0g‘𝑈)}
→ 𝑄 ≠
{(0g‘𝑈)})) |
25 | 14, 24 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑄 ≠ {(0g‘𝑈)}) |
26 | 25 | necomd 2996 |
. . . . . 6
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) →
{(0g‘𝑈)}
≠ 𝑄) |
27 | | df-pss 3885 |
. . . . . 6
⊢
({(0g‘𝑈)} ⊊ 𝑄 ↔ ({(0g‘𝑈)} ⊆ 𝑄 ∧ {(0g‘𝑈)} ≠ 𝑄)) |
28 | 11, 26, 27 | sylanbrc 586 |
. . . . 5
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) →
{(0g‘𝑈)}
⊊ 𝑄) |
29 | 3 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
30 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑈) =
(Base‘𝑈) |
31 | 30, 9 | lssss 19973 |
. . . . . . . . 9
⊢ (𝑄 ∈ 𝑆 → 𝑄 ⊆ (Base‘𝑈)) |
32 | 6, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ⊆ (Base‘𝑈)) |
33 | 32 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑄 ⊆ (Base‘𝑈)) |
34 | 1, 2, 30, 18 | dochocss 39117 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ⊆ (Base‘𝑈)) → 𝑄 ⊆ ( ⊥ ‘( ⊥
‘𝑄))) |
35 | 29, 33, 34 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑄 ⊆ ( ⊥ ‘( ⊥
‘𝑄))) |
36 | 9, 12, 5, 13 | lsatlssel 36748 |
. . . . . . . 8
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝑆) |
37 | 9 | lsssubg 19994 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘( ⊥ ‘𝑄)) ∈ 𝑆) → ( ⊥ ‘( ⊥
‘𝑄)) ∈
(SubGrp‘𝑈)) |
38 | 5, 36, 37 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → ( ⊥ ‘( ⊥
‘𝑄)) ∈
(SubGrp‘𝑈)) |
39 | | eqid 2737 |
. . . . . . . 8
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
40 | 8, 39 | lsm02 19062 |
. . . . . . 7
⊢ (( ⊥
‘( ⊥ ‘𝑄)) ∈ (SubGrp‘𝑈) →
({(0g‘𝑈)}
(LSSum‘𝑈)( ⊥
‘( ⊥ ‘𝑄))) = ( ⊥ ‘( ⊥
‘𝑄))) |
41 | 38, 40 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) →
({(0g‘𝑈)}
(LSSum‘𝑈)( ⊥
‘( ⊥ ‘𝑄))) = ( ⊥ ‘( ⊥
‘𝑄))) |
42 | 35, 41 | sseqtrrd 3942 |
. . . . 5
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑄 ⊆ ({(0g‘𝑈)} (LSSum‘𝑈)( ⊥ ‘( ⊥
‘𝑄)))) |
43 | 1, 2, 3 | dvhlvec 38860 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ LVec) |
44 | 43 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑈 ∈ LVec) |
45 | 8, 9 | lsssn0 19984 |
. . . . . . 7
⊢ (𝑈 ∈ LMod →
{(0g‘𝑈)}
∈ 𝑆) |
46 | 5, 45 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) →
{(0g‘𝑈)}
∈ 𝑆) |
47 | 9, 39, 12, 44, 46, 7, 13 | lsmsatcv 36761 |
. . . . 5
⊢ (((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) ∧
{(0g‘𝑈)}
⊊ 𝑄 ∧ 𝑄 ⊆
({(0g‘𝑈)}
(LSSum‘𝑈)( ⊥
‘( ⊥ ‘𝑄)))) → 𝑄 = ({(0g‘𝑈)} (LSSum‘𝑈)( ⊥ ‘( ⊥
‘𝑄)))) |
48 | 28, 42, 47 | mpd3an23 1465 |
. . . 4
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑄 = ({(0g‘𝑈)} (LSSum‘𝑈)( ⊥ ‘( ⊥
‘𝑄)))) |
49 | 48, 41 | eqtr2d 2778 |
. . 3
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄) |
50 | 49, 13 | eqeltrrd 2839 |
. 2
⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) → 𝑄 ∈ 𝐴) |
51 | 3 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
52 | | eqid 2737 |
. . . . . 6
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
53 | 1, 2, 52, 12 | dih1dimat 39081 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
54 | 3, 53 | sylan 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
55 | 1, 52, 18 | dochoc 39118 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄) |
56 | 51, 54, 55 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄) |
57 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ 𝐴) |
58 | 56, 57 | eqeltrd 2838 |
. 2
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → ( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴) |
59 | 50, 58 | impbida 801 |
1
⊢ (𝜑 → (( ⊥ ‘( ⊥
‘𝑄)) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴)) |