Axiom ax-hvmulass 28436

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 10270	. . . 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 28348	. . . 4 class ℋ
8	6, 7	wcel 2107	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1071	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 10277	. . . . 5 class ·
11	1, 4, 10	co 6922	. . . 4 class (𝐴 · 𝐵)
12		csm 28350	. . . 4 class ·ℎ
13	11, 6, 12	co 6922	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 6922	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 6922	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1601	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  28453  hvmul0or  28454  hvm1neg  28461  hvmulcom  28472  hvmulassi  28475  hvsubdistr2  28479  hilvc  28591  hhssnv  28693  h1de2bi  28985  spansncol  28999  h1datomi  29012  mayete3i  29159  homulass  29233  kbmul  29386  kbass5  29551  strlem1  29681