Axiom ax-hvmulass 28784

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 10535	. . . 4 class ℂ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2114	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 28696	. . . 4 class ℋ
8	6, 7	wcel 2114	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1083	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 10542	. . . . 5 class ·
11	1, 4, 10	co 7156	. . . 4 class (𝐴 · 𝐵)
12		csm 28698	. . . 4 class ·ℎ
13	11, 6, 12	co 7156	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7156	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7156	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1537	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  28801  hvmul0or  28802  hvm1neg  28809  hvmulcom  28820  hvmulassi  28823  hvsubdistr2  28827  hilvc  28939  hhssnv  29041  h1de2bi  29331  spansncol  29345  h1datomi  29358  mayete3i  29505  homulass  29579  kbmul  29732  kbass5  29897  strlem1  30027