Metamath Proof Explorer

Theorem hlmulass

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

Ref Expression
Hypotheses hlmulf.1 ⊢ X = BaseSet ⁡ U
hlmulf.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion hlmulass ⊢ U ∈ CHil OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S B S C

Proof

Step Hyp Ref Expression
1 hlmulf.1 ⊢ X = BaseSet ⁡ U
2 hlmulf.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 hlnv ⊢ U ∈ CHil OLD → U ∈ NrmCVec
4 1 2 nvsass ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S B S C
5 3 4 sylan ⊢ U ∈ CHil OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S B S C