Axiom ax-hvmulass 31096

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 11030	. . . 4 class ℂ
3	1, 2	wcel 2114	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2114	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 31008	. . . 4 class ℋ
8	6, 7	wcel 2114	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1087	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11037	. . . . 5 class ·
11	1, 4, 10	co 7361	. . . 4 class (𝐴 · 𝐵)
12		csm 31010	. . . 4 class ·ℎ
13	11, 6, 12	co 7361	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7361	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7361	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1542	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  31113  hvmul0or  31114  hvm1neg  31121  hvmulcom  31132  hvmulassi  31135  hvsubdistr2  31139  hilvc  31251  hhssnv  31353  h1de2bi  31643  spansncol  31657  h1datomi  31670  mayete3i  31817  homulass  31891  kbmul  32044  kbass5  32209  strlem1  32339