Axiom ax-hvmulass 31078

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 11036	. . . 4 class ℂ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2114	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30990	. . . 4 class ℋ
8	6, 7	wcel 2114	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11043	. . . . 5 class ·
11	1, 4, 10	co 7367	. . . 4 class (𝐴 · 𝐵)
12		csm 30992	. . . 4 class ·ℎ
13	11, 6, 12	co 7367	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7367	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7367	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1542	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31095  hvmul0or  31096  hvm1neg  31103  hvmulcom  31114  hvmulassi  31117  hvsubdistr2  31121  hilvc  31233  hhssnv  31335  h1de2bi  31625  spansncol  31639  h1datomi  31652  mayete3i  31799  homulass  31873  kbmul  32026  kbass5  32191  strlem1  32321