Axiom ax-hvmul0

Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid and hvsubval ). (Contributed by NM, 29-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvmul0	$$⊢A\in \mathscr{H}\to 0{\cdot }_{ℎ}A=0_{ℎ}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		chba	$$class\mathscr{H}$$
2	0 1	wcel	$$wffA\in \mathscr{H}$$
3		cc0	$$class0$$
4		csm	$$class{\cdot }_{ℎ}$$
5	3 0 4	co	$$class\left(0{\cdot }_{ℎ}A\right)$$
6		c0v	$$class{0}_{ℎ}$$
7	5 6	wceq	$$wff0{\cdot }_{ℎ}A=0_{ℎ}$$
8	2 7	wi	$$wff\left(A\in \mathscr{H}\to 0{\cdot }_{ℎ}A=0_{ℎ}\right)$$