Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (πΎ β HL β§ π β π»)) |
2 | | simpr1 1195 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β π β πΈ) |
3 | | simpr2 1196 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β π β πΈ) |
4 | | tendopl.h |
. . . . 5
β’ π» = (LHypβπΎ) |
5 | | tendopl.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
6 | | tendopl.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
7 | | tendopl.p |
. . . . 5
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
8 | 4, 5, 6, 7 | tendoplcl 39247 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) |
9 | 1, 2, 3, 8 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (πππ) β πΈ) |
10 | | simpr3 1197 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β π β πΈ) |
11 | 4, 5, 6, 7 | tendoplcl 39247 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πππ) β πΈ β§ π β πΈ) β ((πππ)ππ) β πΈ) |
12 | 1, 9, 10, 11 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ)ππ) β πΈ) |
13 | 4, 5, 6, 7 | tendoplcl 39247 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) |
14 | 1, 3, 10, 13 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (πππ) β πΈ) |
15 | 4, 5, 6, 7 | tendoplcl 39247 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πππ) β πΈ) β (ππ(πππ)) β πΈ) |
16 | 1, 2, 14, 15 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (ππ(πππ)) β πΈ) |
17 | | coass 6218 |
. . . . 5
β’ (((πβπ) β (πβπ)) β (πβπ)) = ((πβπ) β ((πβπ) β (πβπ))) |
18 | | simplr1 1216 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
19 | | simplr2 1217 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
20 | | simpr 486 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β π) |
21 | 7, 5 | tendopl2 39243 |
. . . . . . 7
β’ ((π β πΈ β§ π β πΈ β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
22 | 18, 19, 20, 21 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
23 | 22 | coeq1d 5818 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((πππ)βπ) β (πβπ)) = (((πβπ) β (πβπ)) β (πβπ))) |
24 | | simplr3 1218 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
25 | 7, 5 | tendopl2 39243 |
. . . . . . 7
β’ ((π β πΈ β§ π β πΈ β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
26 | 19, 24, 20, 25 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
27 | 26 | coeq2d 5819 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((πβπ) β ((πππ)βπ)) = ((πβπ) β ((πβπ) β (πβπ)))) |
28 | 17, 23, 27 | 3eqtr4a 2803 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((πππ)βπ) β (πβπ)) = ((πβπ) β ((πππ)βπ))) |
29 | 9 | adantr 482 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πππ) β πΈ) |
30 | 7, 5 | tendopl2 39243 |
. . . . 5
β’ (((πππ) β πΈ β§ π β πΈ β§ π β π) β (((πππ)ππ)βπ) = (((πππ)βπ) β (πβπ))) |
31 | 29, 24, 20, 30 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((πππ)ππ)βπ) = (((πππ)βπ) β (πβπ))) |
32 | 14 | adantr 482 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πππ) β πΈ) |
33 | 7, 5 | tendopl2 39243 |
. . . . 5
β’ ((π β πΈ β§ (πππ) β πΈ β§ π β π) β ((ππ(πππ))βπ) = ((πβπ) β ((πππ)βπ))) |
34 | 18, 32, 20, 33 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((ππ(πππ))βπ) = ((πβπ) β ((πππ)βπ))) |
35 | 28, 31, 34 | 3eqtr4d 2787 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((πππ)ππ)βπ) = ((ππ(πππ))βπ)) |
36 | 35 | ralrimiva 3144 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β βπ β π (((πππ)ππ)βπ) = ((ππ(πππ))βπ)) |
37 | 4, 5, 6 | tendoeq1 39230 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (((πππ)ππ) β πΈ β§ (ππ(πππ)) β πΈ) β§ βπ β π (((πππ)ππ)βπ) = ((ππ(πππ))βπ)) β ((πππ)ππ) = (ππ(πππ))) |
38 | 1, 12, 16, 36, 37 | syl121anc 1376 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ)ππ) = (ππ(πππ))) |