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

Axiom ax-hvaddid 21509
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 21424 . . 3  class  ~H
31, 2wcel 1621 . 2  wff  A  e. 
~H
4 c0v 21429 . . . 4  class  0h
5 cva 21425 . . . 4  class  +h
61, 4, 5co 5757 . . 3  class  ( A  +h  0h )
76, 1wceq 1619 . 2  wff  ( A  +h  0h )  =  A
83, 7wi 6 1  wff  ( A  e.  ~H  ->  ( A  +h  0h )  =  A )
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  21527  hvpncan  21543  hvsubeq0i  21567  hvsubcan2i  21568  hvsubaddi  21570  hvsub0  21580  hvaddsub4  21582  norm3difi  21651  shsel1  21825  shunssi  21872  omlsilem  21906  pjoc1i  21935  pjchi  21936  spansncvi  22174  5oalem1  22176  5oalem2  22177  3oalem2  22185  pjssmii  22203  hoaddid1i  22291  lnop0  22471  lnopmul  22472  lnfn0i  22547  lnfnmuli  22549  pjclem4  22704  pj3si  22712  hst1h  22732  sumdmdlem  22923
  Copyright terms: Public domain W3C validator