Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β HL) |
2 | 1 | hllatd 37855 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β Lat) |
3 | | simp3l 1202 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΄) |
4 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
5 | | trlcolem.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
6 | 4, 5 | atbase 37780 |
. . . . . 6
β’ (π β π΄ β π β (BaseβπΎ)) |
7 | 3, 6 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β (BaseβπΎ)) |
8 | | simp1 1137 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
9 | | simp2r 1201 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ β π) |
10 | | trlco.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
11 | | trlco.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
12 | | trlco.t |
. . . . . . . 8
β’ π = ((LTrnβπΎ)βπ) |
13 | 10, 5, 11, 12 | ltrnat 38632 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
14 | 8, 9, 3, 13 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊβπ) β π΄) |
15 | 4, 5 | atbase 37780 |
. . . . . 6
β’ ((πΊβπ) β π΄ β (πΊβπ) β (BaseβπΎ)) |
16 | 14, 15 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊβπ) β (BaseβπΎ)) |
17 | | trlco.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
18 | 4, 10, 17 | latlej1 18344 |
. . . . 5
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (πΊβπ) β (BaseβπΎ)) β π β€ (π β¨ (πΊβπ))) |
19 | 2, 7, 16, 18 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β€ (π β¨ (πΊβπ))) |
20 | 4, 17, 5 | hlatjcl 37858 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ (πΊβπ) β π΄) β (π β¨ (πΊβπ)) β (BaseβπΎ)) |
21 | 1, 3, 14, 20 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (πΊβπ)) β (BaseβπΎ)) |
22 | | simp2l 1200 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
23 | 4, 11, 12 | ltrncl 38617 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (πΊβπ) β (BaseβπΎ)) β (πΉβ(πΊβπ)) β (BaseβπΎ)) |
24 | 8, 22, 16, 23 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβ(πΊβπ)) β (BaseβπΎ)) |
25 | 4, 10, 17 | latjlej1 18349 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ (πΊβπ)) β (BaseβπΎ) β§ (πΉβ(πΊβπ)) β (BaseβπΎ))) β (π β€ (π β¨ (πΊβπ)) β (π β¨ (πΉβ(πΊβπ))) β€ ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))))) |
26 | 2, 7, 21, 24, 25 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β€ (π β¨ (πΊβπ)) β (π β¨ (πΉβ(πΊβπ))) β€ ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))))) |
27 | 19, 26 | mpd 15 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (πΉβ(πΊβπ))) β€ ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ)))) |
28 | 4, 17 | latjcl 18335 |
. . . . 5
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (πΉβ(πΊβπ)) β (BaseβπΎ)) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
29 | 2, 7, 24, 28 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
30 | 4, 17 | latjcl 18335 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ (πΊβπ)) β (BaseβπΎ) β§ (πΉβ(πΊβπ)) β (BaseβπΎ)) β ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
31 | 2, 21, 24, 30 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
32 | | simp1r 1199 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π») |
33 | 4, 11 | lhpbase 38490 |
. . . . 5
β’ (π β π» β π β (BaseβπΎ)) |
34 | 32, 33 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β (BaseβπΎ)) |
35 | | trlcolem.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
36 | 4, 10, 35 | latmlem1 18365 |
. . . 4
β’ ((πΎ β Lat β§ ((π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ) β§ ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β¨ (πΉβ(πΊβπ))) β€ ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) β€ (((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β§ π))) |
37 | 2, 29, 31, 34, 36 | syl13anc 1373 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΉβ(πΊβπ))) β€ ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) β€ (((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β§ π))) |
38 | 27, 37 | mpd 15 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) β€ (((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β§ π)) |
39 | 11, 12 | ltrnco 39211 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πΉ β πΊ) β π) |
40 | 8, 22, 9, 39 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ β πΊ) β π) |
41 | | trlco.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
42 | 10, 17, 35, 5, 11, 12, 41 | trlval2 38655 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β πΊ) β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πΉ β πΊ)) = ((π β¨ ((πΉ β πΊ)βπ)) β§ π)) |
43 | 40, 42 | syld3an2 1412 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πΉ β πΊ)) = ((π β¨ ((πΉ β πΊ)βπ)) β§ π)) |
44 | 10, 5, 11, 12 | ltrncoval 38637 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β ((πΉ β πΊ)βπ) = (πΉβ(πΊβπ))) |
45 | 44 | 3adant3r 1182 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉ β πΊ)βπ) = (πΉβ(πΊβπ))) |
46 | 45 | oveq2d 7378 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((πΉ β πΊ)βπ)) = (π β¨ (πΉβ(πΊβπ)))) |
47 | 46 | oveq1d 7377 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ ((πΉ β πΊ)βπ)) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |
48 | 43, 47 | eqtrd 2777 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πΉ β πΊ)) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |
49 | 10, 5, 11, 12 | ltrnel 38631 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
50 | 9, 49 | syld3an2 1412 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
51 | 10, 17, 35, 5, 11, 12, 41 | trlval2 38655 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) β (π
βπΉ) = (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) |
52 | 8, 22, 50, 51 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) |
53 | 10, 17, 35, 5, 11, 12, 41 | trlval2 38655 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΊ) = ((π β¨ (πΊβπ)) β§ π)) |
54 | 9, 53 | syld3an2 1412 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΊ) = ((π β¨ (πΊβπ)) β§ π)) |
55 | 52, 54 | oveq12d 7380 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π
βπΉ) β¨ (π
βπΊ)) = ((((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) β¨ ((π β¨ (πΊβπ)) β§ π))) |
56 | 10, 5, 11, 12 | ltrnat 38632 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (πΊβπ) β π΄) β (πΉβ(πΊβπ)) β π΄) |
57 | 8, 22, 14, 56 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβ(πΊβπ)) β π΄) |
58 | 4, 17, 5 | hlatjcl 37858 |
. . . . . 6
β’ ((πΎ β HL β§ (πΊβπ) β π΄ β§ (πΉβ(πΊβπ)) β π΄) β ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
59 | 1, 14, 57, 58 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
60 | 4, 35 | latmcl 18336 |
. . . . 5
β’ ((πΎ β Lat β§ ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) β (BaseβπΎ)) |
61 | 2, 59, 34, 60 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) β (BaseβπΎ)) |
62 | 4, 35 | latmcl 18336 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ (πΊβπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ (πΊβπ)) β§ π) β (BaseβπΎ)) |
63 | 2, 21, 34, 62 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΊβπ)) β§ π) β (BaseβπΎ)) |
64 | 4, 17 | latjcom 18343 |
. . . 4
β’ ((πΎ β Lat β§ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) β (BaseβπΎ) β§ ((π β¨ (πΊβπ)) β§ π) β (BaseβπΎ)) β ((((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) β¨ ((π β¨ (πΊβπ)) β§ π)) = (((π β¨ (πΊβπ)) β§ π) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π))) |
65 | 2, 61, 63, 64 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π) β¨ ((π β¨ (πΊβπ)) β§ π)) = (((π β¨ (πΊβπ)) β§ π) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π))) |
66 | 4, 17 | latjcl 18335 |
. . . . . 6
β’ ((πΎ β Lat β§ (πΊβπ) β (BaseβπΎ) β§ (πΉβ(πΊβπ)) β (BaseβπΎ)) β ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
67 | 2, 16, 24, 66 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
68 | 4, 10, 35 | latmle2 18361 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ (πΊβπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ (πΊβπ)) β§ π) β€ π) |
69 | 2, 21, 34, 68 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΊβπ)) β§ π) β€ π) |
70 | 4, 10, 17, 35, 11 | lhpmod6i1 38531 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (((π β¨ (πΊβπ)) β§ π) β (BaseβπΎ) β§ ((πΊβπ) β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) β§ ((π β¨ (πΊβπ)) β§ π) β€ π) β (((π β¨ (πΊβπ)) β§ π) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) = ((((π β¨ (πΊβπ)) β§ π) β¨ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) β§ π)) |
71 | 8, 63, 67, 69, 70 | syl121anc 1376 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((π β¨ (πΊβπ)) β§ π) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) = ((((π β¨ (πΊβπ)) β§ π) β¨ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) β§ π)) |
72 | 4, 17 | latjass 18379 |
. . . . . . 7
β’ ((πΎ β Lat β§ (((π β¨ (πΊβπ)) β§ π) β (BaseβπΎ) β§ (πΊβπ) β (BaseβπΎ) β§ (πΉβ(πΊβπ)) β (BaseβπΎ))) β ((((π β¨ (πΊβπ)) β§ π) β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) = (((π β¨ (πΊβπ)) β§ π) β¨ ((πΊβπ) β¨ (πΉβ(πΊβπ))))) |
73 | 2, 63, 16, 24, 72 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((((π β¨ (πΊβπ)) β§ π) β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) = (((π β¨ (πΊβπ)) β§ π) β¨ ((πΊβπ) β¨ (πΉβ(πΊβπ))))) |
74 | 4, 10, 17 | latlej2 18345 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (πΊβπ) β (BaseβπΎ)) β (πΊβπ) β€ (π β¨ (πΊβπ))) |
75 | 2, 7, 16, 74 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊβπ) β€ (π β¨ (πΊβπ))) |
76 | 4, 10, 17, 35, 11 | lhpmod2i2 38530 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ ((π β¨ (πΊβπ)) β (BaseβπΎ) β§ (πΊβπ) β (BaseβπΎ)) β§ (πΊβπ) β€ (π β¨ (πΊβπ))) β (((π β¨ (πΊβπ)) β§ π) β¨ (πΊβπ)) = ((π β¨ (πΊβπ)) β§ (π β¨ (πΊβπ)))) |
77 | 8, 21, 16, 75, 76 | syl121anc 1376 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((π β¨ (πΊβπ)) β§ π) β¨ (πΊβπ)) = ((π β¨ (πΊβπ)) β§ (π β¨ (πΊβπ)))) |
78 | | eqid 2737 |
. . . . . . . . . . 11
β’
(1.βπΎ) =
(1.βπΎ) |
79 | 10, 17, 78, 5, 11 | lhpjat1 38512 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) β (π β¨ (πΊβπ)) = (1.βπΎ)) |
80 | 8, 50, 79 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (πΊβπ)) = (1.βπΎ)) |
81 | 80 | oveq2d 7378 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΊβπ)) β§ (π β¨ (πΊβπ))) = ((π β¨ (πΊβπ)) β§ (1.βπΎ))) |
82 | | hlol 37852 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OL) |
83 | 1, 82 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β OL) |
84 | 4, 35, 78 | olm11 37718 |
. . . . . . . . 9
β’ ((πΎ β OL β§ (π β¨ (πΊβπ)) β (BaseβπΎ)) β ((π β¨ (πΊβπ)) β§ (1.βπΎ)) = (π β¨ (πΊβπ))) |
85 | 83, 21, 84 | syl2anc 585 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΊβπ)) β§ (1.βπΎ)) = (π β¨ (πΊβπ))) |
86 | 77, 81, 85 | 3eqtrd 2781 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((π β¨ (πΊβπ)) β§ π) β¨ (πΊβπ)) = (π β¨ (πΊβπ))) |
87 | 86 | oveq1d 7377 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((((π β¨ (πΊβπ)) β§ π) β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) = ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ)))) |
88 | 73, 87 | eqtr3d 2779 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((π β¨ (πΊβπ)) β§ π) β¨ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ)))) |
89 | 88 | oveq1d 7377 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((((π β¨ (πΊβπ)) β§ π) β¨ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) β§ π) = (((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β§ π)) |
90 | 71, 89 | eqtrd 2777 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((π β¨ (πΊβπ)) β§ π) β¨ (((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ π)) = (((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β§ π)) |
91 | 55, 65, 90 | 3eqtrd 2781 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π
βπΉ) β¨ (π
βπΊ)) = (((π β¨ (πΊβπ)) β¨ (πΉβ(πΊβπ))) β§ π)) |
92 | 38, 48, 91 | 3brtr4d 5142 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πΉ β πΊ)) β€ ((π
βπΉ) β¨ (π
βπΊ))) |