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

Metamath Proof Explorer

Theorem 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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
hlpar2.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
hlpar2.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
hlpar2.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion hlpar2 ( ( 𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 hlpar2.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 hlpar2.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 hlpar2.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
4 hlpar2.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
5 hlph ⊢ ( 𝑈 ∈ CHilOLD → 𝑈 ∈ CPreHilOLD )
6 1 2 3 4 phpar2 ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
7 5 6 syl3an1 ⊢ ( ( 𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( 𝐴 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐵 ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ 𝐴 ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )