Step |
Hyp |
Ref |
Expression |
1 |
|
isphg.1 |
|- X = ran G |
2 |
|
df-ph |
|- CPreHilOLD = ( NrmCVec i^i { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } ) |
3 |
2
|
elin2 |
|- ( <. <. G , S >. , N >. e. CPreHilOLD <-> ( <. <. G , S >. , N >. e. NrmCVec /\ <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } ) ) |
4 |
|
rneq |
|- ( g = G -> ran g = ran G ) |
5 |
4 1
|
eqtr4di |
|- ( g = G -> ran g = X ) |
6 |
|
oveq |
|- ( g = G -> ( x g y ) = ( x G y ) ) |
7 |
6
|
fveq2d |
|- ( g = G -> ( n ` ( x g y ) ) = ( n ` ( x G y ) ) ) |
8 |
7
|
oveq1d |
|- ( g = G -> ( ( n ` ( x g y ) ) ^ 2 ) = ( ( n ` ( x G y ) ) ^ 2 ) ) |
9 |
|
oveq |
|- ( g = G -> ( x g ( -u 1 s y ) ) = ( x G ( -u 1 s y ) ) ) |
10 |
9
|
fveq2d |
|- ( g = G -> ( n ` ( x g ( -u 1 s y ) ) ) = ( n ` ( x G ( -u 1 s y ) ) ) ) |
11 |
10
|
oveq1d |
|- ( g = G -> ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) = ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) |
12 |
8 11
|
oveq12d |
|- ( g = G -> ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) ) |
13 |
12
|
eqeq1d |
|- ( g = G -> ( ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) ) |
14 |
5 13
|
raleqbidv |
|- ( g = G -> ( A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) ) |
15 |
5 14
|
raleqbidv |
|- ( g = G -> ( A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) ) |
16 |
|
oveq |
|- ( s = S -> ( -u 1 s y ) = ( -u 1 S y ) ) |
17 |
16
|
oveq2d |
|- ( s = S -> ( x G ( -u 1 s y ) ) = ( x G ( -u 1 S y ) ) ) |
18 |
17
|
fveq2d |
|- ( s = S -> ( n ` ( x G ( -u 1 s y ) ) ) = ( n ` ( x G ( -u 1 S y ) ) ) ) |
19 |
18
|
oveq1d |
|- ( s = S -> ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) = ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) |
20 |
19
|
oveq2d |
|- ( s = S -> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) ) |
21 |
20
|
eqeq1d |
|- ( s = S -> ( ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) ) |
22 |
21
|
2ralbidv |
|- ( s = S -> ( A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) ) ) |
23 |
|
fveq1 |
|- ( n = N -> ( n ` ( x G y ) ) = ( N ` ( x G y ) ) ) |
24 |
23
|
oveq1d |
|- ( n = N -> ( ( n ` ( x G y ) ) ^ 2 ) = ( ( N ` ( x G y ) ) ^ 2 ) ) |
25 |
|
fveq1 |
|- ( n = N -> ( n ` ( x G ( -u 1 S y ) ) ) = ( N ` ( x G ( -u 1 S y ) ) ) ) |
26 |
25
|
oveq1d |
|- ( n = N -> ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) = ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) |
27 |
24 26
|
oveq12d |
|- ( n = N -> ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) ) |
28 |
|
fveq1 |
|- ( n = N -> ( n ` x ) = ( N ` x ) ) |
29 |
28
|
oveq1d |
|- ( n = N -> ( ( n ` x ) ^ 2 ) = ( ( N ` x ) ^ 2 ) ) |
30 |
|
fveq1 |
|- ( n = N -> ( n ` y ) = ( N ` y ) ) |
31 |
30
|
oveq1d |
|- ( n = N -> ( ( n ` y ) ^ 2 ) = ( ( N ` y ) ^ 2 ) ) |
32 |
29 31
|
oveq12d |
|- ( n = N -> ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) = ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) |
33 |
32
|
oveq2d |
|- ( n = N -> ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) |
34 |
27 33
|
eqeq12d |
|- ( n = N -> ( ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) |
35 |
34
|
2ralbidv |
|- ( n = N -> ( A. x e. X A. y e. X ( ( ( n ` ( x G y ) ) ^ 2 ) + ( ( n ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) <-> A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) |
36 |
15 22 35
|
eloprabg |
|- ( ( G e. A /\ S e. B /\ N e. C ) -> ( <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } <-> A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) |
37 |
36
|
anbi2d |
|- ( ( G e. A /\ S e. B /\ N e. C ) -> ( ( <. <. G , S >. , N >. e. NrmCVec /\ <. <. G , S >. , N >. e. { <. <. g , s >. , n >. | A. x e. ran g A. y e. ran g ( ( ( n ` ( x g y ) ) ^ 2 ) + ( ( n ` ( x g ( -u 1 s y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( n ` x ) ^ 2 ) + ( ( n ` y ) ^ 2 ) ) ) } ) <-> ( <. <. G , S >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) ) |
38 |
3 37
|
syl5bb |
|- ( ( G e. A /\ S e. B /\ N e. C ) -> ( <. <. G , S >. , N >. e. CPreHilOLD <-> ( <. <. G , S >. , N >. e. NrmCVec /\ A. x e. X A. y e. X ( ( ( N ` ( x G y ) ) ^ 2 ) + ( ( N ` ( x G ( -u 1 S y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` x ) ^ 2 ) + ( ( N ` y ) ^ 2 ) ) ) ) ) ) |