Axiom ax-hvmulass 31095

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 11036	. . . 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 31007	. . . 4 class ℋ
8	6, 7	wcel 2114	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11043	. . . . 5 class ·
11	1, 4, 10	co 7368	. . . 4 class (𝐴 · 𝐵)
12		csm 31009	. . . 4 class ·ℎ
13	11, 6, 12	co 7368	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7368	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7368	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1542	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31112  hvmul0or  31113  hvm1neg  31120  hvmulcom  31131  hvmulassi  31134  hvsubdistr2  31138  hilvc  31250  hhssnv  31352  h1de2bi  31642  spansncol  31656  h1datomi  31669  mayete3i  31816  homulass  31890  kbmul  32043  kbass5  32208  strlem1  32338