Axiom ax-hvmulass 31666

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

This axiom is used by:  hvmul0  31683  hvmul0or  31684  hvm1neg  31691  hvmulcom  31702  hvmulassi  31705  hvsubdistr2  31709  hilvc  31821  hhssnv  31923  h1de2bi  32213  spansncol  32227  h1datomi  32240  mayete3i  32387  homulass  32461  kbmul  32614  kbass5  32779  strlem1  32909