Step | Hyp | Ref
| Expression |
1 | | dochsatshp.k |
. . 3
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | eqid 2759 |
. . . 4
⊢
(Base‘𝑈) =
(Base‘𝑈) |
3 | | dochsatshp.a |
. . . 4
⊢ 𝐴 = (LSAtoms‘𝑈) |
4 | | dochsatshp.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | dochsatshp.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
6 | 4, 5, 1 | dvhlmod 38671 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ LMod) |
7 | | dochsatshp.q |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
8 | 2, 3, 6, 7 | lsatssv 36559 |
. . 3
⊢ (𝜑 → 𝑄 ⊆ (Base‘𝑈)) |
9 | | eqid 2759 |
. . . 4
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
10 | | dochsatshp.o |
. . . 4
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
11 | 4, 5, 2, 9, 10 | dochlss 38915 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈)) |
12 | 1, 8, 11 | syl2anc 588 |
. 2
⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈)) |
13 | | eqid 2759 |
. . . 4
⊢
(0g‘𝑈) = (0g‘𝑈) |
14 | 13, 3, 6, 7 | lsatn0 36560 |
. . 3
⊢ (𝜑 → 𝑄 ≠ {(0g‘𝑈)}) |
15 | 4, 5, 10, 2, 13 | doch0 38919 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥
‘{(0g‘𝑈)}) = (Base‘𝑈)) |
16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → ( ⊥
‘{(0g‘𝑈)}) = (Base‘𝑈)) |
17 | 16 | eqeq2d 2770 |
. . . . 5
⊢ (𝜑 → (( ⊥ ‘𝑄) = ( ⊥
‘{(0g‘𝑈)}) ↔ ( ⊥ ‘𝑄) = (Base‘𝑈))) |
18 | | eqid 2759 |
. . . . . 6
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
19 | 4, 5, 18, 3 | dih1dimat 38891 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) → 𝑄 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
20 | 1, 7, 19 | syl2anc 588 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
21 | 4, 18, 5, 13 | dih0rn 38845 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → {(0g‘𝑈)} ∈ ran
((DIsoH‘𝐾)‘𝑊)) |
22 | 1, 21 | syl 17 |
. . . . . 6
⊢ (𝜑 →
{(0g‘𝑈)}
∈ ran ((DIsoH‘𝐾)‘𝑊)) |
23 | 4, 18, 10, 1, 20, 22 | doch11 38934 |
. . . . 5
⊢ (𝜑 → (( ⊥ ‘𝑄) = ( ⊥
‘{(0g‘𝑈)}) ↔ 𝑄 = {(0g‘𝑈)})) |
24 | 17, 23 | bitr3d 284 |
. . . 4
⊢ (𝜑 → (( ⊥ ‘𝑄) = (Base‘𝑈) ↔ 𝑄 = {(0g‘𝑈)})) |
25 | 24 | necon3bid 2993 |
. . 3
⊢ (𝜑 → (( ⊥ ‘𝑄) ≠ (Base‘𝑈) ↔ 𝑄 ≠ {(0g‘𝑈)})) |
26 | 14, 25 | mpbird 260 |
. 2
⊢ (𝜑 → ( ⊥ ‘𝑄) ≠ (Base‘𝑈)) |
27 | | eqid 2759 |
. . . . . 6
⊢
(LSpan‘𝑈) =
(LSpan‘𝑈) |
28 | 2, 27, 13, 3 | islsat 36552 |
. . . . 5
⊢ (𝑈 ∈ LMod → (𝑄 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣}))) |
29 | 6, 28 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣}))) |
30 | 7, 29 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣})) |
31 | | eldifi 4028 |
. . . . . . 7
⊢ (𝑣 ∈ ((Base‘𝑈) ∖
{(0g‘𝑈)})
→ 𝑣 ∈
(Base‘𝑈)) |
32 | 31 | adantr 485 |
. . . . . 6
⊢ ((𝑣 ∈ ((Base‘𝑈) ∖
{(0g‘𝑈)})
∧ 𝑄 =
((LSpan‘𝑈)‘{𝑣})) → 𝑣 ∈ (Base‘𝑈)) |
33 | 32 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → 𝑣 ∈ (Base‘𝑈))) |
34 | 9, 27 | lspid 19807 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘𝑄) ∈
(LSubSp‘𝑈)) →
((LSpan‘𝑈)‘(
⊥
‘𝑄)) = ( ⊥
‘𝑄)) |
35 | 6, 12, 34 | syl2anc 588 |
. . . . . . . . . . 11
⊢ (𝜑 → ((LSpan‘𝑈)‘( ⊥ ‘𝑄)) = ( ⊥ ‘𝑄)) |
36 | 35 | uneq1d 4063 |
. . . . . . . . . 10
⊢ (𝜑 → (((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣})) = (( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣}))) |
37 | 36 | fveq2d 6655 |
. . . . . . . . 9
⊢ (𝜑 → ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣}))) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣})))) |
38 | 37 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣}))) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣})))) |
39 | 6 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → 𝑈 ∈ LMod) |
40 | 2, 9 | lssss 19761 |
. . . . . . . . . . 11
⊢ (( ⊥
‘𝑄) ∈
(LSubSp‘𝑈) → (
⊥
‘𝑄) ⊆
(Base‘𝑈)) |
41 | 12, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ( ⊥ ‘𝑄) ⊆ (Base‘𝑈)) |
42 | 41 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ( ⊥ ‘𝑄) ⊆ (Base‘𝑈)) |
43 | 31 | snssd 4692 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ((Base‘𝑈) ∖
{(0g‘𝑈)})
→ {𝑣} ⊆
(Base‘𝑈)) |
44 | 43 | adantr 485 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ((Base‘𝑈) ∖
{(0g‘𝑈)})
∧ 𝑄 =
((LSpan‘𝑈)‘{𝑣})) → {𝑣} ⊆ (Base‘𝑈)) |
45 | 44 | adantl 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → {𝑣} ⊆ (Base‘𝑈)) |
46 | 2, 27 | lspun 19812 |
. . . . . . . . 9
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘𝑄) ⊆
(Base‘𝑈) ∧ {𝑣} ⊆ (Base‘𝑈)) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣})))) |
47 | 39, 42, 45, 46 | syl3anc 1369 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = ((LSpan‘𝑈)‘(((LSpan‘𝑈)‘( ⊥ ‘𝑄)) ∪ ((LSpan‘𝑈)‘{𝑣})))) |
48 | | uneq2 4058 |
. . . . . . . . . . 11
⊢ (𝑄 = ((LSpan‘𝑈)‘{𝑣}) → (( ⊥ ‘𝑄) ∪ 𝑄) = (( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣}))) |
49 | 48 | fveq2d 6655 |
. . . . . . . . . 10
⊢ (𝑄 = ((LSpan‘𝑈)‘{𝑣}) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣})))) |
50 | 49 | adantl 486 |
. . . . . . . . 9
⊢ ((𝑣 ∈ ((Base‘𝑈) ∖
{(0g‘𝑈)})
∧ 𝑄 =
((LSpan‘𝑈)‘{𝑣})) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣})))) |
51 | 50 | adantl 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ ((LSpan‘𝑈)‘{𝑣})))) |
52 | 38, 47, 51 | 3eqtr4d 2804 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄))) |
53 | | eqid 2759 |
. . . . . . . . . . 11
⊢
((joinH‘𝐾)‘𝑊) = ((joinH‘𝐾)‘𝑊) |
54 | | eqid 2759 |
. . . . . . . . . . 11
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
55 | 4, 18, 5, 2, 10 | dochcl 38914 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ⊆ (Base‘𝑈)) → ( ⊥ ‘𝑄) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
56 | 1, 8, 55 | syl2anc 588 |
. . . . . . . . . . 11
⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
57 | 4, 18, 53, 5, 54, 3, 1, 56, 7 | dihjat2 38992 |
. . . . . . . . . 10
⊢ (𝜑 → (( ⊥ ‘𝑄)((joinH‘𝐾)‘𝑊)𝑄) = (( ⊥ ‘𝑄)(LSSum‘𝑈)𝑄)) |
58 | 4, 5, 2, 53, 1, 41, 8 | djhcom 38966 |
. . . . . . . . . 10
⊢ (𝜑 → (( ⊥ ‘𝑄)((joinH‘𝐾)‘𝑊)𝑄) = (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄))) |
59 | 9, 3, 6, 7 | lsatlssel 36558 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ (LSubSp‘𝑈)) |
60 | 9, 27, 54 | lsmsp 19911 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ LMod ∧ ( ⊥
‘𝑄) ∈
(LSubSp‘𝑈) ∧
𝑄 ∈
(LSubSp‘𝑈)) → ((
⊥
‘𝑄)(LSSum‘𝑈)𝑄) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄))) |
61 | 6, 12, 59, 60 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (𝜑 → (( ⊥ ‘𝑄)(LSSum‘𝑈)𝑄) = ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄))) |
62 | 57, 58, 61 | 3eqtr3rd 2803 |
. . . . . . . . 9
⊢ (𝜑 → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄))) |
63 | 4, 5, 2, 10, 53 | djhexmid 38972 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ⊆ (Base‘𝑈)) → (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄)) = (Base‘𝑈)) |
64 | 1, 8, 63 | syl2anc 588 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄((joinH‘𝐾)‘𝑊)( ⊥ ‘𝑄)) = (Base‘𝑈)) |
65 | 62, 64 | eqtrd 2794 |
. . . . . . . 8
⊢ (𝜑 → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = (Base‘𝑈)) |
66 | 65 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ 𝑄)) = (Base‘𝑈)) |
67 | 52, 66 | eqtrd 2794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣}))) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈)) |
68 | 67 | ex 417 |
. . . . 5
⊢ (𝜑 → ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈))) |
69 | 33, 68 | jcad 517 |
. . . 4
⊢ (𝜑 → ((𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)}) ∧ 𝑄 = ((LSpan‘𝑈)‘{𝑣})) → (𝑣 ∈ (Base‘𝑈) ∧ ((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈)))) |
70 | 69 | reximdv2 3193 |
. . 3
⊢ (𝜑 → (∃𝑣 ∈ ((Base‘𝑈) ∖ {(0g‘𝑈)})𝑄 = ((LSpan‘𝑈)‘{𝑣}) → ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈))) |
71 | 30, 70 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈)) |
72 | 4, 5, 1 | dvhlvec 38670 |
. . 3
⊢ (𝜑 → 𝑈 ∈ LVec) |
73 | | dochsatshp.y |
. . . 4
⊢ 𝑌 = (LSHyp‘𝑈) |
74 | 2, 27, 9, 73 | islshp 36540 |
. . 3
⊢ (𝑈 ∈ LVec → (( ⊥
‘𝑄) ∈ 𝑌 ↔ (( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈) ∧ ( ⊥ ‘𝑄) ≠ (Base‘𝑈) ∧ ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈)))) |
75 | 72, 74 | syl 17 |
. 2
⊢ (𝜑 → (( ⊥ ‘𝑄) ∈ 𝑌 ↔ (( ⊥ ‘𝑄) ∈ (LSubSp‘𝑈) ∧ ( ⊥ ‘𝑄) ≠ (Base‘𝑈) ∧ ∃𝑣 ∈ (Base‘𝑈)((LSpan‘𝑈)‘(( ⊥ ‘𝑄) ∪ {𝑣})) = (Base‘𝑈)))) |
76 | 12, 26, 71, 75 | mpbir3and 1340 |
1
⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝑌) |