Step | Hyp | Ref
| Expression |
1 | | phnv 29805 |
. 2
β’ (π β CPreHilOLD
β π β
NrmCVec) |
2 | | isph.2 |
. . . . 5
β’ πΊ = ( +π£
βπ) |
3 | | eqid 2733 |
. . . . 5
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
4 | | isph.6 |
. . . . 5
β’ π =
(normCVβπ) |
5 | 2, 3, 4 | nvop 29667 |
. . . 4
β’ (π β NrmCVec β π = β¨β¨πΊ, ( Β·π OLD
βπ)β©, πβ©) |
6 | | eleq1 2822 |
. . . . 5
β’ (π = β¨β¨πΊ, ( Β·π OLD
βπ)β©, πβ© β (π β CPreHilOLD β
β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β
CPreHilOLD)) |
7 | 2 | fvexi 6860 |
. . . . . . 7
β’ πΊ β V |
8 | | fvex 6859 |
. . . . . . 7
β’ (
Β·π OLD βπ) β V |
9 | 4 | fvexi 6860 |
. . . . . . 7
β’ π β V |
10 | | isph.1 |
. . . . . . . . 9
β’ π = (BaseSetβπ) |
11 | 10, 2 | bafval 29595 |
. . . . . . . 8
β’ π = ran πΊ |
12 | 11 | isphg 29808 |
. . . . . . 7
β’ ((πΊ β V β§ (
Β·π OLD βπ) β V β§ π β V) β (β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β CPreHilOLD β
(β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) |
13 | 7, 8, 9, 12 | mp3an 1462 |
. . . . . 6
β’
(β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β CPreHilOLD β
(β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) |
14 | | isph.3 |
. . . . . . . . . . . . . . . 16
β’ π = ( βπ£
βπ) |
15 | 10, 2, 3, 14 | nvmval 29633 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ π₯ β π β§ π¦ β π) β (π₯ππ¦) = (π₯πΊ(-1( Β·π OLD
βπ)π¦))) |
16 | 15 | 3expa 1119 |
. . . . . . . . . . . . . 14
β’ (((π β NrmCVec β§ π₯ β π) β§ π¦ β π) β (π₯ππ¦) = (π₯πΊ(-1( Β·π OLD
βπ)π¦))) |
17 | 16 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (((π β NrmCVec β§ π₯ β π) β§ π¦ β π) β (πβ(π₯ππ¦)) = (πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))) |
18 | 17 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ (((π β NrmCVec β§ π₯ β π) β§ π¦ β π) β ((πβ(π₯ππ¦))β2) = ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) |
19 | 18 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (((π β NrmCVec β§ π₯ β π) β§ π¦ β π) β (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2))) |
20 | 19 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π₯ β π) β§ π¦ β π) β ((((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))) β (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) |
21 | 20 | ralbidva 3169 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π₯ β π) β (βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))) β βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) |
22 | 21 | ralbidva 3169 |
. . . . . . . 8
β’ (π β NrmCVec β
(βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))) β βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) |
23 | 22 | pm5.32i 576 |
. . . . . . 7
β’ ((π β NrmCVec β§
βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))) β (π β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) |
24 | | eleq1 2822 |
. . . . . . . 8
β’ (π = β¨β¨πΊ, ( Β·π OLD
βπ)β©, πβ© β (π β NrmCVec β β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β NrmCVec)) |
25 | 24 | anbi1d 631 |
. . . . . . 7
β’ (π = β¨β¨πΊ, ( Β·π OLD
βπ)β©, πβ© β ((π β NrmCVec β§
βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))) β (β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) |
26 | 23, 25 | bitr2id 284 |
. . . . . 6
β’ (π = β¨β¨πΊ, ( Β·π OLD
βπ)β©, πβ© β
((β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1( Β·π OLD
βπ)π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))) β (π β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) |
27 | 13, 26 | bitrid 283 |
. . . . 5
β’ (π = β¨β¨πΊ, ( Β·π OLD
βπ)β©, πβ© β (β¨β¨πΊ, (
Β·π OLD βπ)β©, πβ© β CPreHilOLD β
(π β NrmCVec β§
βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) |
28 | 6, 27 | bitrd 279 |
. . . 4
β’ (π = β¨β¨πΊ, ( Β·π OLD
βπ)β©, πβ© β (π β CPreHilOLD β (π β NrmCVec β§
βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) |
29 | 5, 28 | syl 17 |
. . 3
β’ (π β NrmCVec β (π β CPreHilOLD
β (π β NrmCVec
β§ βπ₯ β
π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) |
30 | 29 | bianabs 543 |
. 2
β’ (π β NrmCVec β (π β CPreHilOLD
β βπ₯ β
π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) |
31 | 1, 30 | biadanii 821 |
1
β’ (π β CPreHilOLD
β (π β NrmCVec
β§ βπ₯ β
π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) |