Axiom ax-hvmulass 8872

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 5244	. . . 4 class CC
3	1, 2	wcel 960	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 960	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 8783	. . . 4 class H~
8	6, 7	wcel 960	. . 3 wff C e. H~
9	3, 5, 8	w3a 777	. 2 wff (A e. CC /\ B e. CC /\ C e. H~)
10		cmul 5251	. . . . 5 class x.
11	1, 4, 10	co 3969	. . . 4 class (A x. B)
12		csm 8785	. . . 4 class .h
13	11, 6, 12	co 3969	. . 3 class ((A x. B) .h C)
14	4, 6, 12	co 3969	. . . 4 class (B .h C)
15	1, 14, 12	co 3969	. . 3 class (A .h (B .h C))
16	13, 15	wceq 958	. 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 8888  hvmul0ort 8889  hvm1negt 8896  hvmulcomt 8907  hvmulass 8908  hvsubdistr2t 8912  hilvc 9024  hhssnv 9129  h1de2b 9472  spansncol 9486  h1datom 9499  mayete3 9668  homulasst 9723  kbmult 9874  kbass5t 10048  strlem1 10172

Copyright terms: Public domain