Metamath Proof Explorer

Theorem hvmulcom

Description: Scalar multiplication commutative law. (Contributed by NM, 19-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hvmulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ B ⋅ ℎ C = B ⋅ ℎ A ⋅ ℎ C

Proof

Step Hyp Ref Expression
1 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
2 1 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ⋅ ℎ C = B ⁢ A ⋅ ℎ C
3 2 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⁢ B ⋅ ℎ C = B ⁢ A ⋅ ℎ C
4 ax-hvmulass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⁢ B ⋅ ℎ C = A ⋅ ℎ B ⋅ ℎ C
5 ax-hvmulass ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℋ → B ⁢ A ⋅ ℎ C = B ⋅ ℎ A ⋅ ℎ C
6 5 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → B ⁢ A ⋅ ℎ C = B ⋅ ℎ A ⋅ ℎ C
7 3 4 6 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ B ⋅ ℎ C = B ⋅ ℎ A ⋅ ℎ C