Axiom ax-hvmulzer 4995

Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubidt 5005 and hvsubvalt 4997).

Assertion

Ref	Expression
ax-hvmulzer	⊢ (A ∈ ℋ → (0 ·s A) = 0v)

Detailed syntax breakdown of Axiom ax-hvmulzer

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 4958	. . 3 class ℋ
3	1, 2	wcel 1092	. 2 wff A ∈ ℋ
4		cc0 4028	. . . 4 class 0
5		csm 4960	. . . 4 class ·s
6	4, 1, 5	co 3001	. . 3 class (0 ·s A)
7		c0v 4961	. . 3 class 0v
8	6, 7	wceq 1091	. 2 wff (0 ·s A) = 0v
9	3, 8	wi 2	1 wff (A ∈ ℋ → (0 ·s A) = 0v)

This axiom is referenced by:  hvmul0t 5004  hvsubidt 5005  hizer1t 5054  h1de2ctlem 5460  spansneleq 5475  h1datom 5483

metamath.org