Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’
(leβπΎ) =
(leβπΎ) |
2 | | tendoco.h |
. 2
β’ π» = (LHypβπΎ) |
3 | | eqid 2733 |
. 2
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
4 | | eqid 2733 |
. 2
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
5 | | tendoco.e |
. 2
β’ πΈ = ((TEndoβπΎ)βπ) |
6 | | simp1 1137 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πΎ β HL β§ π β π»)) |
7 | | simp2 1138 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π β πΈ) |
8 | 2, 3, 5 | tendof 39634 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
9 | 6, 7, 8 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
10 | | simp3 1139 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π β πΈ) |
11 | 2, 3, 5 | tendof 39634 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
12 | 6, 10, 11 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
13 | | fco 6742 |
. . 3
β’ ((π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) β (π β π):((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
14 | 9, 12, 13 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π):((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
15 | | simp11l 1285 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β πΎ β HL) |
16 | | simp11r 1286 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β π») |
17 | | simp13 1206 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
18 | | simp2 1138 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β ((LTrnβπΎ)βπ)) |
19 | | simp3 1139 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β ((LTrnβπΎ)βπ)) |
20 | 2, 3, 5 | tendovalco 39636 |
. . . . . 6
β’ (((πΎ β HL β§ π β π» β§ π β πΈ) β§ (π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ))) β (πβ(π β π)) = ((πβπ) β (πβπ))) |
21 | 15, 16, 17, 18, 19, 20 | syl32anc 1379 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(π β π)) = ((πβπ) β (πβπ))) |
22 | 21 | fveq2d 6896 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(πβ(π β π))) = (πβ((πβπ) β (πβπ)))) |
23 | | simp12 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
24 | | simp11 1204 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πΎ β HL β§ π β π»)) |
25 | 2, 3, 5 | tendocl 39638 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
26 | 24, 17, 18, 25 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
27 | 2, 3, 5 | tendocl 39638 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
28 | 24, 17, 19, 27 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
29 | 2, 3, 5 | tendovalco 39636 |
. . . . 5
β’ (((πΎ β HL β§ π β π» β§ π β πΈ) β§ ((πβπ) β ((LTrnβπΎ)βπ) β§ (πβπ) β ((LTrnβπΎ)βπ))) β (πβ((πβπ) β (πβπ))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
30 | 15, 16, 23, 26, 28, 29 | syl32anc 1379 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ((πβπ) β (πβπ))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
31 | 22, 30 | eqtrd 2773 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(πβ(π β π))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
32 | 2, 3 | ltrnco 39590 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (π β π) β ((LTrnβπΎ)βπ)) |
33 | 24, 18, 19, 32 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (π β π) β ((LTrnβπΎ)βπ)) |
34 | 2, 3, 5 | tendocoval 39637 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (π β π) β ((LTrnβπΎ)βπ)) β ((π β π)β(π β π)) = (πβ(πβ(π β π)))) |
35 | 24, 23, 17, 33, 34 | syl121anc 1376 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)β(π β π)) = (πβ(πβ(π β π)))) |
36 | 2, 3, 5 | tendocoval 39637 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
37 | 15, 16, 23, 17, 18, 36 | syl221anc 1382 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
38 | 2, 3, 5 | tendocoval 39637 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
39 | 15, 16, 23, 17, 19, 38 | syl221anc 1382 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
40 | 37, 39 | coeq12d 5865 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (((π β π)βπ) β ((π β π)βπ)) = ((πβ(πβπ)) β (πβ(πβπ)))) |
41 | 31, 35, 40 | 3eqtr4d 2783 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)β(π β π)) = (((π β π)βπ) β ((π β π)βπ))) |
42 | | eqid 2733 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
43 | | simpl1l 1225 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β πΎ β HL) |
44 | 43 | hllatd 38234 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β πΎ β Lat) |
45 | | simpl1 1192 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (πΎ β HL β§ π β π»)) |
46 | | simpl2 1193 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
47 | | simpl3 1194 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
48 | | simpr 486 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β ((LTrnβπΎ)βπ)) |
49 | 45, 46, 47, 48, 36 | syl121anc 1376 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
50 | 45, 47, 48, 25 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
51 | 2, 3, 5 | tendocl 39638 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πβπ) β ((LTrnβπΎ)βπ)) β (πβ(πβπ)) β ((LTrnβπΎ)βπ)) |
52 | 45, 46, 50, 51 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(πβπ)) β ((LTrnβπΎ)βπ)) |
53 | 49, 52 | eqeltrd 2834 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) β ((LTrnβπΎ)βπ)) |
54 | 42, 2, 3, 4 | trlcl 39035 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π)βπ) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ)) β (BaseβπΎ)) |
55 | 45, 53, 54 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ)) β (BaseβπΎ)) |
56 | 42, 2, 3, 4 | trlcl 39035 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ)) β (BaseβπΎ)) |
57 | 45, 50, 56 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ)) β (BaseβπΎ)) |
58 | 42, 2, 3, 4 | trlcl 39035 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β (BaseβπΎ)) |
59 | 45, 48, 58 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β (BaseβπΎ)) |
60 | | simpl1r 1226 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β π») |
61 | 43, 60, 46, 47, 48, 36 | syl221anc 1382 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
62 | 61 | fveq2d 6896 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ)) = (((trLβπΎ)βπ)β(πβ(πβπ)))) |
63 | 1, 2, 3, 4, 5 | tendotp 39632 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πβπ) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβ(πβπ)))(leβπΎ)(((trLβπΎ)βπ)β(πβπ))) |
64 | 45, 46, 50, 63 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβ(πβπ)))(leβπΎ)(((trLβπΎ)βπ)β(πβπ))) |
65 | 62, 64 | eqbrtrd 5171 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ))(leβπΎ)(((trLβπΎ)βπ)β(πβπ))) |
66 | 1, 2, 3, 4, 5 | tendotp 39632 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) |
67 | 45, 47, 48, 66 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) |
68 | 42, 1, 44, 55, 57, 59, 65, 67 | lattrd 18399 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) |
69 | 1, 2, 3, 4, 5, 6, 14, 41, 68 | istendod 39633 |
1
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) |