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

Axiom ax-hvaddid 22460
Description: Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvaddid  |-  ( A  e.  ~H  ->  ( A  +h  0h )  =  A )

Detailed syntax breakdown of Axiom ax-hvaddid
StepHypRef Expression
1 cA . . 3  class  A
2 chil 22375 . . 3  class  ~H
31, 2wcel 1721 . 2  wff  A  e. 
~H
4 c0v 22380 . . . 4  class  0h
5 cva 22376 . . . 4  class  +h
61, 4, 5co 6040 . . 3  class  ( A  +h  0h )
76, 1wceq 1649 . 2  wff  ( A  +h  0h )  =  A
83, 7wi 4 1  wff  ( A  e.  ~H  ->  ( A  +h  0h )  =  A )
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  22478  hvpncan  22494  hvsubeq0i  22518  hvsubcan2i  22519  hvsubaddi  22521  hvsub0  22531  hvaddsub4  22533  norm3difi  22602  shsel1  22776  shunssi  22823  omlsilem  22857  pjoc1i  22886  pjchi  22887  spansncvi  23107  5oalem1  23109  5oalem2  23110  3oalem2  23118  pjssmii  23136  hoaddid1i  23242  lnop0  23422  lnopmul  23423  lnfn0i  23498  lnfnmuli  23500  pjclem4  23655  pj3si  23663  hst1h  23683  sumdmdlem  23874
  Copyright terms: Public domain W3C validator