Axiom ax-hvmulass 30970

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 11026	. . . 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 30882	. . . 4 class ℋ
8	6, 7	wcel 2109	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1086	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11033	. . . . 5 class ·
11	1, 4, 10	co 7353	. . . 4 class (𝐴 · 𝐵)
12		csm 30884	. . . 4 class ·ℎ
13	11, 6, 12	co 7353	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7353	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7353	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1540	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  30987  hvmul0or  30988  hvm1neg  30995  hvmulcom  31006  hvmulassi  31009  hvsubdistr2  31013  hilvc  31125  hhssnv  31227  h1de2bi  31517  spansncol  31531  h1datomi  31544  mayete3i  31691  homulass  31765  kbmul  31918  kbass5  32083  strlem1  32213