Axiom ax-hvmul0 8819

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

Assertion

Ref	Expression
ax-hvmul0	|- (A e. H~ -> (0 .h A) = 0h)

Detailed syntax breakdown of Axiom ax-hvmul0

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 8727	. . 3 class H~
3	1, 2	wcel 956	. 2 wff A e. H~
4		cc0 5214	. . . 4 class 0
5		csm 8729	. . . 4 class .h
6	4, 1, 5	co 3954	. . 3 class (0 .h A)
7		c0v 8730	. . 3 class 0h
8	6, 7	wceq 954	. 2 wff (0 .h A) = 0h
9	3, 8	wi 3	1 wff (A e. H~ -> (0 .h A) = 0h)

This axiom is referenced by:  hvmul0t 8832  hvmul0ort 8833  hvsubidt 8834  hi01t 8901  h1de2ctlem 9417  spansneleq 9432  spansneleqOLD 9433  h1datom 9444

Copyright terms: Public domain