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	⊢ ( 𝐴 ∈ ℋ → ( 0 ·_ℎ 𝐴 ) = 0_ℎ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		chba	⊢ ℋ
2	0 1	wcel	⊢ 𝐴 ∈ ℋ
3		cc0	⊢ 0
4		csm	⊢ ·_ℎ
5	3 0 4	co	⊢ ( 0 ·_ℎ 𝐴 )
6		c0v	⊢ 0_ℎ
7	5 6	wceq	⊢ ( 0 ·_ℎ 𝐴 ) = 0_ℎ
8	2 7	wi	⊢ ( 𝐴 ∈ ℋ → ( 0 ·_ℎ 𝐴 ) = 0_ℎ )