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

Axiom ax-hvmul0 21515
Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 21530 and hvsubval 21521). (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 21424 . . 3  class  ~H
31, 2wcel 1621 . 2  wff  A  e. 
~H
4 cc0 8670 . . . 4  class  0
5 csm 21426 . . . 4  class  .h
64, 1, 5co 5757 . . 3  class  ( 0  .h  A )
7 c0v 21429 . . 3  class  0h
86, 7wceq 1619 . 2  wff  ( 0  .h  A )  =  0h
93, 8wi 6 1  wff  ( A  e.  ~H  ->  (
0  .h  A )  =  0h )
Colors of variables: wff set class
This axiom is referenced by:  hvmul0  21528  hvmul0or  21529  hvsubid  21530  hi01  21600  h1de2ctlem  22059  spansneleq  22074  h1datomi  22085
  Copyright terms: Public domain W3C validator