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

Axiom ax-hvmul0 21606
Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 21621 and hvsubval 21612). (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 21515 . . 3  class  ~H
31, 2wcel 1696 . 2  wff  A  e. 
~H
4 cc0 8753 . . . 4  class  0
5 csm 21517 . . . 4  class  .h
64, 1, 5co 5874 . . 3  class  ( 0  .h  A )
7 c0v 21520 . . 3  class  0h
86, 7wceq 1632 . 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  21619  hvmul0or  21620  hvsubid  21621  hi01  21691  h1de2ctlem  22150  spansneleq  22165  h1datomi  22176
  Copyright terms: Public domain W3C validator