Axiom ax-hvmulass 31082

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 11024	. . . 4 class ℂ
3	1, 2	wcel 2113	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2113	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30994	. . . 4 class ℋ
8	6, 7	wcel 2113	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11031	. . . . 5 class ·
11	1, 4, 10	co 7358	. . . 4 class (𝐴 · 𝐵)
12		csm 30996	. . . 4 class ·ℎ
13	11, 6, 12	co 7358	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7358	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7358	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1541	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31099  hvmul0or  31100  hvm1neg  31107  hvmulcom  31118  hvmulassi  31121  hvsubdistr2  31125  hilvc  31237  hhssnv  31339  h1de2bi  31629  spansncol  31643  h1datomi  31656  mayete3i  31803  homulass  31877  kbmul  32030  kbass5  32195  strlem1  32325