Metamath Proof Explorer


Theorem hldir

Description: Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hldi.1 𝑋 = ( BaseSet ‘ 𝑈 )
hldi.2 𝐺 = ( +𝑣𝑈 )
hldi.4 𝑆 = ( ·𝑠OLD𝑈 )
Assertion hldir ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶𝑋 ) ) → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 hldi.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 hldi.2 𝐺 = ( +𝑣𝑈 )
3 hldi.4 𝑆 = ( ·𝑠OLD𝑈 )
4 hlnv ( 𝑈 ∈ CHilOLD𝑈 ∈ NrmCVec )
5 1 2 3 nvdir ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶𝑋 ) ) → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) )
6 4 5 sylan ( ( 𝑈 ∈ CHilOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶𝑋 ) ) → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) )