Step | Hyp | Ref
| Expression |
1 | | phpar.2 |
. . . . . 6
β’ πΊ = ( +π£
βπ) |
2 | 1 | fvexi 6861 |
. . . . 5
β’ πΊ β V |
3 | | phpar.4 |
. . . . . 6
β’ π = (
Β·π OLD βπ) |
4 | 3 | fvexi 6861 |
. . . . 5
β’ π β V |
5 | | phpar.6 |
. . . . . 6
β’ π =
(normCVβπ) |
6 | 5 | fvexi 6861 |
. . . . 5
β’ π β V |
7 | 2, 4, 6 | 3pm3.2i 1340 |
. . . 4
β’ (πΊ β V β§ π β V β§ π β V) |
8 | 1, 3, 5 | phop 29802 |
. . . . . 6
β’ (π β CPreHilOLD
β π =
β¨β¨πΊ, πβ©, πβ©) |
9 | 8 | eleq1d 2823 |
. . . . 5
β’ (π β CPreHilOLD
β (π β
CPreHilOLD β β¨β¨πΊ, πβ©, πβ© β
CPreHilOLD)) |
10 | 9 | ibi 267 |
. . . 4
β’ (π β CPreHilOLD
β β¨β¨πΊ, πβ©, πβ© β
CPreHilOLD) |
11 | | phpar.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
12 | 11, 1 | bafval 29588 |
. . . . . 6
β’ π = ran πΊ |
13 | 12 | isphg 29801 |
. . . . 5
β’ ((πΊ β V β§ π β V β§ π β V) β
(β¨β¨πΊ, πβ©, πβ© β CPreHilOLD β
(β¨β¨πΊ, πβ©, πβ© β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) |
14 | 13 | simplbda 501 |
. . . 4
β’ (((πΊ β V β§ π β V β§ π β V) β§
β¨β¨πΊ, πβ©, πβ© β CPreHilOLD) β
βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))) |
15 | 7, 10, 14 | sylancr 588 |
. . 3
β’ (π β CPreHilOLD
β βπ₯ β
π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))) |
16 | 15 | 3ad2ant1 1134 |
. 2
β’ ((π β CPreHilOLD
β§ π΄ β π β§ π΅ β π) β βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))) |
17 | | fvoveq1 7385 |
. . . . . . 7
β’ (π₯ = π΄ β (πβ(π₯πΊπ¦)) = (πβ(π΄πΊπ¦))) |
18 | 17 | oveq1d 7377 |
. . . . . 6
β’ (π₯ = π΄ β ((πβ(π₯πΊπ¦))β2) = ((πβ(π΄πΊπ¦))β2)) |
19 | | fvoveq1 7385 |
. . . . . . 7
β’ (π₯ = π΄ β (πβ(π₯πΊ(-1ππ¦))) = (πβ(π΄πΊ(-1ππ¦)))) |
20 | 19 | oveq1d 7377 |
. . . . . 6
β’ (π₯ = π΄ β ((πβ(π₯πΊ(-1ππ¦)))β2) = ((πβ(π΄πΊ(-1ππ¦)))β2)) |
21 | 18, 20 | oveq12d 7380 |
. . . . 5
β’ (π₯ = π΄ β (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (((πβ(π΄πΊπ¦))β2) + ((πβ(π΄πΊ(-1ππ¦)))β2))) |
22 | | fveq2 6847 |
. . . . . . . 8
β’ (π₯ = π΄ β (πβπ₯) = (πβπ΄)) |
23 | 22 | oveq1d 7377 |
. . . . . . 7
β’ (π₯ = π΄ β ((πβπ₯)β2) = ((πβπ΄)β2)) |
24 | 23 | oveq1d 7377 |
. . . . . 6
β’ (π₯ = π΄ β (((πβπ₯)β2) + ((πβπ¦)β2)) = (((πβπ΄)β2) + ((πβπ¦)β2))) |
25 | 24 | oveq2d 7378 |
. . . . 5
β’ (π₯ = π΄ β (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))) = (2 Β· (((πβπ΄)β2) + ((πβπ¦)β2)))) |
26 | 21, 25 | eqeq12d 2753 |
. . . 4
β’ (π₯ = π΄ β ((((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))) β (((πβ(π΄πΊπ¦))β2) + ((πβ(π΄πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ¦)β2))))) |
27 | | oveq2 7370 |
. . . . . . . 8
β’ (π¦ = π΅ β (π΄πΊπ¦) = (π΄πΊπ΅)) |
28 | 27 | fveq2d 6851 |
. . . . . . 7
β’ (π¦ = π΅ β (πβ(π΄πΊπ¦)) = (πβ(π΄πΊπ΅))) |
29 | 28 | oveq1d 7377 |
. . . . . 6
β’ (π¦ = π΅ β ((πβ(π΄πΊπ¦))β2) = ((πβ(π΄πΊπ΅))β2)) |
30 | | oveq2 7370 |
. . . . . . . . 9
β’ (π¦ = π΅ β (-1ππ¦) = (-1ππ΅)) |
31 | 30 | oveq2d 7378 |
. . . . . . . 8
β’ (π¦ = π΅ β (π΄πΊ(-1ππ¦)) = (π΄πΊ(-1ππ΅))) |
32 | 31 | fveq2d 6851 |
. . . . . . 7
β’ (π¦ = π΅ β (πβ(π΄πΊ(-1ππ¦))) = (πβ(π΄πΊ(-1ππ΅)))) |
33 | 32 | oveq1d 7377 |
. . . . . 6
β’ (π¦ = π΅ β ((πβ(π΄πΊ(-1ππ¦)))β2) = ((πβ(π΄πΊ(-1ππ΅)))β2)) |
34 | 29, 33 | oveq12d 7380 |
. . . . 5
β’ (π¦ = π΅ β (((πβ(π΄πΊπ¦))β2) + ((πβ(π΄πΊ(-1ππ¦)))β2)) = (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2))) |
35 | | fveq2 6847 |
. . . . . . . 8
β’ (π¦ = π΅ β (πβπ¦) = (πβπ΅)) |
36 | 35 | oveq1d 7377 |
. . . . . . 7
β’ (π¦ = π΅ β ((πβπ¦)β2) = ((πβπ΅)β2)) |
37 | 36 | oveq2d 7378 |
. . . . . 6
β’ (π¦ = π΅ β (((πβπ΄)β2) + ((πβπ¦)β2)) = (((πβπ΄)β2) + ((πβπ΅)β2))) |
38 | 37 | oveq2d 7378 |
. . . . 5
β’ (π¦ = π΅ β (2 Β· (((πβπ΄)β2) + ((πβπ¦)β2))) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) |
39 | 34, 38 | eqeq12d 2753 |
. . . 4
β’ (π¦ = π΅ β ((((πβ(π΄πΊπ¦))β2) + ((πβ(π΄πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ¦)β2))) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2))))) |
40 | 26, 39 | rspc2v 3593 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2))))) |
41 | 40 | 3adant1 1131 |
. 2
β’ ((π β CPreHilOLD
β§ π΄ β π β§ π΅ β π) β (βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2))))) |
42 | 16, 41 | mpd 15 |
1
β’ ((π β CPreHilOLD
β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) |