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โ„Ž )