Axiom ax-hvmulass 31299

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 11097	. . . 4 class ℂ
3	1, 2	wcel 2149	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2149	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 31211	. . . 4 class ℋ
8	6, 7	wcel 2149	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1101	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11104	. . . . 5 class ·
11	1, 4, 10	co 7411	. . . 4 class (𝐴 · 𝐵)
12		csm 31213	. . . 4 class ·ℎ
13	11, 6, 12	co 7411	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7411	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7411	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1567	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31316  hvmul0or  31317  hvm1neg  31324  hvmulcom  31335  hvmulassi  31338  hvsubdistr2  31342  hilvc  31454  hhssnv  31556  h1de2bi  31846  spansncol  31860  h1datomi  31873  mayete3i  32020  homulass  32094  kbmul  32247  kbass5  32412  strlem1  32542