Axiom ax-hvmulass 11347

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 6750	. . . 4 class CC
3	1, 2	wcel 1588	. . 3 wff A e. CC
4		cB	. . . 4 class B
5	4, 2	wcel 1588	. . 3 wff B e. CC
6		cC	. . . 4 class C
7		chil 11258	. . . 4 class ~H
8	6, 7	wcel 1588	. . 3 wff C e. ~H
9	3, 5, 8	w3a 1102	. 2 wff (A e. CC /\ B e. CC /\ C e. ~H)
10		cmul 6757	. . . . 5 class x.
11	1, 4, 10	co 4981	. . . 4 class (A x. B)
12		csm 11260	. . . 4 class .h
13	11, 6, 12	co 4981	. . 3 class ((A x. B) .h C)
14	4, 6, 12	co 4981	. . . 4 class (B .h C)
15	1, 14, 12	co 4981	. . 3 class (A .h (B .h C))
16	13, 15	wceq 1586	. 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 11363  hvmul0or 11364  hvm1neg 11371  hvmulcom 11382  hvmulassi 11383  hvsubdistr2 11387  hilvc 11498  hhssnv 11601  h1de2bi 11944  spansncol 11958  h1datomi 11971  mayete3i 12140  mayete3OLDi 12141  homulass 12197  kbmul 12348  kbass5 12522  strlem1 12653

Copyright terms: Public domain