Axiom ax-hvmulass 30979

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 10999	. . . 4 class ℂ
3	1, 2	wcel 2111	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2111	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30891	. . . 4 class ℋ
8	6, 7	wcel 2111	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11006	. . . . 5 class ·
11	1, 4, 10	co 7341	. . . 4 class (𝐴 · 𝐵)
12		csm 30893	. . . 4 class ·ℎ
13	11, 6, 12	co 7341	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7341	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7341	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1541	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  30996  hvmul0or  30997  hvm1neg  31004  hvmulcom  31015  hvmulassi  31018  hvsubdistr2  31022  hilvc  31134  hhssnv  31236  h1de2bi  31526  spansncol  31540  h1datomi  31553  mayete3i  31700  homulass  31774  kbmul  31927  kbass5  32092  strlem1  32222