Axiom ax-hvmulass 4992

Description: Scalar multiplication associative law

Assertion

Ref	Expression
ax-hvmulass	⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ) → ((A · B) ·s C) = (A ·s (B ·s C)))

Detailed syntax breakdown of Axiom ax-hvmulass

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cc 4026	. . . 4 class ℂ
3	1, 2	wcel 1092	. . 3 wff A ∈ ℂ
4		cB	. . . 4 class B
5	4, 2	wcel 1092	. . 3 wff B ∈ ℂ
6		cC	. . . 4 class C
7		chil 4958	. . . 4 class ℋ
8	6, 7	wcel 1092	. . 3 wff C ∈ ℋ
9	3, 5, 8	w3a 581	. 2 wff (A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ )
10		cmulc 4032	. . . . 5 class ·
11	1, 4, 10	co 3001	. . . 4 class (A · B)
12		csm 4960	. . . 4 class ·s
13	11, 6, 12	co 3001	. . 3 class ((A · B) ·s C)
14	4, 6, 12	co 3001	. . . 4 class (B ·s C)
15	1, 14, 12	co 3001	. . 3 class (A ·s (B ·s C))
16	13, 15	wceq 1091	. 2 wff ((A · B) ·s C) = (A ·s (B ·s C))
17	9, 16	wi 2	1 wff ((A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ) → ((A · B) ·s C) = (A ·s (B ·s C)))

This axiom is referenced by:  hvmul0t 5004  hvm1negt 5007  hvmulass 5020  h1de2b 5459  spansncol 5473  h1datom 5483  strlem1 5691

metamath.org