Metamath Proof Explorer


Theorem hlipdir

Description: Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hlipdir.1 𝑋 = ( BaseSet ‘ 𝑈 )
hlipdir.2 𝐺 = ( +𝑣𝑈 )
hlipdir.7 𝑃 = ( ·𝑖OLD𝑈 )
Assertion hlipdir ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 hlipdir.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 hlipdir.2 𝐺 = ( +𝑣𝑈 )
3 hlipdir.7 𝑃 = ( ·𝑖OLD𝑈 )
4 hlph ( 𝑈 ∈ CHilOLD𝑈 ∈ CPreHilOLD )
5 1 2 3 dipdir ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )
6 4 5 sylan ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴𝑋𝐵𝑋𝐶𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )