Axiom ax-hvmulass 29270

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 10800	. . . 4 class ℂ
3	1, 2	wcel 2108	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2108	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 29182	. . . 4 class ℋ
8	6, 7	wcel 2108	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1085	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 10807	. . . . 5 class ·
11	1, 4, 10	co 7255	. . . 4 class (𝐴 · 𝐵)
12		csm 29184	. . . 4 class ·ℎ
13	11, 6, 12	co 7255	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7255	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7255	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1539	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  29287  hvmul0or  29288  hvm1neg  29295  hvmulcom  29306  hvmulassi  29309  hvsubdistr2  29313  hilvc  29425  hhssnv  29527  h1de2bi  29817  spansncol  29831  h1datomi  29844  mayete3i  29991  homulass  30065  kbmul  30218  kbass5  30383  strlem1  30513