Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β πΎ β HL) |
2 | | simp1r 1199 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β π β π») |
3 | | simp2l 1200 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β π β πΈ) |
4 | | simp3l 1202 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β πΉ β π) |
5 | | simp3r 1203 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β πΊ β π) |
6 | | tendof.h |
. . . . 5
β’ π» = (LHypβπΎ) |
7 | | tendof.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
8 | | tendof.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
9 | 6, 7, 8 | tendovalco 39231 |
. . . 4
β’ (((πΎ β HL β§ π β π» β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) |
10 | 1, 2, 3, 4, 5, 9 | syl32anc 1379 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) |
11 | | simp2r 1201 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β π β πΈ) |
12 | 6, 7, 8 | tendovalco 39231 |
. . . 4
β’ (((πΎ β HL β§ π β π» β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) |
13 | 1, 2, 11, 4, 5, 12 | syl32anc 1379 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) |
14 | 10, 13 | coeq12d 5821 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β ((πβ(πΉ β πΊ)) β (πβ(πΉ β πΊ))) = (((πβπΉ) β (πβπΊ)) β ((πβπΉ) β (πβπΊ)))) |
15 | | simp1 1137 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πΎ β HL β§ π β π»)) |
16 | 6, 7, 8 | tendocl 39233 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΊ β π) β (πβπΊ) β π) |
17 | 15, 3, 5, 16 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβπΊ) β π) |
18 | 6, 7, 8 | tendocl 39233 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) |
19 | 15, 11, 4, 18 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβπΉ) β π) |
20 | 6, 7 | ltrnco4 39205 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πβπΊ) β π β§ (πβπΉ) β π) β (((πβπΉ) β (πβπΊ)) β ((πβπΉ) β (πβπΊ))) = (((πβπΉ) β (πβπΉ)) β ((πβπΊ) β (πβπΊ)))) |
21 | 15, 17, 19, 20 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (((πβπΉ) β (πβπΊ)) β ((πβπΉ) β (πβπΊ))) = (((πβπΉ) β (πβπΉ)) β ((πβπΊ) β (πβπΊ)))) |
22 | 14, 21 | eqtrd 2777 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β ((πβ(πΉ β πΊ)) β (πβ(πΉ β πΊ))) = (((πβπΉ) β (πβπΉ)) β ((πβπΊ) β (πβπΊ)))) |