Axiom ax-hvmulass 9025

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 5155	. . . 4 class CC
3	1, 2	wcel 1105	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 1105	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 8968	. . . 4 class H~
8	6, 7	wcel 1105	. . 3 wff C e. H~
9	3, 5, 8	w3a 772	. 2 wff (A e. CC /\ B e. CC /\ C e. H~)
10		cmul 5162	. . . . 5 class x.
11	1, 4, 10	co 3902	. . . 4 class (A x. B)
12		csm 8970	. . . 4 class .h
13	11, 6, 12	co 3902	. . 3 class ((A x. B) .h C)
14	4, 6, 12	co 3902	. . . 4 class (B .h C)
15	1, 14, 12	co 3902	. . 3 class (A .h (B .h C))
16	13, 15	wceq 1099	. 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 9042  hvmul0ort 9043  hvm1negt 9050  hvmulcomt 9061  hvmulass 9062  hvsubdistr2t 9066  hilvc 9178  h1de2b 9606  h1de2bOLD 9607  spansncol 9621  h1datom 9635  mayete3 9804  homulasst 9859  kbmult 10009  kbass5t 10179  strlem1 10301

Copyright terms: Public domain