Metamath Proof Explorer


Theorem hhph

Description: The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 U=+norm
Assertion hhph UCPreHilOLD

Proof

Step Hyp Ref Expression
1 hhnv.1 U=+norm
2 eqid +norm=+norm
3 2 hhnv +normNrmCVec
4 normpar xynormx-y2+normx+y2=2normx2+2normy2
5 hvsubval xyx-y=x+-1y
6 5 fveq2d xynormx-y=normx+-1y
7 6 oveq1d xynormx-y2=normx+-1y2
8 7 oveq2d xynormx+y2+normx-y2=normx+y2+normx+-1y2
9 hvaddcl xyx+y
10 normcl x+ynormx+y
11 9 10 syl xynormx+y
12 11 recnd xynormx+y
13 12 sqcld xynormx+y2
14 hvsubcl xyx-y
15 normcl x-ynormx-y
16 15 recnd x-ynormx-y
17 14 16 syl xynormx-y
18 17 sqcld xynormx-y2
19 13 18 addcomd xynormx+y2+normx-y2=normx-y2+normx+y2
20 8 19 eqtr3d xynormx+y2+normx+-1y2=normx-y2+normx+y2
21 normcl xnormx
22 21 recnd xnormx
23 22 sqcld xnormx2
24 normcl ynormy
25 24 recnd ynormy
26 25 sqcld ynormy2
27 2cn 2
28 adddi 2normx2normy22normx2+normy2=2normx2+2normy2
29 27 28 mp3an1 normx2normy22normx2+normy2=2normx2+2normy2
30 23 26 29 syl2an xy2normx2+normy2=2normx2+2normy2
31 4 20 30 3eqtr4d xynormx+y2+normx+-1y2=2normx2+normy2
32 31 rgen2 xynormx+y2+normx+-1y2=2normx2+normy2
33 hilablo +AbelOp
34 33 elexi +V
35 hvmulex V
36 normf norm:
37 ax-hilex V
38 fex norm:VnormV
39 36 37 38 mp2an normV
40 1 eleq1i UCPreHilOLD+normCPreHilOLD
41 ablogrpo +AbelOp+GrpOp
42 33 41 ax-mp +GrpOp
43 ax-hfvadd +:×
44 43 fdmi dom+=×
45 42 44 grporn =ran+
46 45 isphg +VVnormV+normCPreHilOLD+normNrmCVecxynormx+y2+normx+-1y2=2normx2+normy2
47 40 46 syl5bb +VVnormVUCPreHilOLD+normNrmCVecxynormx+y2+normx+-1y2=2normx2+normy2
48 34 35 39 47 mp3an UCPreHilOLD+normNrmCVecxynormx+y2+normx+-1y2=2normx2+normy2
49 3 32 48 mpbir2an UCPreHilOLD