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 = \cdot_{𝑠OLD} (U)$
	hlpar.6	$⊢ N = {norm}_{CV} (U)$
Assertion	hlpar	$⊢ (U \in {CHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Step	Hyp	Ref	Expression
1		hlpar.1	$⊢ X = BaseSet (U)$
2		hlpar.2	$⊢ G = +_{v} (U)$
3		hlpar.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		hlpar.6	$⊢ N = {norm}_{CV} (U)$
5		hlph	$⊢ U \in {CHil}_{OLD} \to U \in {CPreHil}_{OLD}$
6	1 2 3 4	phpar	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$
7	5 6	syl3an1	$⊢ (U \in {CHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A G (-1 S B))}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Metamath Proof Explorer