Axiom ax-hvmulass 28790

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 10524	. . . 4 class ℂ
3	1, 2	wcel 2111	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2111	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 28702	. . . 4 class ℋ
8	6, 7	wcel 2111	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1084	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 10531	. . . . 5 class ·
11	1, 4, 10	co 7135	. . . 4 class (𝐴 · 𝐵)
12		csm 28704	. . . 4 class ·ℎ
13	11, 6, 12	co 7135	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7135	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7135	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1538	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  28807  hvmul0or  28808  hvm1neg  28815  hvmulcom  28826  hvmulassi  28829  hvsubdistr2  28833  hilvc  28945  hhssnv  29047  h1de2bi  29337  spansncol  29351  h1datomi  29364  mayete3i  29511  homulass  29585  kbmul  29738  kbass5  29903  strlem1  30033