Axiom ax-hvmulass 28204

Description: Scalar multiplication associative law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hvmulass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

Detailed syntax breakdown of Axiom ax-hvmulass

Step	Hyp	Ref	Expression
1		cA	. . . 4 class 𝐴
2		cc 10136	. . . 4 class ℂ
3	1, 2	wcel 2145	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2145	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chil 28116	. . . 4 class ℋ
8	6, 7	wcel 2145	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1071	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 10143	. . . . 5 class ·
11	1, 4, 10	co 6793	. . . 4 class (𝐴 · 𝐵)
12		csm 28118	. . . 4 class ·ℎ
13	11, 6, 12	co 6793	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 6793	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 6793	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1631	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  28221  hvmul0or  28222  hvm1neg  28229  hvmulcom  28240  hvmulassi  28243  hvsubdistr2  28247  hilvc  28359  hhssnv  28461  h1de2bi  28753  spansncol  28767  h1datomi  28780  mayete3i  28927  homulass  29001  kbmul  29154  kbass5  29319  strlem1  29449