Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
β’
(leβπΎ) =
(leβπΎ) |
2 | | tendof.h |
. 2
β’ π» = (LHypβπΎ) |
3 | | tendof.t |
. 2
β’ π = ((LTrnβπΎ)βπ) |
4 | | eqid 2737 |
. 2
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
5 | | tendof.e |
. 2
β’ πΈ = ((TEndoβπΎ)βπ) |
6 | | id 22 |
. 2
β’ ((πΎ β HL β§ π β π») β (πΎ β HL β§ π β π»)) |
7 | | f1oi 6823 |
. . 3
β’ ( I
βΎ π):πβ1-1-ontoβπ |
8 | | f1of 6785 |
. . 3
β’ (( I
βΎ π):πβ1-1-ontoβπ β ( I βΎ π):πβΆπ) |
9 | 7, 8 | mp1i 13 |
. 2
β’ ((πΎ β HL β§ π β π») β ( I βΎ π):πβΆπ) |
10 | 2, 3 | ltrnco 39185 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (π β π) β π) |
11 | | fvresi 7120 |
. . . 4
β’ ((π β π) β π β (( I βΎ π)β(π β π)) = (π β π)) |
12 | 10, 11 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (( I βΎ π)β(π β π)) = (π β π)) |
13 | | fvresi 7120 |
. . . . 5
β’ (π β π β (( I βΎ π)βπ) = π) |
14 | 13 | 3ad2ant2 1135 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (( I βΎ π)βπ) = π) |
15 | | fvresi 7120 |
. . . . 5
β’ (π β π β (( I βΎ π)βπ) = π) |
16 | 15 | 3ad2ant3 1136 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (( I βΎ π)βπ) = π) |
17 | 14, 16 | coeq12d 5821 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β ((( I βΎ π)βπ) β (( I βΎ π)βπ)) = (π β π)) |
18 | 12, 17 | eqtr4d 2780 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (( I βΎ π)β(π β π)) = ((( I βΎ π)βπ) β (( I βΎ π)βπ))) |
19 | 13 | adantl 483 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (( I βΎ π)βπ) = π) |
20 | 19 | fveq2d 6847 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((trLβπΎ)βπ)β(( I βΎ π)βπ)) = (((trLβπΎ)βπ)βπ)) |
21 | | hllat 37828 |
. . . . 5
β’ (πΎ β HL β πΎ β Lat) |
22 | 21 | ad2antrr 725 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β πΎ β Lat) |
23 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
24 | 23, 2, 3, 4 | trlcl 38630 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((trLβπΎ)βπ)βπ) β (BaseβπΎ)) |
25 | 23, 1 | latref 18331 |
. . . 4
β’ ((πΎ β Lat β§
(((trLβπΎ)βπ)βπ) β (BaseβπΎ)) β (((trLβπΎ)βπ)βπ)(leβπΎ)(((trLβπΎ)βπ)βπ)) |
26 | 22, 24, 25 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((trLβπΎ)βπ)βπ)(leβπΎ)(((trLβπΎ)βπ)βπ)) |
27 | 20, 26 | eqbrtrd 5128 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((trLβπΎ)βπ)β(( I βΎ π)βπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) |
28 | 1, 2, 3, 4, 5, 6, 9, 18, 27 | istendod 39228 |
1
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |