Axiom ax-hvmulass 31430

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 11113	. . . 4 class ℂ
3	1, 2	wcel 2146	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2146	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 31342	. . . 4 class ℋ
8	6, 7	wcel 2146	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1103	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11120	. . . . 5 class ·
11	1, 4, 10	co 7419	. . . 4 class (𝐴 · 𝐵)
12		csm 31344	. . . 4 class ·ℎ
13	11, 6, 12	co 7419	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7419	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7419	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1570	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is used by:  hvmul0  31447  hvmul0or  31448  hvm1neg  31455  hvmulcom  31466  hvmulassi  31469  hvsubdistr2  31473  hilvc  31585  hhssnv  31687  h1de2bi  31977  spansncol  31991  h1datomi  32004  mayete3i  32151  homulass  32225  kbmul  32378  kbass5  32543  strlem1  32673