Step | Hyp | Ref
| Expression |
1 | | dihmeetlem9.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | dihmeetlem9.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
3 | | simp1 1137 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | dvhlmod 39619 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β π β LMod) |
5 | | eqid 2733 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
6 | 5 | lsssssubg 20434 |
. . . . 5
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
7 | 4, 6 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (LSubSpβπ) β (SubGrpβπ)) |
8 | | simp1l 1198 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β πΎ β HL) |
9 | 8 | hllatd 37872 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β πΎ β Lat) |
10 | | simp2l 1200 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
11 | | simp2r 1201 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
12 | | dihmeetlem9.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
13 | | dihmeetlem9.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
14 | 12, 13 | latmcl 18334 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
15 | 9, 10, 11, 14 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (π β§ π) β π΅) |
16 | | dihmeetlem9.i |
. . . . . 6
β’ πΌ = ((DIsoHβπΎ)βπ) |
17 | 12, 1, 16, 2, 5 | dihlss 39759 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β§ π) β π΅) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
18 | 3, 15, 17 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
19 | 7, 18 | sseldd 3946 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΌβ(π β§ π)) β (SubGrpβπ)) |
20 | | dihmeetlem9.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
21 | 12, 20 | atbase 37797 |
. . . . . 6
β’ (π β π΄ β π β π΅) |
22 | 21 | 3ad2ant3 1136 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β π β π΅) |
23 | 12, 1, 16, 2, 5 | dihlss 39759 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β (LSubSpβπ)) |
24 | 3, 22, 23 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΌβπ) β (LSubSpβπ)) |
25 | 7, 24 | sseldd 3946 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΌβπ) β (SubGrpβπ)) |
26 | 12, 1, 16, 2, 5 | dihlss 39759 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β (LSubSpβπ)) |
27 | 3, 11, 26 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΌβπ) β (LSubSpβπ)) |
28 | 7, 27 | sseldd 3946 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΌβπ) β (SubGrpβπ)) |
29 | | dihmeetlem9.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
30 | 12, 29, 13 | latmle2 18359 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β€ π) |
31 | 9, 10, 11, 30 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (π β§ π) β€ π) |
32 | 12, 29, 1, 16 | dihord 39773 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β§ π) β π΅ β§ π β π΅) β ((πΌβ(π β§ π)) β (πΌβπ) β (π β§ π) β€ π)) |
33 | 3, 15, 11, 32 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β ((πΌβ(π β§ π)) β (πΌβπ) β (π β§ π) β€ π)) |
34 | 31, 33 | mpbird 257 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (πΌβ(π β§ π)) β (πΌβπ)) |
35 | | dihmeetlem9.s |
. . . 4
β’ β =
(LSSumβπ) |
36 | 35 | lsmmod 19462 |
. . 3
β’ ((((πΌβ(π β§ π)) β (SubGrpβπ) β§ (πΌβπ) β (SubGrpβπ) β§ (πΌβπ) β (SubGrpβπ)) β§ (πΌβ(π β§ π)) β (πΌβπ)) β ((πΌβ(π β§ π)) β ((πΌβπ) β© (πΌβπ))) = (((πΌβ(π β§ π)) β (πΌβπ)) β© (πΌβπ))) |
37 | 19, 25, 28, 34, 36 | syl31anc 1374 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β ((πΌβ(π β§ π)) β ((πΌβπ) β© (πΌβπ))) = (((πΌβ(π β§ π)) β (πΌβπ)) β© (πΌβπ))) |
38 | | lmodabl 20384 |
. . . . 5
β’ (π β LMod β π β Abel) |
39 | 4, 38 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β π β Abel) |
40 | 35 | lsmcom 19641 |
. . . 4
β’ ((π β Abel β§ (πΌβ(π β§ π)) β (SubGrpβπ) β§ (πΌβπ) β (SubGrpβπ)) β ((πΌβ(π β§ π)) β (πΌβπ)) = ((πΌβπ) β (πΌβ(π β§ π)))) |
41 | 39, 19, 25, 40 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β ((πΌβ(π β§ π)) β (πΌβπ)) = ((πΌβπ) β (πΌβ(π β§ π)))) |
42 | 41 | ineq1d 4172 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (((πΌβ(π β§ π)) β (πΌβπ)) β© (πΌβπ)) = (((πΌβπ) β (πΌβ(π β§ π))) β© (πΌβπ))) |
43 | 37, 42 | eqtr2d 2774 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (((πΌβπ) β (πΌβ(π β§ π))) β© (πΌβπ)) = ((πΌβ(π β§ π)) β ((πΌβπ) β© (πΌβπ)))) |