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

Metamath Proof Explorer

Theorem nvsass

Description: Associative law for the scalar product of a normed complex vector space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nvscl.1 ⊢ X = BaseSet ⁡ U
2 nvscl.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 eqid ⊢ 1 st ⁡ U = 1 st ⁡ U
4 3 nvvc ⊢ U ∈ NrmCVec → 1 st ⁡ U ∈ CVec OLD
5 eqid ⊢ + v ⁡ U = + v ⁡ U
6 5 vafval ⊢ + v ⁡ U = 1 st ⁡ 1 st ⁡ U
7 2 smfval ⊢ S = 2 nd ⁡ 1 st ⁡ U
8 1 5 bafval ⊢ X = ran ⁡ + v ⁡ U
9 6 7 8 vcass ⊢ 1 st ⁡ U ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S B S C
10 4 9 sylan ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S B S C