This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℋ \to 0 \cdot_{ℎ} A = 0_{ℎ}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		chba	$class ℋ$
2	0 1	wcel	$wff A \in ℋ$
3		cc0	$class 0$
4		csm	$class \cdot_{ℎ}$
5	3 0 4	co	$class (0 \cdot_{ℎ} A)$
6		c0v	$class 0_{ℎ}$
7	5 6	wceq	$wff 0 \cdot_{ℎ} A = 0_{ℎ}$
8	2 7	wi	$wff (A \in ℋ \to 0 \cdot_{ℎ} A = 0_{ℎ})$