Axiom ax-hvmulass 31026

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 11153	. . . 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 30938	. . . 4 class ℋ
8	6, 7	wcel 2108	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11160	. . . . 5 class ·
11	1, 4, 10	co 7431	. . . 4 class (𝐴 · 𝐵)
12		csm 30940	. . . 4 class ·ℎ
13	11, 6, 12	co 7431	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7431	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7431	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1540	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31043  hvmul0or  31044  hvm1neg  31051  hvmulcom  31062  hvmulassi  31065  hvsubdistr2  31069  hilvc  31181  hhssnv  31283  h1de2bi  31573  spansncol  31587  h1datomi  31600  mayete3i  31747  homulass  31821  kbmul  31974  kbass5  32139  strlem1  32269