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, 6 | tendococl 39238 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πππ) β πΈ β§ π β πΈ) β ((πππ) β π) β πΈ) |
12 | 1, 9, 10, 11 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ) β π) β πΈ) |
13 | 4, 6 | tendococl 39238 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) |
14 | 1, 2, 10, 13 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β π) β πΈ) |
15 | 4, 6 | tendococl 39238 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) |
16 | 1, 3, 10, 15 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β π) β πΈ) |
17 | 4, 5, 6, 7 | tendoplcl 39247 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π) β πΈ β§ (π β π) β πΈ) β ((π β π)π(π β π)) β πΈ) |
18 | 1, 14, 16, 17 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((π β π)π(π β π)) β πΈ) |
19 | | simpll 766 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πΎ β HL β§ π β π»)) |
20 | | simplr1 1216 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
21 | | simplr2 1217 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
22 | 19, 20, 21, 8 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πππ) β πΈ) |
23 | | simplr3 1218 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β πΈ) |
24 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β π) |
25 | 4, 5, 6 | tendocoval 39232 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((πππ) β πΈ β§ π β πΈ) β§ π β π) β (((πππ) β π)βπ) = ((πππ)β(πβπ))) |
26 | 19, 22, 23, 24, 25 | syl121anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((πππ) β π)βπ) = ((πππ)β(πβπ))) |
27 | | simplll 774 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β πΎ β HL) |
28 | | simpllr 775 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β π β π») |
29 | 4, 5, 6 | tendocoval 39232 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
30 | 27, 28, 20, 23, 24, 29 | syl221anc 1382 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
31 | 4, 5, 6 | tendocoval 39232 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
32 | 27, 28, 21, 23, 24, 31 | syl221anc 1382 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
33 | 30, 32 | coeq12d 5821 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((π β π)βπ) β ((π β π)βπ)) = ((πβ(πβπ)) β (πβ(πβπ)))) |
34 | 19, 20, 23, 13 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (π β π) β πΈ) |
35 | 19, 21, 23, 15 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (π β π) β πΈ) |
36 | 7, 5 | tendopl2 39243 |
. . . . . 6
β’ (((π β π) β πΈ β§ (π β π) β πΈ β§ π β π) β (((π β π)π(π β π))βπ) = (((π β π)βπ) β ((π β π)βπ))) |
37 | 34, 35, 24, 36 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((π β π)π(π β π))βπ) = (((π β π)βπ) β ((π β π)βπ))) |
38 | 4, 5, 6 | tendocl 39233 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
39 | 19, 23, 24, 38 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (πβπ) β π) |
40 | 7, 5 | tendopl2 39243 |
. . . . . 6
β’ ((π β πΈ β§ π β πΈ β§ (πβπ) β π) β ((πππ)β(πβπ)) = ((πβ(πβπ)) β (πβ(πβπ)))) |
41 | 20, 21, 39, 40 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((πππ)β(πβπ)) = ((πβ(πβπ)) β (πβ(πβπ)))) |
42 | 33, 37, 41 | 3eqtr4rd 2788 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β ((πππ)β(πβπ)) = (((π β π)π(π β π))βπ)) |
43 | 26, 42 | eqtrd 2777 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β§ π β π) β (((πππ) β π)βπ) = (((π β π)π(π β π))βπ)) |
44 | 43 | ralrimiva 3144 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β βπ β π (((πππ) β π)βπ) = (((π β π)π(π β π))βπ)) |
45 | 4, 5, 6 | tendoeq1 39230 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (((πππ) β π) β πΈ β§ ((π β π)π(π β π)) β πΈ) β§ βπ β π (((πππ) β π)βπ) = (((π β π)π(π β π))βπ)) β ((πππ) β π) = ((π β π)π(π β π))) |
46 | 1, 12, 18, 44, 45 | syl121anc 1376 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ) β π) = ((π β π)π(π β π))) |