Metamath Proof Explorer


Theorem nmpar

Description: A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses nmpar.v V=BaseW
nmpar.p +˙=+W
nmpar.m -˙=-W
nmpar.n N=normW
Assertion nmpar WCPreHilAVBVNA+˙B2+NA-˙B2=2NA2+NB2

Proof

Step Hyp Ref Expression
1 nmpar.v V=BaseW
2 nmpar.p +˙=+W
3 nmpar.m -˙=-W
4 nmpar.n N=normW
5 eqid 𝑖W=𝑖W
6 eqid ScalarW=ScalarW
7 eqid BaseScalarW=BaseScalarW
8 simp1 WCPreHilAVBVWCPreHil
9 simp2 WCPreHilAVBVAV
10 simp3 WCPreHilAVBVBV
11 1 2 3 4 5 6 7 8 9 10 nmparlem WCPreHilAVBVNA+˙B2+NA-˙B2=2NA2+NB2