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