Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πΎ β HL β§ π β π»)) |
2 | | tendo0.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | tendo0.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | tendo0.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
5 | | tendo0.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
6 | | tendo0.o |
. . . . 5
β’ π = (π β π β¦ ( I βΎ π΅)) |
7 | 2, 3, 4, 5, 6 | tendo0cl 39256 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π β πΈ) |
8 | 7 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π β πΈ) |
9 | | simpr 486 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π β πΈ) |
10 | | tendo0pl.p |
. . . 4
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
11 | 3, 4, 5, 10 | tendoplcl 39247 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) |
12 | 1, 8, 9, 11 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) β πΈ) |
13 | | simpll 766 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β (πΎ β HL β§ π β π»)) |
14 | 13, 7 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β π β πΈ) |
15 | | simplr 768 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β π β πΈ) |
16 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β π β π) |
17 | 10, 4 | tendopl2 39243 |
. . . . 5
β’ ((π β πΈ β§ π β πΈ β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
18 | 14, 15, 16, 17 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
19 | 6, 2 | tendo02 39253 |
. . . . . 6
β’ (π β π β (πβπ) = ( I βΎ π΅)) |
20 | 19 | adantl 483 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β (πβπ) = ( I βΎ π΅)) |
21 | 20 | coeq1d 5818 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β ((πβπ) β (πβπ)) = (( I βΎ π΅) β (πβπ))) |
22 | 3, 4, 5 | tendocl 39233 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
23 | 22 | 3expa 1119 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β (πβπ) β π) |
24 | 2, 3, 4 | ltrn1o 38590 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β π) β (πβπ):π΅β1-1-ontoβπ΅) |
25 | 13, 23, 24 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β (πβπ):π΅β1-1-ontoβπ΅) |
26 | | f1of 6785 |
. . . . 5
β’ ((πβπ):π΅β1-1-ontoβπ΅ β (πβπ):π΅βΆπ΅) |
27 | | fcoi2 6718 |
. . . . 5
β’ ((πβπ):π΅βΆπ΅ β (( I βΎ π΅) β (πβπ)) = (πβπ)) |
28 | 25, 26, 27 | 3syl 18 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β (( I βΎ π΅) β (πβπ)) = (πβπ)) |
29 | 18, 21, 28 | 3eqtrd 2781 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ π β π) β ((πππ)βπ) = (πβπ)) |
30 | 29 | ralrimiva 3144 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β βπ β π ((πππ)βπ) = (πβπ)) |
31 | 3, 4, 5 | tendoeq1 39230 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((πππ) β πΈ β§ π β πΈ) β§ βπ β π ((πππ)βπ) = (πβπ)) β (πππ) = π) |
32 | 1, 12, 9, 30, 31 | syl121anc 1376 |
1
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) |