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 
|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A x. B ) .h C ) = ( A .h ( B .h C ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cc 
 |-  CC
2 0 1 wcel 
 |-  A e. CC
3 cB 
 |-  B
4 3 1 wcel 
 |-  B e. CC
5 cC 
 |-  C
6 chba 
 |-  ~H
7 5 6 wcel 
 |-  C e. ~H
8 2 4 7 w3a 
 |-  ( A e. CC /\ B e. CC /\ C e. ~H )
9 cmul 
 |-  x.
10 0 3 9 co 
 |-  ( A x. B )
11 csm 
 |-  .h
12 10 5 11 co 
 |-  ( ( A x. B ) .h C )
13 3 5 11 co 
 |-  ( B .h C )
14 0 13 11 co 
 |-  ( A .h ( B .h C ) )
15 12 14 wceq 
 |-  ( ( A x. B ) .h C ) = ( A .h ( B .h C ) )
16 8 15 wi 
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A x. B ) .h C ) = ( A .h ( B .h C ) ) )