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

Axiom ax-hvmul0 22518
Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 22533 and hvsubval 22524). (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 22427 . . 3  class  ~H
31, 2wcel 1726 . 2  wff  A  e. 
~H
4 cc0 8995 . . . 4  class  0
5 csm 22429 . . . 4  class  .h
64, 1, 5co 6084 . . 3  class  ( 0  .h  A )
7 c0v 22432 . . 3  class  0h
86, 7wceq 1653 . 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  22531  hvmul0or  22532  hvsubid  22533  hi01  22603  h1de2ctlem  23062  spansneleq  23077  h1datomi  23088
  Copyright terms: Public domain W3C validator