Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
2 | | simp2r 1201 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ β π) |
3 | | simp2l 1200 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
4 | | cdlemk.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
5 | | cdlemk.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
6 | 4, 5 | ltrncnv 38612 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
7 | 1, 3, 6 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β β‘πΉ β π) |
8 | 4, 5 | ltrnco 39185 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ β‘πΉ β π) β (πΊ β β‘πΉ) β π) |
9 | 1, 2, 7, 8 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β β‘πΉ) β π) |
10 | | cdlemk.l |
. . . . 5
β’ β€ =
(leβπΎ) |
11 | | cdlemk.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
12 | 10, 11, 4, 5 | ltrnel 38605 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
13 | 12 | 3adant2r 1180 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
14 | | cdlemk.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
15 | | cdlemk.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
16 | 10, 14, 11, 4, 5, 15 | trljat3 38634 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΊ β β‘πΉ) β π β§ ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) β ((πΉβπ) β¨ (π
β(πΊ β β‘πΉ))) = (((πΊ β β‘πΉ)β(πΉβπ)) β¨ (π
β(πΊ β β‘πΉ)))) |
17 | 1, 9, 13, 16 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ (π
β(πΊ β β‘πΉ))) = (((πΊ β β‘πΉ)β(πΉβπ)) β¨ (π
β(πΊ β β‘πΉ)))) |
18 | | simp3l 1202 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΄) |
19 | 10, 11, 4, 5 | ltrncoval 38611 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((πΊ β β‘πΉ) β π β§ πΉ β π) β§ π β π΄) β (((πΊ β β‘πΉ) β πΉ)βπ) = ((πΊ β β‘πΉ)β(πΉβπ))) |
20 | 1, 9, 3, 18, 19 | syl121anc 1376 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊ β β‘πΉ) β πΉ)βπ) = ((πΊ β β‘πΉ)β(πΉβπ))) |
21 | | coass 6218 |
. . . . . 6
β’ ((πΊ β β‘πΉ) β πΉ) = (πΊ β (β‘πΉ β πΉ)) |
22 | | cdlemk.b |
. . . . . . . . . . 11
β’ π΅ = (BaseβπΎ) |
23 | 22, 4, 5 | ltrn1o 38590 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:π΅β1-1-ontoβπ΅) |
24 | 1, 3, 23 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ:π΅β1-1-ontoβπ΅) |
25 | | f1ococnv1 6814 |
. . . . . . . . 9
β’ (πΉ:π΅β1-1-ontoβπ΅ β (β‘πΉ β πΉ) = ( I βΎ π΅)) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (β‘πΉ β πΉ) = ( I βΎ π΅)) |
27 | 26 | coeq2d 5819 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β (β‘πΉ β πΉ)) = (πΊ β ( I βΎ π΅))) |
28 | 22, 4, 5 | ltrn1o 38590 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β πΊ:π΅β1-1-ontoβπ΅) |
29 | 1, 2, 28 | syl2anc 585 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ:π΅β1-1-ontoβπ΅) |
30 | | f1of 6785 |
. . . . . . . 8
β’ (πΊ:π΅β1-1-ontoβπ΅ β πΊ:π΅βΆπ΅) |
31 | | fcoi1 6717 |
. . . . . . . 8
β’ (πΊ:π΅βΆπ΅ β (πΊ β ( I βΎ π΅)) = πΊ) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β ( I βΎ π΅)) = πΊ) |
33 | 27, 32 | eqtrd 2777 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β (β‘πΉ β πΉ)) = πΊ) |
34 | 21, 33 | eqtrid 2789 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊ β β‘πΉ) β πΉ) = πΊ) |
35 | 34 | fveq1d 6845 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊ β β‘πΉ) β πΉ)βπ) = (πΊβπ)) |
36 | 20, 35 | eqtr3d 2779 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊ β β‘πΉ)β(πΉβπ)) = (πΊβπ)) |
37 | 36 | oveq1d 7373 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊ β β‘πΉ)β(πΉβπ)) β¨ (π
β(πΊ β β‘πΉ))) = ((πΊβπ) β¨ (π
β(πΊ β β‘πΉ)))) |
38 | 17, 37 | eqtr2d 2778 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β¨ (π
β(πΊ β β‘πΉ))) = ((πΉβπ) β¨ (π
β(πΊ β β‘πΉ)))) |