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 ⊢ X = BaseSet ⁡ U
nvscl.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion nvscom ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A S B S C = B S A S C

Proof

Step Hyp Ref Expression
1 nvscl.1 ⊢ X = BaseSet ⁡ U
2 nvscl.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
4 3 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B S C = B ⁢ A S C
5 4 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = B ⁢ A S C
6 5 adantl ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = B ⁢ A S C
7 1 2 nvsass ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S B S C
8 3ancoma ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X ↔ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ X
9 1 2 nvsass ⊢ U ∈ NrmCVec ∧ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ X → B ⁢ A S C = B S A S C
10 8 9 sylan2b ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → B ⁢ A S C = B S A S C
11 6 7 10 3eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A S B S C = B S A S C