Metamath Proof Explorer


Theorem isphg

Description: The predicate "is a complex inner product space." An inner product space is a normed vector space whose norm satisfies the parallelogram law. The vector (group) addition operation is G , the scalar product is S , and the norm is N . An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis isphg.1 X = ran G
Assertion isphg G A S B N C G S N CPreHil OLD G S N NrmCVec x X y X N x G y 2 + N x G -1 S y 2 = 2 N x 2 + N y 2

Proof

Step Hyp Ref Expression
1 isphg.1 X = ran G
2 df-ph CPreHil OLD = NrmCVec g s n | x ran g y ran g n x g y 2 + n x g -1 s y 2 = 2 n x 2 + n y 2
3 2 elin2 G S N CPreHil OLD G S N NrmCVec G S N g s n | x ran g y ran g n x g y 2 + n x g -1 s y 2 = 2 n x 2 + n y 2
4 rneq g = G ran g = ran G
5 4 1 eqtr4di g = G ran g = X
6 oveq g = G x g y = x G y
7 6 fveq2d g = G n x g y = n x G y
8 7 oveq1d g = G n x g y 2 = n x G y 2
9 oveq g = G x g -1 s y = x G -1 s y
10 9 fveq2d g = G n x g -1 s y = n x G -1 s y
11 10 oveq1d g = G n x g -1 s y 2 = n x G -1 s y 2
12 8 11 oveq12d g = G n x g y 2 + n x g -1 s y 2 = n x G y 2 + n x G -1 s y 2
13 12 eqeq1d g = G n x g y 2 + n x g -1 s y 2 = 2 n x 2 + n y 2 n x G y 2 + n x G -1 s y 2 = 2 n x 2 + n y 2
14 5 13 raleqbidv g = G y ran g n x g y 2 + n x g -1 s y 2 = 2 n x 2 + n y 2 y X n x G y 2 + n x G -1 s y 2 = 2 n x 2 + n y 2
15 5 14 raleqbidv g = G x ran g y ran g n x g y 2 + n x g -1 s y 2 = 2 n x 2 + n y 2 x X y X n x G y 2 + n x G -1 s y 2 = 2 n x 2 + n y 2
16 oveq s = S -1 s y = -1 S y
17 16 oveq2d s = S x G -1 s y = x G -1 S y
18 17 fveq2d s = S n x G -1 s y = n x G -1 S y
19 18 oveq1d s = S n x G -1 s y 2 = n x G -1 S y 2
20 19 oveq2d s = S n x G y 2 + n x G -1 s y 2 = n x G y 2 + n x G -1 S y 2
21 20 eqeq1d s = S n x G y 2 + n x G -1 s y 2 = 2 n x 2 + n y 2 n x G y 2 + n x G -1 S y 2 = 2 n x 2 + n y 2
22 21 2ralbidv s = S x X y X n x G y 2 + n x G -1 s y 2 = 2 n x 2 + n y 2 x X y X n x G y 2 + n x G -1 S y 2 = 2 n x 2 + n y 2
23 fveq1 n = N n x G y = N x G y
24 23 oveq1d n = N n x G y 2 = N x G y 2
25 fveq1 n = N n x G -1 S y = N x G -1 S y
26 25 oveq1d n = N n x G -1 S y 2 = N x G -1 S y 2
27 24 26 oveq12d n = N n x G y 2 + n x G -1 S y 2 = N x G y 2 + N x G -1 S y 2
28 fveq1 n = N n x = N x
29 28 oveq1d n = N n x 2 = N x 2
30 fveq1 n = N n y = N y
31 30 oveq1d n = N n y 2 = N y 2
32 29 31 oveq12d n = N n x 2 + n y 2 = N x 2 + N y 2
33 32 oveq2d n = N 2 n x 2 + n y 2 = 2 N x 2 + N y 2
34 27 33 eqeq12d n = N n x G y 2 + n x G -1 S y 2 = 2 n x 2 + n y 2 N x G y 2 + N x G -1 S y 2 = 2 N x 2 + N y 2
35 34 2ralbidv n = N x X y X n x G y 2 + n x G -1 S y 2 = 2 n x 2 + n y 2 x X y X N x G y 2 + N x G -1 S y 2 = 2 N x 2 + N y 2
36 15 22 35 eloprabg G A S B N C G S N g s n | x ran g y ran g n x g y 2 + n x g -1 s y 2 = 2 n x 2 + n y 2 x X y X N x G y 2 + N x G -1 S y 2 = 2 N x 2 + N y 2
37 36 anbi2d G A S B N C G S N NrmCVec G S N g s n | x ran g y ran g n x g y 2 + n x g -1 s y 2 = 2 n x 2 + n y 2 G S N NrmCVec x X y X N x G y 2 + N x G -1 S y 2 = 2 N x 2 + N y 2
38 3 37 syl5bb G A S B N C G S N CPreHil OLD G S N NrmCVec x X y X N x G y 2 + N x G -1 S y 2 = 2 N x 2 + N y 2