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

Axiom ax-hvmul0 22505
Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 22520 and hvsubval 22511). (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 22414 . . 3  class  ~H
31, 2wcel 1725 . 2  wff  A  e. 
~H
4 cc0 8982 . . . 4  class  0
5 csm 22416 . . . 4  class  .h
64, 1, 5co 6073 . . 3  class  ( 0  .h  A )
7 c0v 22419 . . 3  class  0h
86, 7wceq 1652 . 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  22518  hvmul0or  22519  hvsubid  22520  hi01  22590  h1de2ctlem  23049  spansneleq  23064  h1datomi  23075
  Copyright terms: Public domain W3C validator