Axiom ax-hvmulass 27248

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 9813	. . . 4 class ℂ
3	1, 2	wcel 1977	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 1977	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chil 27160	. . . 4 class ℋ
8	6, 7	wcel 1977	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1031	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 9820	. . . . 5 class ·
11	1, 4, 10	co 6549	. . . 4 class (𝐴 · 𝐵)
12		csm 27162	. . . 4 class ·ℎ
13	11, 6, 12	co 6549	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 6549	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 6549	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1475	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  27265  hvmul0or  27266  hvm1neg  27273  hvmulcom  27284  hvmulassi  27287  hvsubdistr2  27291  hilvc  27403  hhssnv  27505  h1de2bi  27797  spansncol  27811  h1datomi  27824  mayete3i  27971  homulass  28045  kbmul  28198  kbass5  28363  strlem1  28493