Step | Hyp | Ref
| Expression |
1 | | simp11 1200 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΎ β HL β§ π β π»)) |
2 | | simp13 1202 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π
β π΄ β§ Β¬ π
β€ π)) |
3 | | simp12 1201 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
4 | | simp11l 1281 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β πΎ β HL) |
5 | 4 | hllatd 38690 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β πΎ β Lat) |
6 | | simp2r 1197 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β π΅) |
7 | | simp11r 1282 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β π») |
8 | | dihjust.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
9 | | dihjust.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
10 | 8, 9 | lhpbase 39325 |
. . . . . 6
β’ (π β π» β π β π΅) |
11 | 7, 10 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β π΅) |
12 | | dihjust.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
13 | 8, 12 | latmcl 18392 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
14 | 5, 6, 11, 13 | syl3anc 1368 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β§ π) β π΅) |
15 | | dihjust.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
16 | 8, 15, 12 | latmle2 18417 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β€ π) |
17 | 5, 6, 11, 16 | syl3anc 1368 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β§ π) β€ π) |
18 | 14, 17 | jca 511 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β ((π β§ π) β π΅ β§ (π β§ π) β€ π)) |
19 | | simp12l 1283 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β π΄) |
20 | | dihjust.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
21 | 8, 20 | atbase 38615 |
. . . . . 6
β’ (π β π΄ β π β π΅) |
22 | 19, 21 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β π΅) |
23 | | simp2l 1196 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β π΅) |
24 | 8, 12 | latmcl 18392 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
25 | 5, 23, 11, 24 | syl3anc 1368 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β§ π) β π΅) |
26 | | dihjust.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
27 | 8, 26 | latjcl 18391 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ (π β§ π) β π΅) β (π β¨ (π β§ π)) β π΅) |
28 | 5, 22, 25, 27 | syl3anc 1368 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β¨ (π β§ π)) β π΅) |
29 | 8, 15, 26 | latlej1 18400 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ (π β§ π) β π΅) β π β€ (π β¨ (π β§ π))) |
30 | 5, 22, 25, 29 | syl3anc 1368 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β€ (π β¨ (π β§ π))) |
31 | | simp31 1206 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β¨ (π β§ π)) = π) |
32 | | simp33 1208 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β€ π) |
33 | 31, 32 | eqbrtrd 5160 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β¨ (π β§ π)) β€ π) |
34 | 8, 15, 5, 22, 28, 6, 30, 33 | lattrd 18398 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β€ π) |
35 | | simp32 1207 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π
β¨ (π β§ π)) = π) |
36 | 34, 35 | breqtrrd 5166 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β€ (π
β¨ (π β§ π))) |
37 | | dihjust.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
38 | | dihjust.s |
. . . 4
β’ β =
(LSSumβπ) |
39 | | dihjust.i |
. . . 4
β’ πΌ = ((DIsoBβπΎ)βπ) |
40 | | dihjust.J |
. . . 4
β’ π½ = ((DIsoCβπΎ)βπ) |
41 | 8, 15, 26, 20, 9, 37, 38, 39, 40 | cdlemn5 40528 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ ((π β§ π) β π΅ β§ (π β§ π) β€ π)) β§ π β€ (π
β¨ (π β§ π))) β (π½βπ) β ((π½βπ
) β (πΌβ(π β§ π)))) |
42 | 1, 2, 3, 18, 36, 41 | syl131anc 1380 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π½βπ) β ((π½βπ
) β (πΌβ(π β§ π)))) |
43 | 8, 15, 12 | latmlem1 18421 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β (π β§ π) β€ (π β§ π))) |
44 | 5, 23, 6, 11, 43 | syl13anc 1369 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β€ π β (π β§ π) β€ (π β§ π))) |
45 | 32, 44 | mpd 15 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β§ π) β€ (π β§ π)) |
46 | 8, 15, 12 | latmle2 18417 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β€ π) |
47 | 5, 23, 11, 46 | syl3anc 1368 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π β§ π) β€ π) |
48 | 8, 15, 9, 39 | dibord 40486 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β§ π) β π΅ β§ (π β§ π) β€ π) β§ ((π β§ π) β π΅ β§ (π β§ π) β€ π)) β ((πΌβ(π β§ π)) β (πΌβ(π β§ π)) β (π β§ π) β€ (π β§ π))) |
49 | 1, 25, 47, 14, 17, 48 | syl122anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β ((πΌβ(π β§ π)) β (πΌβ(π β§ π)) β (π β§ π) β€ (π β§ π))) |
50 | 45, 49 | mpbird 257 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΌβ(π β§ π)) β (πΌβ(π β§ π))) |
51 | 9, 37, 1 | dvhlmod 40437 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β π β LMod) |
52 | | eqid 2724 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
53 | 52 | lsssssubg 20790 |
. . . . . 6
β’ (π β LMod β
(LSubSpβπ) β
(SubGrpβπ)) |
54 | 51, 53 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (LSubSpβπ) β (SubGrpβπ)) |
55 | 15, 20, 9, 37, 40, 52 | diclss 40520 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π
β π΄ β§ Β¬ π
β€ π)) β (π½βπ
) β (LSubSpβπ)) |
56 | 1, 2, 55 | syl2anc 583 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π½βπ
) β (LSubSpβπ)) |
57 | 54, 56 | sseldd 3975 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π½βπ
) β (SubGrpβπ)) |
58 | 8, 15, 9, 37, 39, 52 | diblss 40497 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β§ π) β π΅ β§ (π β§ π) β€ π)) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
59 | 1, 14, 17, 58 | syl12anc 834 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
60 | 54, 59 | sseldd 3975 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΌβ(π β§ π)) β (SubGrpβπ)) |
61 | 38 | lsmub2 19563 |
. . . 4
β’ (((π½βπ
) β (SubGrpβπ) β§ (πΌβ(π β§ π)) β (SubGrpβπ)) β (πΌβ(π β§ π)) β ((π½βπ
) β (πΌβ(π β§ π)))) |
62 | 57, 60, 61 | syl2anc 583 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΌβ(π β§ π)) β ((π½βπ
) β (πΌβ(π β§ π)))) |
63 | 50, 62 | sstrd 3984 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΌβ(π β§ π)) β ((π½βπ
) β (πΌβ(π β§ π)))) |
64 | 15, 20, 9, 37, 40, 52 | diclss 40520 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (π½βπ) β (LSubSpβπ)) |
65 | 1, 3, 64 | syl2anc 583 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π½βπ) β (LSubSpβπ)) |
66 | 54, 65 | sseldd 3975 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (π½βπ) β (SubGrpβπ)) |
67 | 8, 15, 9, 37, 39, 52 | diblss 40497 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β§ π) β π΅ β§ (π β§ π) β€ π)) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
68 | 1, 25, 47, 67 | syl12anc 834 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΌβ(π β§ π)) β (LSubSpβπ)) |
69 | 54, 68 | sseldd 3975 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (πΌβ(π β§ π)) β (SubGrpβπ)) |
70 | 52, 38 | lsmcl 20916 |
. . . . 5
β’ ((π β LMod β§ (π½βπ
) β (LSubSpβπ) β§ (πΌβ(π β§ π)) β (LSubSpβπ)) β ((π½βπ
) β (πΌβ(π β§ π))) β (LSubSpβπ)) |
71 | 51, 56, 59, 70 | syl3anc 1368 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β ((π½βπ
) β (πΌβ(π β§ π))) β (LSubSpβπ)) |
72 | 54, 71 | sseldd 3975 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β ((π½βπ
) β (πΌβ(π β§ π))) β (SubGrpβπ)) |
73 | 38 | lsmlub 19569 |
. . 3
β’ (((π½βπ) β (SubGrpβπ) β§ (πΌβ(π β§ π)) β (SubGrpβπ) β§ ((π½βπ
) β (πΌβ(π β§ π))) β (SubGrpβπ)) β (((π½βπ) β ((π½βπ
) β (πΌβ(π β§ π))) β§ (πΌβ(π β§ π)) β ((π½βπ
) β (πΌβ(π β§ π)))) β ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π))))) |
74 | 66, 69, 72, 73 | syl3anc 1368 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β (((π½βπ) β ((π½βπ
) β (πΌβ(π β§ π))) β§ (πΌβ(π β§ π)) β ((π½βπ
) β (πΌβ(π β§ π)))) β ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π))))) |
75 | 42, 63, 74 | mpbi2and 709 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π
β¨ (π β§ π)) = π β§ π β€ π)) β ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ
) β (πΌβ(π β§ π)))) |