Metamath Proof Explorer

Theorem cncph

Description: The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007) (Revised by Mario Carneiro, 7-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypothesis cncph.6 
|- U = <. <. + , x. >. , abs >.
Assertion cncph 
|- U e. CPreHilOLD

Proof

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