Axiom ax-hvmulass 27864

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

Assertion

Ref	Expression
ax-hvmulass	|- ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A x. B ) .h C ) = ( A .h ( B .h C ) ) )

Detailed syntax breakdown of Axiom ax-hvmulass

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 9934	. . . 4 class CC
3	1, 2	wcel 1990	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 1990	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 27776	. . . 4 class ~H
8	6, 7	wcel 1990	. . 3 wff C e. ~H
9	3, 5, 8	w3a 1037	. 2 wff ( A e. CC /\ B e. CC /\ C e. ~H )
10		cmul 9941	. . . . 5 class x.
11	1, 4, 10	co 6650	. . . 4 class ( A x. B )
12		csm 27778	. . . 4 class .h
13	11, 6, 12	co 6650	. . 3 class ( ( A x. B ) .h C )
14	4, 6, 12	co 6650	. . . 4 class ( B .h C )
15	1, 14, 12	co 6650	. . 3 class ( A .h ( B .h C ) )
16	13, 15	wceq 1483	. 2 wff ( ( A x. B ) .h C ) = ( A .h ( B .h C ) )
17	9, 16	wi 4	1 wff ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A x. B ) .h C ) = ( A .h ( B .h C ) ) )

This axiom is referenced by:  hvmul0  27881  hvmul0or  27882  hvm1neg  27889  hvmulcom  27900  hvmulassi  27903  hvsubdistr2  27907  hilvc  28019  hhssnv  28121  h1de2bi  28413  spansncol  28427  h1datomi  28440  mayete3i  28587  homulass  28661  kbmul  28814  kbass5  28979  strlem1  29109