Theorem hlpar

Description: The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlpar.1	|- X = ( BaseSet ` U )
	hlpar.2	|- G = ( +v ` U )
	hlpar.4	|- S = ( .sOLD ` U )
	hlpar.6	|- N = ( normCV ` U )
Assertion	hlpar	|- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlpar.1	|- X = ( BaseSet ` U )
2		hlpar.2	|- G = ( +v ` U )
3		hlpar.4	|- S = ( .sOLD ` U )
4		hlpar.6	|- N = ( normCV ` U )
5		hlph	|- ( U e. CHilOLD -> U e. CPreHilOLD )
6	1 2 3 4	phpar	|- ( ( U e. CPreHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )
7	5 6	syl3an1	|- ( ( U e. CHilOLD /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) + ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )