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	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
4	3	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
5		eqid	⊢ ( +_𝑣 ‘ 𝑈 ) = ( +_𝑣 ‘ 𝑈 )
6	5	vafval	⊢ ( +_𝑣 ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
7	2	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
8	1 5	bafval	⊢ 𝑋 = ran ( +_𝑣 ‘ 𝑈 )
9	6 7 8	vcass	⊢ ( ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) )
10	4 9	sylan	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) )