Axiom ax-hvmul0 30251

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

Assertion

Ref	Expression
ax-hvmul0	⊢ (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)

Detailed syntax breakdown of Axiom ax-hvmul0

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		chba 30160	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		cc0 11107	. . . 4 class 0
5		csm 30162	. . . 4 class ·ℎ
6	4, 1, 5	co 7406	. . 3 class (0 ·ℎ 𝐴)
7		c0v 30165	. . 3 class 0ℎ
8	6, 7	wceq 1542	. 2 wff (0 ·ℎ 𝐴) = 0ℎ
9	3, 8	wi 4	1 wff (𝐴 ∈ ℋ → (0 ·ℎ 𝐴) = 0ℎ)

This axiom is referenced by:  hvmul0  30265  hvmul0or  30266  hvsubid  30267  hi01  30337  h1de2ctlem  30796  spansneleq  30811  h1datomi  30822