Axiom ax-hvmulass 31008

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 11015	. . . 4 class ℂ
3	1, 2	wcel 2113	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2113	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30920	. . . 4 class ℋ
8	6, 7	wcel 2113	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11022	. . . . 5 class ·
11	1, 4, 10	co 7355	. . . 4 class (𝐴 · 𝐵)
12		csm 30922	. . . 4 class ·ℎ
13	11, 6, 12	co 7355	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7355	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7355	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1541	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31025  hvmul0or  31026  hvm1neg  31033  hvmulcom  31044  hvmulassi  31047  hvsubdistr2  31051  hilvc  31163  hhssnv  31265  h1de2bi  31555  spansncol  31569  h1datomi  31582  mayete3i  31729  homulass  31803  kbmul  31956  kbass5  32121  strlem1  32251