Axiom ax-hvmulass 29378

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 10878	. . . 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 29290	. . . 4 class ℋ
8	6, 7	wcel 2107	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 10885	. . . . 5 class ·
11	1, 4, 10	co 7284	. . . 4 class (𝐴 · 𝐵)
12		csm 29292	. . . 4 class ·ℎ
13	11, 6, 12	co 7284	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7284	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7284	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1539	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  29395  hvmul0or  29396  hvm1neg  29403  hvmulcom  29414  hvmulassi  29417  hvsubdistr2  29421  hilvc  29533  hhssnv  29635  h1de2bi  29925  spansncol  29939  h1datomi  29952  mayete3i  30099  homulass  30173  kbmul  30326  kbass5  30491  strlem1  30621