Axiom ax-hvmulass 8798

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 5204	. . . 4 class CC
3	1, 2	wcel 955	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 955	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 8727	. . . 4 class H~
8	6, 7	wcel 955	. . 3 wff C e. H~
9	3, 5, 8	w3a 773	. 2 wff (A e. CC /\ B e. CC /\ C e. H~)
10		cmul 5211	. . . . 5 class x.
11	1, 4, 10	co 3948	. . . 4 class (A x. B)
12		csm 8729	. . . 4 class .h
13	11, 6, 12	co 3948	. . 3 class ((A x. B) .h C)
14	4, 6, 12	co 3948	. . . 4 class (B .h C)
15	1, 14, 12	co 3948	. . 3 class (A .h (B .h C))
16	13, 15	wceq 953	. 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 8814  hvmul0ort 8815  hvm1negt 8822  hvmulcomt 8833  hvmulass 8834  hvsubdistr2t 8838  hilvc 8950  hhssnv 9054  h1de2b 9392  h1de2bOLD 9393  spansncol 9407  h1datom 9421  mayete3 9590  homulasst 9645  kbmult 9795  kbass5t 9965  strlem1 10087

Copyright terms: Public domain