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 = ( Base ` W )
nmpar.p 
|- .+ = ( +g ` W )
nmpar.m 
|- .- = ( -g ` W )
nmpar.n 
|- N = ( norm ` W )
Assertion nmpar 
|- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) + ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 nmpar.v 
 |-  V = ( Base ` W )
2 nmpar.p 
 |-  .+ = ( +g ` W )
3 nmpar.m 
 |-  .- = ( -g ` W )
4 nmpar.n 
 |-  N = ( norm ` W )
5 eqid 
 |-  ( .i ` W ) = ( .i ` W )
6 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
7 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
8 simp1 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> W e. CPreHil )
9 simp2 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> A e. V )
10 simp3 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> B e. V )
11 1 2 3 4 5 6 7 8 9 10 nmparlem 
 |-  ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) + ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )