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={\mathrm{Base}}_W$$
	nmpar.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	nmpar.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	nmpar.n	$$⊢N=\mathrm{norm}\left(W\right)$$
Assertion	nmpar	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\wedge B\in V\right)\to {N\left(A\underset{\dot{}}{+}B\right)}^2+{N\left(A\underset{\dot{}}{-}B\right)}^2=2\left({N\left(A\right)}^2+{N\left(B\right)}^2\right)$$

Proof

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