Theorem nmpar

Description: A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	nmpar.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	nmpar.p	⊢ + = ( +g ‘ 𝑊 )
	nmpar.m	⊢ − = ( -g ‘ 𝑊 )
	nmpar.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
Assertion	nmpar	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmpar.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		nmpar.p	⊢ + = ( +g ‘ 𝑊 )
3		nmpar.m	⊢ − = ( -g ‘ 𝑊 )
4		nmpar.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
5		eqid	⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
6		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
8		simp1	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ ℂPreHil )
9		simp2	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
10		simp3	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
11	1 2 3 4 5 6 7 8 9 10	nmparlem	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( 𝑁 ‘ ( 𝐴 + 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 − 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )