Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (πΎ β HL β§ π β π»)) |
2 | | simpr1 1195 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β π β πΈ) |
3 | | simpr2 1196 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β π β πΈ) |
4 | | simpr3 1197 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β π β πΈ) |
5 | | tendopl.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | | tendopl.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
7 | | tendopl.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
8 | | tendopl.p |
. . . . 5
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
9 | 5, 6, 7, 8 | tendoplcl 39247 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) |
10 | 1, 3, 4, 9 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (πππ) β πΈ) |
11 | 5, 7 | tendococl 39238 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πππ) β πΈ) β (π β (πππ)) β πΈ) |
12 | 1, 2, 10, 11 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β (πππ)) β πΈ) |
13 | 5, 7 | tendococl 39238 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) |
14 | 1, 2, 3, 13 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β π) β πΈ) |
15 | 5, 7 | tendococl 39238 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) |
16 | 1, 2, 4, 15 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β π) β πΈ) |
17 | 5, 6, 7, 8 | tendoplcl 39247 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π) β πΈ β§ (π β π) β πΈ) β ((π β π)π(π β π)) β πΈ) |
18 | 1, 14, 16, 17 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((π β π)π(π β π)) β πΈ) |
19 | | simplll 774 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β πΎ β HL) |
20 | | simpllr 775 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β π») |
21 | | simplr1 1216 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
22 | | simpll 766 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πΎ β HL β§ π β π»)) |
23 | | simplr2 1217 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
24 | | simpr 486 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β π) |
25 | 5, 6, 7 | tendocl 39233 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
26 | 22, 23, 24, 25 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πβπ) β π) |
27 | | simplr3 1218 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
28 | 5, 6, 7 | tendocl 39233 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
29 | 22, 27, 24, 28 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πβπ) β π) |
30 | 5, 6, 7 | tendovalco 39231 |
. . . . . 6
β’ (((πΎ β HL β§ π β π» β§ π β πΈ) β§ ((πβπ) β π β§ (πβπ) β π)) β (πβ((πβπ) β (πβπ))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
31 | 19, 20, 21, 26, 29, 30 | syl32anc 1379 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πβ((πβπ) β (πβπ))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
32 | 8, 6 | tendopl2 39243 |
. . . . . . 7
β’ ((π β πΈ β§ π β πΈ β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
33 | 23, 27, 24, 32 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((πππ)βπ) = ((πβπ) β (πβπ))) |
34 | 33 | fveq2d 6847 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πβ((πππ)βπ)) = (πβ((πβπ) β (πβπ)))) |
35 | 5, 6, 7 | tendocoval 39232 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
36 | 19, 20, 21, 23, 24, 35 | syl221anc 1382 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
37 | 5, 6, 7 | tendocoval 39232 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
38 | 19, 20, 21, 27, 24, 37 | syl221anc 1382 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
39 | 36, 38 | coeq12d 5821 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((π β π)βπ) β ((π β π)βπ)) = ((πβ(πβπ)) β (πβ(πβπ)))) |
40 | 31, 34, 39 | 3eqtr4rd 2788 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((π β π)βπ) β ((π β π)βπ)) = (πβ((πππ)βπ))) |
41 | 22, 21, 23, 13 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (π β π) β πΈ) |
42 | 22, 21, 27, 15 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (π β π) β πΈ) |
43 | 8, 6 | tendopl2 39243 |
. . . . 5
β’ (((π β π) β πΈ β§ (π β π) β πΈ β§ π β π) β (((π β π)π(π β π))βπ) = (((π β π)βπ) β ((π β π)βπ))) |
44 | 41, 42, 24, 43 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((π β π)π(π β π))βπ) = (((π β π)βπ) β ((π β π)βπ))) |
45 | 22, 23, 27, 9 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πππ) β πΈ) |
46 | 5, 6, 7 | tendocoval 39232 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (πππ) β πΈ) β§ π β π) β ((π β (πππ))βπ) = (πβ((πππ)βπ))) |
47 | 22, 21, 45, 24, 46 | syl121anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((π β (πππ))βπ) = (πβ((πππ)βπ))) |
48 | 40, 44, 47 | 3eqtr4rd 2788 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((π β (πππ))βπ) = (((π β π)π(π β π))βπ)) |
49 | 48 | ralrimiva 3144 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β βπ β π ((π β (πππ))βπ) = (((π β π)π(π β π))βπ)) |
50 | 5, 6, 7 | tendoeq1 39230 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β (πππ)) β πΈ β§ ((π β π)π(π β π)) β πΈ) β§ βπ β π ((π β (πππ))βπ) = (((π β π)π(π β π))βπ)) β (π β (πππ)) = ((π β π)π(π β π))) |
51 | 1, 12, 18, 49, 50 | syl121anc 1376 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β (πππ)) = ((π β π)π(π β π))) |