Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πΎ β HL β§ π β π»)) |
2 | | tendopl.h |
. . 3
β’ π» = (LHypβπΎ) |
3 | | tendopl.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
4 | | tendopl.e |
. . 3
β’ πΈ = ((TEndoβπΎ)βπ) |
5 | | tendopl.p |
. . 3
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
6 | 2, 3, 4, 5 | tendoplcl 39247 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) |
7 | 2, 3, 4, 5 | tendoplcl 39247 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) |
8 | 7 | 3com23 1127 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) |
9 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β (πΎ β HL β§ π β π»)) |
10 | | simpl2 1193 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β π β πΈ) |
11 | | simpr 486 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β π β π) |
12 | 2, 3, 4 | tendocl 39233 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
13 | 9, 10, 11, 12 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β (πβπ) β π) |
14 | | simpl3 1194 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β π β πΈ) |
15 | 2, 3, 4 | tendocl 39233 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
16 | 9, 14, 11, 15 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β (πβπ) β π) |
17 | 2, 3 | ltrncom 39204 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β π β§ (πβπ) β π) β ((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) |
18 | 9, 13, 16, 17 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β ((πβπ) β (πβπ)) = ((πβπ) β (πβπ))) |
19 | 5, 3 | tendopl2 39243 |
. . . . 5
β’ ((π β πΈ β§ π β πΈ β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
20 | 10, 14, 11, 19 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
21 | 5, 3 | tendopl2 39243 |
. . . . 5
β’ ((π β πΈ β§ π β πΈ β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
22 | 14, 10, 11, 21 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
23 | 18, 20, 22 | 3eqtr4d 2787 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β π) β ((πππ)βπ) = ((πππ)βπ)) |
24 | 23 | ralrimiva 3144 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β βπ β π ((πππ)βπ) = ((πππ)βπ)) |
25 | 2, 3, 4 | tendoeq1 39230 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((πππ) β πΈ β§ (πππ) β πΈ) β§ βπ β π ((πππ)βπ) = ((πππ)βπ)) β (πππ) = (πππ)) |
26 | 1, 6, 8, 24, 25 | syl121anc 1376 |
1
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) = (πππ)) |