Axiom ax-hvmulass 31602

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 11191	. . . 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		chba 31514	. . . 4 class ℋ
8	6, 7	wcel 2145	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11198	. . . . 5 class ·
11	1, 4, 10	co 7418	. . . 4 class (𝐴 · 𝐵)
12		csm 31516	. . . 4 class ·ℎ
13	11, 6, 12	co 7418	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7418	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7418	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1570	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is used by:  hvmul0  31619  hvmul0or  31620  hvm1neg  31627  hvmulcom  31638  hvmulassi  31641  hvsubdistr2  31645  hilvc  31757  hhssnv  31859  h1de2bi  32149  spansncol  32163  h1datomi  32176  mayete3i  32323  homulass  32397  kbmul  32550  kbass5  32715  strlem1  32845