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

Metamath Proof Explorer

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 ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑆 ( 𝐵 𝑆 𝐶 ) ) = ( 𝐵 𝑆 ( 𝐴 𝑆 𝐶 ) ) )