Proof of Theorem dia2dimlem5
Step | Hyp | Ref
| Expression |
1 | | dia2dimlem5.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | dia2dimlem5.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑇) |
3 | | dia2dimlem5.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑇) |
4 | | dia2dimlem5.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | dia2dimlem5.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
6 | | dia2dimlem5.y |
. . . . . 6
⊢ 𝑌 = ((DVecA‘𝐾)‘𝑊) |
7 | | eqid 2740 |
. . . . . 6
⊢
(+g‘𝑌) = (+g‘𝑌) |
8 | 4, 5, 6, 7 | dvavadd 39025 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → (𝐷(+g‘𝑌)𝐺) = (𝐷 ∘ 𝐺)) |
9 | 1, 2, 3, 8 | syl12anc 834 |
. . . 4
⊢ (𝜑 → (𝐷(+g‘𝑌)𝐺) = (𝐷 ∘ 𝐺)) |
10 | | dia2dimlem5.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
11 | | dia2dimlem5.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
12 | | dia2dimlem5.p |
. . . . 5
⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
13 | | dia2dimlem5.f |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) |
14 | 13 | simpld 495 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑇) |
15 | | dia2dimlem5.gv |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑃) = 𝑄) |
16 | | dia2dimlem5.dv |
. . . . 5
⊢ (𝜑 → (𝐷‘𝑄) = (𝐹‘𝑃)) |
17 | 10, 11, 4, 5, 1, 12,
14, 3, 15, 2, 16 | dia2dimlem4 39077 |
. . . 4
⊢ (𝜑 → (𝐷 ∘ 𝐺) = 𝐹) |
18 | 9, 17 | eqtr2d 2781 |
. . 3
⊢ (𝜑 → 𝐹 = (𝐷(+g‘𝑌)𝐺)) |
19 | 4, 6 | dvalvec 39036 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑌 ∈ LVec) |
20 | | lveclmod 20366 |
. . . . . . 7
⊢ (𝑌 ∈ LVec → 𝑌 ∈ LMod) |
21 | 1, 19, 20 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ LMod) |
22 | | dia2dimlem5.s |
. . . . . . 7
⊢ 𝑆 = (LSubSp‘𝑌) |
23 | 22 | lsssssubg 20218 |
. . . . . 6
⊢ (𝑌 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑌)) |
24 | 21, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑌)) |
25 | | dia2dimlem5.v |
. . . . . . . 8
⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) |
26 | 25 | simpld 495 |
. . . . . . 7
⊢ (𝜑 → 𝑉 ∈ 𝐴) |
27 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
28 | 27, 11 | atbase 37299 |
. . . . . . 7
⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾)) |
29 | 26, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾)) |
30 | 25 | simprd 496 |
. . . . . 6
⊢ (𝜑 → 𝑉 ≤ 𝑊) |
31 | | dia2dimlem5.i |
. . . . . . 7
⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
32 | 27, 10, 4, 6, 31, 22 | dialss 39056 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 ≤ 𝑊)) → (𝐼‘𝑉) ∈ 𝑆) |
33 | 1, 29, 30, 32 | syl12anc 834 |
. . . . 5
⊢ (𝜑 → (𝐼‘𝑉) ∈ 𝑆) |
34 | 24, 33 | sseldd 3927 |
. . . 4
⊢ (𝜑 → (𝐼‘𝑉) ∈ (SubGrp‘𝑌)) |
35 | | dia2dimlem5.u |
. . . . . . . 8
⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) |
36 | 35 | simpld 495 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ 𝐴) |
37 | 27, 11 | atbase 37299 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾)) |
38 | 36, 37 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾)) |
39 | 35 | simprd 496 |
. . . . . 6
⊢ (𝜑 → 𝑈 ≤ 𝑊) |
40 | 27, 10, 4, 6, 31, 22 | dialss 39056 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ (Base‘𝐾) ∧ 𝑈 ≤ 𝑊)) → (𝐼‘𝑈) ∈ 𝑆) |
41 | 1, 38, 39, 40 | syl12anc 834 |
. . . . 5
⊢ (𝜑 → (𝐼‘𝑈) ∈ 𝑆) |
42 | 24, 41 | sseldd 3927 |
. . . 4
⊢ (𝜑 → (𝐼‘𝑈) ∈ (SubGrp‘𝑌)) |
43 | | dia2dimlem5.r |
. . . . . . . 8
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
44 | | dia2dimlem5.n |
. . . . . . . 8
⊢ 𝑁 = (LSpan‘𝑌) |
45 | 4, 5, 43, 6, 31, 44 | dia1dim2 39072 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) → (𝐼‘(𝑅‘𝐷)) = (𝑁‘{𝐷})) |
46 | 1, 2, 45 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐼‘(𝑅‘𝐷)) = (𝑁‘{𝐷})) |
47 | | dia2dimlem5.j |
. . . . . . . . . 10
⊢ ∨ =
(join‘𝐾) |
48 | | dia2dimlem5.m |
. . . . . . . . . 10
⊢ ∧ =
(meet‘𝐾) |
49 | | dia2dimlem5.q |
. . . . . . . . . 10
⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) |
50 | | dia2dimlem5.rf |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉)) |
51 | | dia2dimlem5.uv |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ≠ 𝑉) |
52 | | dia2dimlem5.ru |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈) |
53 | | dia2dimlem5.rv |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉) |
54 | 10, 47, 48, 11, 4, 5, 43, 49, 1, 35, 25, 12, 13, 50, 51, 52, 53, 2, 16 | dia2dimlem3 39076 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅‘𝐷) = 𝑉) |
55 | 54 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘(𝑅‘𝐷)) = (𝐼‘𝑉)) |
56 | | eqss 3941 |
. . . . . . . 8
⊢ ((𝐼‘(𝑅‘𝐷)) = (𝐼‘𝑉) ↔ ((𝐼‘(𝑅‘𝐷)) ⊆ (𝐼‘𝑉) ∧ (𝐼‘𝑉) ⊆ (𝐼‘(𝑅‘𝐷)))) |
57 | 55, 56 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → ((𝐼‘(𝑅‘𝐷)) ⊆ (𝐼‘𝑉) ∧ (𝐼‘𝑉) ⊆ (𝐼‘(𝑅‘𝐷)))) |
58 | 57 | simpld 495 |
. . . . . 6
⊢ (𝜑 → (𝐼‘(𝑅‘𝐷)) ⊆ (𝐼‘𝑉)) |
59 | 46, 58 | eqsstrrd 3965 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝐷}) ⊆ (𝐼‘𝑉)) |
60 | | eqid 2740 |
. . . . . 6
⊢
(Base‘𝑌) =
(Base‘𝑌) |
61 | 4, 5, 6, 60 | dvavbase 39023 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝑌) = 𝑇) |
62 | 1, 61 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑌) = 𝑇) |
63 | 2, 62 | eleqtrrd 2844 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (Base‘𝑌)) |
64 | 60, 22, 44, 21, 33, 63 | lspsnel5 20255 |
. . . . 5
⊢ (𝜑 → (𝐷 ∈ (𝐼‘𝑉) ↔ (𝑁‘{𝐷}) ⊆ (𝐼‘𝑉))) |
65 | 59, 64 | mpbird 256 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (𝐼‘𝑉)) |
66 | 4, 5, 43, 6, 31, 44 | dia1dim2 39072 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝐼‘(𝑅‘𝐺)) = (𝑁‘{𝐺})) |
67 | 1, 3, 66 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐼‘(𝑅‘𝐺)) = (𝑁‘{𝐺})) |
68 | 10, 47, 48, 11, 4, 5, 43, 49, 1, 35, 25, 12, 13, 50, 53, 3, 15 | dia2dimlem2 39075 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅‘𝐺) = 𝑈) |
69 | 68 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝜑 → (𝐼‘(𝑅‘𝐺)) = (𝐼‘𝑈)) |
70 | | eqss 3941 |
. . . . . . . 8
⊢ ((𝐼‘(𝑅‘𝐺)) = (𝐼‘𝑈) ↔ ((𝐼‘(𝑅‘𝐺)) ⊆ (𝐼‘𝑈) ∧ (𝐼‘𝑈) ⊆ (𝐼‘(𝑅‘𝐺)))) |
71 | 69, 70 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → ((𝐼‘(𝑅‘𝐺)) ⊆ (𝐼‘𝑈) ∧ (𝐼‘𝑈) ⊆ (𝐼‘(𝑅‘𝐺)))) |
72 | 71 | simpld 495 |
. . . . . 6
⊢ (𝜑 → (𝐼‘(𝑅‘𝐺)) ⊆ (𝐼‘𝑈)) |
73 | 67, 72 | eqsstrrd 3965 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝐺}) ⊆ (𝐼‘𝑈)) |
74 | 3, 62 | eleqtrrd 2844 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (Base‘𝑌)) |
75 | 60, 22, 44, 21, 41, 74 | lspsnel5 20255 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ (𝐼‘𝑈) ↔ (𝑁‘{𝐺}) ⊆ (𝐼‘𝑈))) |
76 | 73, 75 | mpbird 256 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐼‘𝑈)) |
77 | | dia2dimlem5.pl |
. . . . 5
⊢ ⊕ =
(LSSum‘𝑌) |
78 | 7, 77 | lsmelvali 19253 |
. . . 4
⊢ ((((𝐼‘𝑉) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑈) ∈ (SubGrp‘𝑌)) ∧ (𝐷 ∈ (𝐼‘𝑉) ∧ 𝐺 ∈ (𝐼‘𝑈))) → (𝐷(+g‘𝑌)𝐺) ∈ ((𝐼‘𝑉) ⊕ (𝐼‘𝑈))) |
79 | 34, 42, 65, 76, 78 | syl22anc 836 |
. . 3
⊢ (𝜑 → (𝐷(+g‘𝑌)𝐺) ∈ ((𝐼‘𝑉) ⊕ (𝐼‘𝑈))) |
80 | 18, 79 | eqeltrd 2841 |
. 2
⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑉) ⊕ (𝐼‘𝑈))) |
81 | | lmodabl 20168 |
. . . 4
⊢ (𝑌 ∈ LMod → 𝑌 ∈ Abel) |
82 | 21, 81 | syl 17 |
. . 3
⊢ (𝜑 → 𝑌 ∈ Abel) |
83 | 77 | lsmcom 19457 |
. . 3
⊢ ((𝑌 ∈ Abel ∧ (𝐼‘𝑉) ∈ (SubGrp‘𝑌) ∧ (𝐼‘𝑈) ∈ (SubGrp‘𝑌)) → ((𝐼‘𝑉) ⊕ (𝐼‘𝑈)) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) |
84 | 82, 34, 42, 83 | syl3anc 1370 |
. 2
⊢ (𝜑 → ((𝐼‘𝑉) ⊕ (𝐼‘𝑈)) = ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) |
85 | 80, 84 | eleqtrd 2843 |
1
⊢ (𝜑 → 𝐹 ∈ ((𝐼‘𝑈) ⊕ (𝐼‘𝑉))) |