Axiom ax-hvmulass 31207

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 11071	. . . 4 class ℂ
3	1, 2	wcel 2142	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2142	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 31119	. . . 4 class ℋ
8	6, 7	wcel 2142	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1098	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11078	. . . . 5 class ·
11	1, 4, 10	co 7396	. . . 4 class (𝐴 · 𝐵)
12		csm 31121	. . . 4 class ·ℎ
13	11, 6, 12	co 7396	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7396	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7396	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1560	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31224  hvmul0or  31225  hvm1neg  31232  hvmulcom  31243  hvmulassi  31246  hvsubdistr2  31250  hilvc  31362  hhssnv  31464  h1de2bi  31754  spansncol  31768  h1datomi  31781  mayete3i  31928  homulass  32002  kbmul  32155  kbass5  32320  strlem1  32450