Step | Hyp | Ref
| Expression |
1 | | f1otrkg.2 |
. . 3
β’ ((π β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) |
2 | 1 | ralrimivvva 3204 |
. 2
β’ (π β βπ β π΅ βπ β π΅ βπ β π΅ (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) |
3 | | f1otrgitv.x |
. . 3
β’ (π β π β π΅) |
4 | | f1otrgitv.y |
. . 3
β’ (π β π β π΅) |
5 | | f1otrgitv.z |
. . 3
β’ (π β π β π΅) |
6 | | oveq1 7416 |
. . . . . 6
β’ (π = π β (ππ½π) = (ππ½π)) |
7 | 6 | eleq2d 2820 |
. . . . 5
β’ (π = π β (π β (ππ½π) β π β (ππ½π))) |
8 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
9 | 8 | oveq1d 7424 |
. . . . . 6
β’ (π = π β ((πΉβπ)πΌ(πΉβπ)) = ((πΉβπ)πΌ(πΉβπ))) |
10 | 9 | eleq2d 2820 |
. . . . 5
β’ (π = π β ((πΉβπ) β ((πΉβπ)πΌ(πΉβπ)) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) |
11 | 7, 10 | bibi12d 346 |
. . . 4
β’ (π = π β ((π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))))) |
12 | | oveq2 7417 |
. . . . . 6
β’ (π = π β (ππ½π) = (ππ½π)) |
13 | 12 | eleq2d 2820 |
. . . . 5
β’ (π = π β (π β (ππ½π) β π β (ππ½π))) |
14 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
15 | 14 | oveq2d 7425 |
. . . . . 6
β’ (π = π β ((πΉβπ)πΌ(πΉβπ)) = ((πΉβπ)πΌ(πΉβπ))) |
16 | 15 | eleq2d 2820 |
. . . . 5
β’ (π = π β ((πΉβπ) β ((πΉβπ)πΌ(πΉβπ)) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) |
17 | 13, 16 | bibi12d 346 |
. . . 4
β’ (π = π β ((π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))))) |
18 | | eleq1 2822 |
. . . . 5
β’ (π = π β (π β (ππ½π) β π β (ππ½π))) |
19 | | fveq2 6892 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
20 | 19 | eleq1d 2819 |
. . . . 5
β’ (π = π β ((πΉβπ) β ((πΉβπ)πΌ(πΉβπ)) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) |
21 | 18, 20 | bibi12d 346 |
. . . 4
β’ (π = π β ((π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))))) |
22 | 11, 17, 21 | rspc3v 3628 |
. . 3
β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β (βπ β π΅ βπ β π΅ βπ β π΅ (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))))) |
23 | 3, 4, 5, 22 | syl3anc 1372 |
. 2
β’ (π β (βπ β π΅ βπ β π΅ βπ β π΅ (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))) β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ))))) |
24 | 2, 23 | mpd 15 |
1
β’ (π β (π β (ππ½π) β (πΉβπ) β ((πΉβπ)πΌ(πΉβπ)))) |