Axiom ax-hvmulass 30938

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 10995	. . . 4 class ℂ
3	1, 2	wcel 2109	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2109	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30850	. . . 4 class ℋ
8	6, 7	wcel 2109	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11002	. . . . 5 class ·
11	1, 4, 10	co 7340	. . . 4 class (𝐴 · 𝐵)
12		csm 30852	. . . 4 class ·ℎ
13	11, 6, 12	co 7340	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7340	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7340	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1540	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  30955  hvmul0or  30956  hvm1neg  30963  hvmulcom  30974  hvmulassi  30977  hvsubdistr2  30981  hilvc  31093  hhssnv  31195  h1de2bi  31485  spansncol  31499  h1datomi  31512  mayete3i  31659  homulass  31733  kbmul  31886  kbass5  32051  strlem1  32181