Axiom ax-hvmulass 30248

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 11105	. . . 4 class ℂ
3	1, 2	wcel 2107	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2107	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30160	. . . 4 class ℋ
8	6, 7	wcel 2107	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1088	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11112	. . . . 5 class ·
11	1, 4, 10	co 7406	. . . 4 class (𝐴 · 𝐵)
12		csm 30162	. . . 4 class ·ℎ
13	11, 6, 12	co 7406	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7406	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7406	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1542	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  30265  hvmul0or  30266  hvm1neg  30273  hvmulcom  30284  hvmulassi  30287  hvsubdistr2  30291  hilvc  30403  hhssnv  30505  h1de2bi  30795  spansncol  30809  h1datomi  30822  mayete3i  30969  homulass  31043  kbmul  31196  kbass5  31361  strlem1  31491