Axiom ax-hvmulass 8862

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 5224	. . . 4 class CC
3	1, 2	wcel 958	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 958	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 8773	. . . 4 class H~
8	6, 7	wcel 958	. . 3 wff C e. H~
9	3, 5, 8	w3a 775	. 2 wff (A e. CC /\ B e. CC /\ C e. H~)
10		cmul 5231	. . . . 5 class x.
11	1, 4, 10	co 3963	. . . 4 class (A x. B)
12		csm 8775	. . . 4 class .h
13	11, 6, 12	co 3963	. . 3 class ((A x. B) .h C)
14	4, 6, 12	co 3963	. . . 4 class (B .h C)
15	1, 14, 12	co 3963	. . 3 class (A .h (B .h C))
16	13, 15	wceq 956	. 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:  hvmul0t 8878  hvmul0ort 8879  hvm1negt 8886  hvmulcomt 8897  hvmulass 8898  hvsubdistr2t 8902  hilvc 9014  hhssnv 9119  h1de2b 9462  spansncol 9476  h1datom 9489  mayete3 9658  homulasst 9713  kbmult 9864  kbass5t 10038  strlem1 10162

Copyright terms: Public domain