Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
2 | | tendof.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | | tendof.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
4 | | eqid 2737 |
. . . . 5
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
5 | | tendof.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
6 | 1, 2, 3, 4, 5 | istendo 39226 |
. . . 4
β’ ((πΎ β π β§ π β π») β (π β πΈ β (π:πβΆπ β§ βπ β π βπ β π (πβ(π β π)) = ((πβπ) β (πβπ)) β§ βπ β π (((trLβπΎ)βπ)β(πβπ))(leβπΎ)(((trLβπΎ)βπ)βπ)))) |
7 | | coeq1 5814 |
. . . . . . . . 9
β’ (π = πΉ β (π β π) = (πΉ β π)) |
8 | 7 | fveq2d 6847 |
. . . . . . . 8
β’ (π = πΉ β (πβ(π β π)) = (πβ(πΉ β π))) |
9 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΉ β (πβπ) = (πβπΉ)) |
10 | 9 | coeq1d 5818 |
. . . . . . . 8
β’ (π = πΉ β ((πβπ) β (πβπ)) = ((πβπΉ) β (πβπ))) |
11 | 8, 10 | eqeq12d 2753 |
. . . . . . 7
β’ (π = πΉ β ((πβ(π β π)) = ((πβπ) β (πβπ)) β (πβ(πΉ β π)) = ((πβπΉ) β (πβπ)))) |
12 | | coeq2 5815 |
. . . . . . . . 9
β’ (π = πΊ β (πΉ β π) = (πΉ β πΊ)) |
13 | 12 | fveq2d 6847 |
. . . . . . . 8
β’ (π = πΊ β (πβ(πΉ β π)) = (πβ(πΉ β πΊ))) |
14 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΊ β (πβπ) = (πβπΊ)) |
15 | 14 | coeq2d 5819 |
. . . . . . . 8
β’ (π = πΊ β ((πβπΉ) β (πβπ)) = ((πβπΉ) β (πβπΊ))) |
16 | 13, 15 | eqeq12d 2753 |
. . . . . . 7
β’ (π = πΊ β ((πβ(πΉ β π)) = ((πβπΉ) β (πβπ)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ)))) |
17 | 11, 16 | rspc2v 3591 |
. . . . . 6
β’ ((πΉ β π β§ πΊ β π) β (βπ β π βπ β π (πβ(π β π)) = ((πβπ) β (πβπ)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ)))) |
18 | 17 | com12 32 |
. . . . 5
β’
(βπ β
π βπ β π (πβ(π β π)) = ((πβπ) β (πβπ)) β ((πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ)))) |
19 | 18 | 3ad2ant2 1135 |
. . . 4
β’ ((π:πβΆπ β§ βπ β π βπ β π (πβ(π β π)) = ((πβπ) β (πβπ)) β§ βπ β π (((trLβπΎ)βπ)β(πβπ))(leβπΎ)(((trLβπΎ)βπ)βπ)) β ((πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ)))) |
20 | 6, 19 | syl6bi 253 |
. . 3
β’ ((πΎ β π β§ π β π») β (π β πΈ β ((πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))))) |
21 | 20 | 3impia 1118 |
. 2
β’ ((πΎ β π β§ π β π» β§ π β πΈ) β ((πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ)))) |
22 | 21 | imp 408 |
1
β’ (((πΎ β π β§ π β π» β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) |