Axiom ax-hvmulass 30729

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 11104	. . . 4 class ℂ
3	1, 2	wcel 2098	. . 3 wff 𝐴 ∈ ℂ
4		cB	. . . 4 class 𝐵
5	4, 2	wcel 2098	. . 3 wff 𝐵 ∈ ℂ
6		cC	. . . 4 class 𝐶
7		chba 30641	. . . 4 class ℋ
8	6, 7	wcel 2098	. . 3 wff 𝐶 ∈ ℋ
9	3, 5, 8	w3a 1084	. 2 wff (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ)
10		cmul 11111	. . . . 5 class ·
11	1, 4, 10	co 7401	. . . 4 class (𝐴 · 𝐵)
12		csm 30643	. . . 4 class ·ℎ
13	11, 6, 12	co 7401	. . 3 class ((𝐴 · 𝐵) ·ℎ 𝐶)
14	4, 6, 12	co 7401	. . . 4 class (𝐵 ·ℎ 𝐶)
15	1, 14, 12	co 7401	. . 3 class (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
16	13, 15	wceq 1533	. 2 wff ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
17	9, 16	wi 4	1 wff ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)))

This axiom is referenced by:  hvmul0  30746  hvmul0or  30747  hvm1neg  30754  hvmulcom  30765  hvmulassi  30768  hvsubdistr2  30772  hilvc  30884  hhssnv  30986  h1de2bi  31276  spansncol  31290  h1datomi  31303  mayete3i  31450  homulass  31524  kbmul  31677  kbass5  31842  strlem1  31972