Step | Hyp | Ref
| Expression |
1 | | dihjust.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | dihjust.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
3 | | simp11 1202 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | dvhlmod 40285 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β π β LMod) |
5 | | eqid 2731 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
6 | 5 | lsssssubg 20714 |
. . . . 5
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
7 | 4, 6 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (LSubSpβπ) β (SubGrpβπ)) |
8 | | simp12 1203 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
9 | | dihjust.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
10 | | dihjust.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
11 | | dihjust.J |
. . . . . 6
β’ π½ = ((DIsoCβπΎ)βπ) |
12 | 9, 10, 1, 2, 11, 5 | diclss 40368 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (π½βπ) β (LSubSpβπ)) |
13 | 3, 8, 12 | syl2anc 583 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (π½βπ) β (LSubSpβπ)) |
14 | 7, 13 | sseldd 3983 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (π½βπ) β (SubGrpβπ)) |
15 | | simp11l 1283 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β πΎ β HL) |
16 | 15 | hllatd 38538 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β πΎ β Lat) |
17 | | simp2l 1198 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β π β π΅) |
18 | | simp11r 1284 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β π β π») |
19 | | dihjust.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
20 | 19, 1 | lhpbase 39173 |
. . . . . . 7
β’ (π β π» β π β π΅) |
21 | 18, 20 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β π β π΅) |
22 | | dihjust.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
23 | 19, 22 | latmcl 18398 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
24 | 16, 17, 21, 23 | syl3anc 1370 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (π β§ π) β π΅) |
25 | 19, 9, 22 | latmle2 18423 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β€ π) |
26 | 16, 17, 21, 25 | syl3anc 1370 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (π β§ π) β€ π) |
27 | | dihjust.i |
. . . . . 6
β’ πΌ = ((DIsoBβπΎ)βπ) |
28 | 19, 9, 1, 2, 27, 5 | diblss 40345 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β§ π) β π΅ β§ (π β§ π) β€ π)) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
29 | 3, 24, 26, 28 | syl12anc 834 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
30 | 7, 29 | sseldd 3983 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (πΌβ(π β§ π)) β (SubGrpβπ)) |
31 | | dihjust.s |
. . . 4
β’ β =
(LSSumβπ) |
32 | 31 | lsmub2 19568 |
. . 3
β’ (((π½βπ) β (SubGrpβπ) β§ (πΌβ(π β§ π)) β (SubGrpβπ)) β (πΌβ(π β§ π)) β ((π½βπ) β (πΌβ(π β§ π)))) |
33 | 14, 30, 32 | syl2anc 583 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (πΌβ(π β§ π)) β ((π½βπ) β (πΌβ(π β§ π)))) |
34 | | simp3 1137 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) |
35 | 33, 34 | sstrd 3992 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) β (πΌβ(π β§ π)) β ((π½βπ
) β (πΌβ(π β§ π)))) |