Theorem nvscom

Description: Commutative law for the scalar product of a normed complex vector space. (Contributed by NM, 14-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvscl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvscl.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
Assertion	nvscom	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) = ( 𝐵 𝑆 ( 𝐴 𝑆 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nvscl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvscl.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
4	3	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐵 · 𝐴 ) 𝑆 𝐶 ) )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐵 · 𝐴 ) 𝑆 𝐶 ) )
6	5	adantl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐵 · 𝐴 ) 𝑆 𝐶 ) )
7	1 2	nvsass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 · 𝐵 ) 𝑆 𝐶 ) = ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) )
8		3ancoma	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) )
9	1 2	nvsass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐵 · 𝐴 ) 𝑆 𝐶 ) = ( 𝐵 𝑆 ( 𝐴 𝑆 𝐶 ) ) )
10	8 9	sylan2b	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐵 · 𝐴 ) 𝑆 𝐶 ) = ( 𝐵 𝑆 ( 𝐴 𝑆 𝐶 ) ) )
11	6 7 10	3eqtr3d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) = ( 𝐵 𝑆 ( 𝐴 𝑆 𝐶 ) ) )