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