This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )