Axiom ax-hvmulass 31359

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 11093	. . . 4 class ℂ
3	1, 2	wcel 2143	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2143	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 31271	. . . 4 class ℋ
8	6, 7	wcel 2143	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11100	. . . . 5 class ·
11	1, 4, 10	co 7410	. . . 4 class (𝐴 · 𝐵)
12		csm 31273	. . . 4 class ·ℎ
13	11, 6, 12	co 7410	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7410	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7410	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1570	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31376  hvmul0or  31377  hvm1neg  31384  hvmulcom  31395  hvmulassi  31398  hvsubdistr2  31402  hilvc  31514  hhssnv  31616  h1de2bi  31906  spansncol  31920  h1datomi  31933  mayete3i  32080  homulass  32154  kbmul  32307  kbass5  32472  strlem1  32602