Axiom ax-hvmulass 10509

Description: Scalar multiplication associative law.

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 6384	. . . 4 class CC
3	1, 2	wcel 1300	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 1300	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 10420	. . . 4 class ~H
8	6, 7	wcel 1300	. . 3 wff C e. ~H
9	3, 5, 8	w3a 858	. 2 wff (A e. CC /\ B e. CC /\ C e. ~H)
10		cmul 6391	. . . . 5 class x.
11	1, 4, 10	co 4884	. . . 4 class (A x. B)
12		csm 10422	. . . 4 class .h
13	11, 6, 12	co 4884	. . 3 class ((A x. B) .h C)
14	4, 6, 12	co 4884	. . . 4 class (B .h C)
15	1, 14, 12	co 4884	. . 3 class (A .h (B .h C))
16	13, 15	wceq 1298	. 2 wff ((A x. B) .h C) = (A .h (B .h C))
17	9, 16	wi 3	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 10525  hvmul0or 10526  hvm1neg 10533  hvmulcom 10544  hvmulassi 10545  hvsubdistr2 10549  hilvc 10662  hhssnv 10767  h1de2bi 11110  spansncol 11124  h1datomi 11137  mayete3i 11308  mayete3OLDi 11309  homulass 11365  kbmul 11516  kbass5 11691  strlem1 11822

Copyright terms: Public domain