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 𝑋 = ( BaseSet ‘ 𝑈 )
nvscl.4 𝑆 = ( ·𝑠OLD𝑈 )
Assertion nvsass ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶𝑋 ) ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nvscl.1 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvscl.4 𝑆 = ( ·𝑠OLD𝑈 )
3 eqid ( 1st𝑈 ) = ( 1st𝑈 )
4 3 nvvc ( 𝑈 ∈ NrmCVec → ( 1st𝑈 ) ∈ CVecOLD )
5 eqid ( +𝑣𝑈 ) = ( +𝑣𝑈 )
6 5 vafval ( +𝑣𝑈 ) = ( 1st ‘ ( 1st𝑈 ) )
7 2 smfval 𝑆 = ( 2nd ‘ ( 1st𝑈 ) )
8 1 5 bafval 𝑋 = ran ( +𝑣𝑈 )
9 6 7 8 vcass ( ( ( 1st𝑈 ) ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶𝑋 ) ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) )
10 4 9 sylan ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶𝑋 ) ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) )