Axiom ax-hvmulass 30123

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 11090	. . . 4 class ℂ
3	1, 2	wcel 2106	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2106	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30035	. . . 4 class ℋ
8	6, 7	wcel 2106	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11097	. . . . 5 class ·
11	1, 4, 10	co 7393	. . . 4 class (𝐴 · 𝐵)
12		csm 30037	. . . 4 class ·ℎ
13	11, 6, 12	co 7393	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7393	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7393	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1541	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  30140  hvmul0or  30141  hvm1neg  30148  hvmulcom  30159  hvmulassi  30162  hvsubdistr2  30166  hilvc  30278  hhssnv  30380  h1de2bi  30670  spansncol  30684  h1datomi  30697  mayete3i  30844  homulass  30918  kbmul  31071  kbass5  31236  strlem1  31366