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=+×abs
Assertion cncph UCPreHilOLD

Proof

Step Hyp Ref Expression
1 cncph.6 U=+×abs
2 eqid +×abs=+×abs
3 2 cnnv +×absNrmCVec
4 mulm1 y-1y=y
5 4 adantl xy-1y=y
6 5 oveq2d xyx+-1y=x+y
7 negsub xyx+y=xy
8 6 7 eqtrd xyx+-1y=xy
9 8 fveq2d xyx+-1y=xy
10 9 oveq1d xyx+-1y2=xy2
11 10 oveq2d xyx+y2+x+-1y2=x+y2+xy2
12 sqabsadd xyx+y2=x2+y2+2xy
13 sqabssub xyxy2=x2+y2-2xy
14 12 13 oveq12d xyx+y2+xy2=x2+y2+2xy+x2+y2-2xy
15 abscl xx
16 15 recnd xx
17 16 sqcld xx2
18 abscl yy
19 18 recnd yy
20 19 sqcld yy2
21 addcl x2y2x2+y2
22 17 20 21 syl2an xyx2+y2
23 2cn 2
24 cjcl yy
25 mulcl xyxy
26 24 25 sylan2 xyxy
27 recl xyxy
28 27 recnd xyxy
29 26 28 syl xyxy
30 mulcl 2xy2xy
31 23 29 30 sylancr xy2xy
32 22 31 22 ppncand xyx2+y2+2xy+x2+y2-2xy=x2+y2+x2+y2
33 14 32 eqtrd xyx+y2+xy2=x2+y2+x2+y2
34 2times x2+y22x2+y2=x2+y2+x2+y2
35 34 eqcomd x2+y2x2+y2+x2+y2=2x2+y2
36 22 35 syl xyx2+y2+x2+y2=2x2+y2
37 33 36 eqtrd xyx+y2+xy2=2x2+y2
38 11 37 eqtrd xyx+y2+x+-1y2=2x2+y2
39 38 rgen2 xyx+y2+x+-1y2=2x2+y2
40 addex +V
41 mulex ×V
42 absf abs:
43 cnex V
44 fex abs:VabsV
45 42 43 44 mp2an absV
46 cnaddabloOLD +AbelOp
47 ablogrpo +AbelOp+GrpOp
48 46 47 ax-mp +GrpOp
49 ax-addf +:×
50 49 fdmi dom+=×
51 48 50 grporn =ran+
52 51 isphg +V×VabsV+×absCPreHilOLD+×absNrmCVecxyx+y2+x+-1y2=2x2+y2
53 40 41 45 52 mp3an +×absCPreHilOLD+×absNrmCVecxyx+y2+x+-1y2=2x2+y2
54 3 39 53 mpbir2an +×absCPreHilOLD
55 1 54 eqeltri UCPreHilOLD