Axiom ax-hvmulass 31035

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 11150	. . . 4 class ℂ
3	1, 2	wcel 2105	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2105	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30947	. . . 4 class ℋ
8	6, 7	wcel 2105	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11157	. . . . 5 class ·
11	1, 4, 10	co 7430	. . . 4 class (𝐴 · 𝐵)
12		csm 30949	. . . 4 class ·ℎ
13	11, 6, 12	co 7430	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7430	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7430	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1536	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31052  hvmul0or  31053  hvm1neg  31060  hvmulcom  31071  hvmulassi  31074  hvsubdistr2  31078  hilvc  31190  hhssnv  31292  h1de2bi  31582  spansncol  31596  h1datomi  31609  mayete3i  31756  homulass  31830  kbmul  31983  kbass5  32148  strlem1  32278