hlpar2

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

	Ref	Expression
Hypotheses	hlpar2.1	$⊢ X = BaseSet (U)$
	hlpar2.2	$⊢ G = +_{v} (U)$
	hlpar2.3	$⊢ M = -_{v} (U)$
	hlpar2.6	$⊢ N = {norm}_{CV} (U)$
Assertion	hlpar2	$⊢ (U \in {CHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A M B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Step	Hyp	Ref	Expression
1		hlpar2.1	$⊢ X = BaseSet (U)$
2		hlpar2.2	$⊢ G = +_{v} (U)$
3		hlpar2.3	$⊢ M = -_{v} (U)$
4		hlpar2.6	$⊢ N = {norm}_{CV} (U)$
5		hlph	$⊢ U \in {CHil}_{OLD} \to U \in {CPreHil}_{OLD}$
6	1 2 3 4	phpar2	$⊢ (U \in {CPreHil}_{OLD} \land A \in X \land B \in X) \to {N (A G B)}^{2} + {N (A M 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 M B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Metamath Proof Explorer