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	$⊢ \underset{˙}{+} = +_{W}$
	nmpar.m	$⊢ \underset{˙}{-} = -_{W}$
	nmpar.n	$⊢ N = norm (W)$
Assertion	nmpar	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to {N (A \underset{˙}{+} B)}^{2} + {N (A \underset{˙}{-} B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Step	Hyp	Ref	Expression
1		nmpar.v	$⊢ V = {Base}_{W}$
2		nmpar.p	$⊢ \underset{˙}{+} = +_{W}$
3		nmpar.m	$⊢ \underset{˙}{-} = -_{W}$
4		nmpar.n	$⊢ N = norm (W)$
5		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
8		simp1	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to W \in CPreHil$
9		simp2	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to A \in V$
10		simp3	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to B \in V$
11	1 2 3 4 5 6 7 8 9 10	nmparlem	$⊢ (W \in CPreHil \land A \in V \land B \in V) \to {N (A \underset{˙}{+} B)}^{2} + {N (A \underset{˙}{-} B)}^{2} = 2 ({N (A)}^{2} + {N (B)}^{2})$

Metamath Proof Explorer