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