# Metamath Proof Explorer

## Axiom ax-hvmulass

Description: Scalar multiplication associative law. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-hvmulass ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to {A}{B}{\cdot }_{ℎ}{C}={A}{\cdot }_{ℎ}\left({B}{\cdot }_{ℎ}{C}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cc ${class}ℂ$
2 0 1 wcel ${wff}{A}\in ℂ$
3 cB ${class}{B}$
4 3 1 wcel ${wff}{B}\in ℂ$
5 cC ${class}{C}$
6 chba ${class}ℋ$
7 5 6 wcel ${wff}{C}\in ℋ$
8 2 4 7 w3a ${wff}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)$
9 cmul ${class}×$
10 0 3 9 co ${class}{A}{B}$
11 csm ${class}{\cdot }_{ℎ}$
12 10 5 11 co ${class}\left({A}{B}{\cdot }_{ℎ}{C}\right)$
13 3 5 11 co ${class}\left({B}{\cdot }_{ℎ}{C}\right)$
14 0 13 11 co ${class}\left({A}{\cdot }_{ℎ}\left({B}{\cdot }_{ℎ}{C}\right)\right)$
15 12 14 wceq ${wff}{A}{B}{\cdot }_{ℎ}{C}={A}{\cdot }_{ℎ}\left({B}{\cdot }_{ℎ}{C}\right)$
16 8 15 wi ${wff}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to {A}{B}{\cdot }_{ℎ}{C}={A}{\cdot }_{ℎ}\left({B}{\cdot }_{ℎ}{C}\right)\right)$