Step |
Hyp |
Ref |
Expression |
1 |
|
cncph.6 |
|- U = <. <. + , x. >. , abs >. |
2 |
|
eqid |
|- <. <. + , x. >. , abs >. = <. <. + , x. >. , abs >. |
3 |
2
|
cnnv |
|- <. <. + , x. >. , abs >. e. NrmCVec |
4 |
|
mulm1 |
|- ( y e. CC -> ( -u 1 x. y ) = -u y ) |
5 |
4
|
adantl |
|- ( ( x e. CC /\ y e. CC ) -> ( -u 1 x. y ) = -u y ) |
6 |
5
|
oveq2d |
|- ( ( x e. CC /\ y e. CC ) -> ( x + ( -u 1 x. y ) ) = ( x + -u y ) ) |
7 |
|
negsub |
|- ( ( x e. CC /\ y e. CC ) -> ( x + -u y ) = ( x - y ) ) |
8 |
6 7
|
eqtrd |
|- ( ( x e. CC /\ y e. CC ) -> ( x + ( -u 1 x. y ) ) = ( x - y ) ) |
9 |
8
|
fveq2d |
|- ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x + ( -u 1 x. y ) ) ) = ( abs ` ( x - y ) ) ) |
10 |
9
|
oveq1d |
|- ( ( x e. CC /\ y e. CC ) -> ( ( abs ` ( x + ( -u 1 x. y ) ) ) ^ 2 ) = ( ( abs ` ( x - y ) ) ^ 2 ) ) |
11 |
10
|
oveq2d |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x + ( -u 1 x. y ) ) ) ^ 2 ) ) = ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x - y ) ) ^ 2 ) ) ) |
12 |
|
sqabsadd |
|- ( ( x e. CC /\ y e. CC ) -> ( ( abs ` ( x + y ) ) ^ 2 ) = ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) ) ) |
13 |
|
sqabssub |
|- ( ( x e. CC /\ y e. CC ) -> ( ( abs ` ( x - y ) ) ^ 2 ) = ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) - ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) ) ) |
14 |
12 13
|
oveq12d |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x - y ) ) ^ 2 ) ) = ( ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) ) + ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) - ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) ) ) ) |
15 |
|
abscl |
|- ( x e. CC -> ( abs ` x ) e. RR ) |
16 |
15
|
recnd |
|- ( x e. CC -> ( abs ` x ) e. CC ) |
17 |
16
|
sqcld |
|- ( x e. CC -> ( ( abs ` x ) ^ 2 ) e. CC ) |
18 |
|
abscl |
|- ( y e. CC -> ( abs ` y ) e. RR ) |
19 |
18
|
recnd |
|- ( y e. CC -> ( abs ` y ) e. CC ) |
20 |
19
|
sqcld |
|- ( y e. CC -> ( ( abs ` y ) ^ 2 ) e. CC ) |
21 |
|
addcl |
|- ( ( ( ( abs ` x ) ^ 2 ) e. CC /\ ( ( abs ` y ) ^ 2 ) e. CC ) -> ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) e. CC ) |
22 |
17 20 21
|
syl2an |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) e. CC ) |
23 |
|
2cn |
|- 2 e. CC |
24 |
|
cjcl |
|- ( y e. CC -> ( * ` y ) e. CC ) |
25 |
|
mulcl |
|- ( ( x e. CC /\ ( * ` y ) e. CC ) -> ( x x. ( * ` y ) ) e. CC ) |
26 |
24 25
|
sylan2 |
|- ( ( x e. CC /\ y e. CC ) -> ( x x. ( * ` y ) ) e. CC ) |
27 |
|
recl |
|- ( ( x x. ( * ` y ) ) e. CC -> ( Re ` ( x x. ( * ` y ) ) ) e. RR ) |
28 |
27
|
recnd |
|- ( ( x x. ( * ` y ) ) e. CC -> ( Re ` ( x x. ( * ` y ) ) ) e. CC ) |
29 |
26 28
|
syl |
|- ( ( x e. CC /\ y e. CC ) -> ( Re ` ( x x. ( * ` y ) ) ) e. CC ) |
30 |
|
mulcl |
|- ( ( 2 e. CC /\ ( Re ` ( x x. ( * ` y ) ) ) e. CC ) -> ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) e. CC ) |
31 |
23 29 30
|
sylancr |
|- ( ( x e. CC /\ y e. CC ) -> ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) e. CC ) |
32 |
22 31 22
|
ppncand |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) ) + ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) - ( 2 x. ( Re ` ( x x. ( * ` y ) ) ) ) ) ) = ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) |
33 |
14 32
|
eqtrd |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x - y ) ) ^ 2 ) ) = ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) |
34 |
|
2times |
|- ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) e. CC -> ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) = ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) |
35 |
34
|
eqcomd |
|- ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) e. CC -> ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) |
36 |
22 35
|
syl |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) + ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) = ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) |
37 |
33 36
|
eqtrd |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x - y ) ) ^ 2 ) ) = ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) |
38 |
11 37
|
eqtrd |
|- ( ( x e. CC /\ y e. CC ) -> ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x + ( -u 1 x. y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) |
39 |
38
|
rgen2 |
|- A. x e. CC A. y e. CC ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x + ( -u 1 x. y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) |
40 |
|
addex |
|- + e. _V |
41 |
|
mulex |
|- x. e. _V |
42 |
|
absf |
|- abs : CC --> RR |
43 |
|
cnex |
|- CC e. _V |
44 |
|
fex |
|- ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V ) |
45 |
42 43 44
|
mp2an |
|- abs e. _V |
46 |
|
cnaddabloOLD |
|- + e. AbelOp |
47 |
|
ablogrpo |
|- ( + e. AbelOp -> + e. GrpOp ) |
48 |
46 47
|
ax-mp |
|- + e. GrpOp |
49 |
|
ax-addf |
|- + : ( CC X. CC ) --> CC |
50 |
49
|
fdmi |
|- dom + = ( CC X. CC ) |
51 |
48 50
|
grporn |
|- CC = ran + |
52 |
51
|
isphg |
|- ( ( + e. _V /\ x. e. _V /\ abs e. _V ) -> ( <. <. + , x. >. , abs >. e. CPreHilOLD <-> ( <. <. + , x. >. , abs >. e. NrmCVec /\ A. x e. CC A. y e. CC ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x + ( -u 1 x. y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) ) ) |
53 |
40 41 45 52
|
mp3an |
|- ( <. <. + , x. >. , abs >. e. CPreHilOLD <-> ( <. <. + , x. >. , abs >. e. NrmCVec /\ A. x e. CC A. y e. CC ( ( ( abs ` ( x + y ) ) ^ 2 ) + ( ( abs ` ( x + ( -u 1 x. y ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( abs ` x ) ^ 2 ) + ( ( abs ` y ) ^ 2 ) ) ) ) ) |
54 |
3 39 53
|
mpbir2an |
|- <. <. + , x. >. , abs >. e. CPreHilOLD |
55 |
1 54
|
eqeltri |
|- U e. CPreHilOLD |