Axiom ax-hvmulass 30909

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 11042	. . . 4 class ℂ
3	1, 2	wcel 2109	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2109	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30821	. . . 4 class ℋ
8	6, 7	wcel 2109	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11049	. . . . 5 class ·
11	1, 4, 10	co 7369	. . . 4 class (𝐴 · 𝐵)
12		csm 30823	. . . 4 class ·ℎ
13	11, 6, 12	co 7369	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7369	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7369	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1540	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  30926  hvmul0or  30927  hvm1neg  30934  hvmulcom  30945  hvmulassi  30948  hvsubdistr2  30952  hilvc  31064  hhssnv  31166  h1de2bi  31456  spansncol  31470  h1datomi  31483  mayete3i  31630  homulass  31704  kbmul  31857  kbass5  32022  strlem1  32152