Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. 2
β’
(leβπΎ) =
(leβπΎ) |
2 | | tendoco.h |
. 2
β’ π» = (LHypβπΎ) |
3 | | eqid 2732 |
. 2
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
4 | | eqid 2732 |
. 2
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
5 | | tendoco.e |
. 2
β’ πΈ = ((TEndoβπΎ)βπ) |
6 | | simp1 1136 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πΎ β HL β§ π β π»)) |
7 | | simp2 1137 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π β πΈ) |
8 | 2, 3, 5 | tendof 39720 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
9 | 6, 7, 8 | syl2anc 584 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
10 | | simp3 1138 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π β πΈ) |
11 | 2, 3, 5 | tendof 39720 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
12 | 6, 10, 11 | syl2anc 584 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
13 | | fco 6741 |
. . 3
β’ ((π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ π:((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) β (π β π):((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
14 | 9, 12, 13 | syl2anc 584 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π):((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
15 | | simp11l 1284 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β πΎ β HL) |
16 | | simp11r 1285 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β π») |
17 | | simp13 1205 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
18 | | simp2 1137 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β ((LTrnβπΎ)βπ)) |
19 | | simp3 1138 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β ((LTrnβπΎ)βπ)) |
20 | 2, 3, 5 | tendovalco 39722 |
. . . . . 6
β’ (((πΎ β HL β§ π β π» β§ π β πΈ) β§ (π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ))) β (πβ(π β π)) = ((πβπ) β (πβπ))) |
21 | 15, 16, 17, 18, 19, 20 | syl32anc 1378 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(π β π)) = ((πβπ) β (πβπ))) |
22 | 21 | fveq2d 6895 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(πβ(π β π))) = (πβ((πβπ) β (πβπ)))) |
23 | | simp12 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
24 | | simp11 1203 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πΎ β HL β§ π β π»)) |
25 | 2, 3, 5 | tendocl 39724 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
26 | 24, 17, 18, 25 | syl3anc 1371 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
27 | 2, 3, 5 | tendocl 39724 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
28 | 24, 17, 19, 27 | syl3anc 1371 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
29 | 2, 3, 5 | tendovalco 39722 |
. . . . 5
β’ (((πΎ β HL β§ π β π» β§ π β πΈ) β§ ((πβπ) β ((LTrnβπΎ)βπ) β§ (πβπ) β ((LTrnβπΎ)βπ))) β (πβ((πβπ) β (πβπ))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
30 | 15, 16, 23, 26, 28, 29 | syl32anc 1378 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ((πβπ) β (πβπ))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
31 | 22, 30 | eqtrd 2772 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(πβ(π β π))) = ((πβ(πβπ)) β (πβ(πβπ)))) |
32 | 2, 3 | ltrnco 39676 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (π β π) β ((LTrnβπΎ)βπ)) |
33 | 24, 18, 19, 32 | syl3anc 1371 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (π β π) β ((LTrnβπΎ)βπ)) |
34 | 2, 3, 5 | tendocoval 39723 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (π β π) β ((LTrnβπΎ)βπ)) β ((π β π)β(π β π)) = (πβ(πβ(π β π)))) |
35 | 24, 23, 17, 33, 34 | syl121anc 1375 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)β(π β π)) = (πβ(πβ(π β π)))) |
36 | 2, 3, 5 | tendocoval 39723 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
37 | 15, 16, 23, 17, 18, 36 | syl221anc 1381 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
38 | 2, 3, 5 | tendocoval 39723 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
39 | 15, 16, 23, 17, 19, 38 | syl221anc 1381 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
40 | 37, 39 | coeq12d 5864 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (((π β π)βπ) β ((π β π)βπ)) = ((πβ(πβπ)) β (πβ(πβπ)))) |
41 | 31, 35, 40 | 3eqtr4d 2782 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)β(π β π)) = (((π β π)βπ) β ((π β π)βπ))) |
42 | | eqid 2732 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
43 | | simpl1l 1224 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β πΎ β HL) |
44 | 43 | hllatd 38320 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β πΎ β Lat) |
45 | | simpl1 1191 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (πΎ β HL β§ π β π»)) |
46 | | simpl2 1192 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
47 | | simpl3 1193 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β πΈ) |
48 | | simpr 485 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β ((LTrnβπΎ)βπ)) |
49 | 45, 46, 47, 48, 36 | syl121anc 1375 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
50 | 45, 47, 48, 25 | syl3anc 1371 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (πβπ) β ((LTrnβπΎ)βπ)) |
51 | 2, 3, 5 | tendocl 39724 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πβπ) β ((LTrnβπΎ)βπ)) β (πβ(πβπ)) β ((LTrnβπΎ)βπ)) |
52 | 45, 46, 50, 51 | syl3anc 1371 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (πβ(πβπ)) β ((LTrnβπΎ)βπ)) |
53 | 49, 52 | eqeltrd 2833 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) β ((LTrnβπΎ)βπ)) |
54 | 42, 2, 3, 4 | trlcl 39121 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π)βπ) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ)) β (BaseβπΎ)) |
55 | 45, 53, 54 | syl2anc 584 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ)) β (BaseβπΎ)) |
56 | 42, 2, 3, 4 | trlcl 39121 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πβπ) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ)) β (BaseβπΎ)) |
57 | 45, 50, 56 | syl2anc 584 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ)) β (BaseβπΎ)) |
58 | 42, 2, 3, 4 | trlcl 39121 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β (BaseβπΎ)) |
59 | 45, 48, 58 | syl2anc 584 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β (BaseβπΎ)) |
60 | | simpl1r 1225 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β π β π») |
61 | 43, 60, 46, 47, 48, 36 | syl221anc 1381 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β ((π β π)βπ) = (πβ(πβπ))) |
62 | 61 | fveq2d 6895 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ)) = (((trLβπΎ)βπ)β(πβ(πβπ)))) |
63 | 1, 2, 3, 4, 5 | tendotp 39718 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πβπ) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβ(πβπ)))(leβπΎ)(((trLβπΎ)βπ)β(πβπ))) |
64 | 45, 46, 50, 63 | syl3anc 1371 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβ(πβπ)))(leβπΎ)(((trLβπΎ)βπ)β(πβπ))) |
65 | 62, 64 | eqbrtrd 5170 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ))(leβπΎ)(((trLβπΎ)βπ)β(πβπ))) |
66 | 1, 2, 3, 4, 5 | tendotp 39718 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) |
67 | 45, 47, 48, 66 | syl3anc 1371 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) |
68 | 42, 1, 44, 55, 57, 59, 65, 67 | lattrd 18401 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π β π)βπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) |
69 | 1, 2, 3, 4, 5, 6, 14, 41, 68 | istendod 39719 |
1
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) |