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 ⊢ X = BaseSet ⁡ U
hldi.2 ⊢ G = + v ⁡ U
hldi.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion hldir ⊢ U ∈ CHil OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B S C

Proof

Step Hyp Ref Expression
1 hldi.1 ⊢ X = BaseSet ⁡ U
2 hldi.2 ⊢ G = + v ⁡ U
3 hldi.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 hlnv ⊢ U ∈ CHil OLD → U ∈ NrmCVec
5 1 2 3 nvdir ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B S C
6 4 5 sylan ⊢ U ∈ CHil OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B S C