Axiom ax-hvmul0 27867

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

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 27776	. . 3 class ~H
3	1, 2	wcel 1990	. 2 wff A e. ~H
4		cc0 9936	. . . 4 class 0
5		csm 27778	. . . 4 class .h
6	4, 1, 5	co 6650	. . 3 class ( 0 .h A )
7		c0v 27781	. . 3 class 0h
8	6, 7	wceq 1483	. 2 wff ( 0 .h A ) = 0h
9	3, 8	wi 4	1 wff ( A e. ~H -> ( 0 .h A ) = 0h )

This axiom is referenced by:  hvmul0  27881  hvmul0or  27882  hvsubid  27883  hi01  27953  h1de2ctlem  28414  spansneleq  28429  h1datomi  28440