Axiom ax-hvmulass 31621

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 11208	. . . 4 class ℂ
3	1, 2	wcel 2146	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2146	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 31533	. . . 4 class ℋ
8	6, 7	wcel 2146	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11215	. . . . 5 class ·
11	1, 4, 10	co 7427	. . . 4 class (𝐴 · 𝐵)
12		csm 31535	. . . 4 class ·ℎ
13	11, 6, 12	co 7427	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7427	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7427	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1569	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is used by:  hvmul0  31638  hvmul0or  31639  hvm1neg  31646  hvmulcom  31657  hvmulassi  31660  hvsubdistr2  31664  hilvc  31776  hhssnv  31878  h1de2bi  32168  spansncol  32182  h1datomi  32195  mayete3i  32342  homulass  32416  kbmul  32569  kbass5  32734  strlem1  32864