Axiom ax-hvmulass 9152

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 5386	. . . 4 class CC
3	1, 2	wcel 994	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 994	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 9063	. . . 4 class H~
8	6, 7	wcel 994	. . 3 wff C e. H~
9	3, 5, 8	w3a 781	. 2 wff (A e. CC /\ B e. CC /\ C e. H~)
10		cmul 5393	. . . . 5 class x.
11	1, 4, 10	co 4021	. . . 4 class (A x. B)
12		csm 9065	. . . 4 class .h
13	11, 6, 12	co 4021	. . 3 class ((A x. B) .h C)
14	4, 6, 12	co 4021	. . . 4 class (B .h C)
15	1, 14, 12	co 4021	. . 3 class (A .h (B .h C))
16	13, 15	wceq 992	. 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 9168  hvmul0or 9169  hvm1neg 9176  hvmulcom 9187  hvmulassi 9188  hvsubdistr2 9192  hilvc 9305  hhssnv 9410  h1de2bi 9753  spansncol 9767  h1datomi 9780  mayete3i 9951  mayete3OLDi 9952  homulass 10008  kbmul 10159  kbass5 10333  strlem1 10458

Copyright terms: Public domain