HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvmul0 Unicode version

Axiom ax-hvmul0 22466
Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 22481 and hvsubval 22472). (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
StepHypRef Expression
1 cA . . 3  class  A
2 chil 22375 . . 3  class  ~H
31, 2wcel 1721 . 2  wff  A  e. 
~H
4 cc0 8946 . . . 4  class  0
5 csm 22377 . . . 4  class  .h
64, 1, 5co 6040 . . 3  class  ( 0  .h  A )
7 c0v 22380 . . 3  class  0h
86, 7wceq 1649 . 2  wff  ( 0  .h  A )  =  0h
93, 8wi 4 1  wff  ( A  e.  ~H  ->  (
0  .h  A )  =  0h )
Colors of variables: wff set class
This axiom is referenced by:  hvmul0  22479  hvmul0or  22480  hvsubid  22481  hi01  22551  h1de2ctlem  23010  spansneleq  23025  h1datomi  23036
  Copyright terms: Public domain W3C validator