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

Axiom ax-hvaddid 21530
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 21445 . . 3  class  ~H
31, 2wcel 1621 . 2  wff  A  e. 
~H
4 c0v 21450 . . . 4  class  0h
5 cva 21446 . . . 4  class  +h
61, 4, 5co 5778 . . 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  21548  hvpncan  21564  hvsubeq0i  21588  hvsubcan2i  21589  hvsubaddi  21591  hvsub0  21601  hvaddsub4  21603  norm3difi  21672  shsel1  21846  shunssi  21893  omlsilem  21927  pjoc1i  21956  pjchi  21957  spansncvi  22195  5oalem1  22197  5oalem2  22198  3oalem2  22206  pjssmii  22224  hoaddid1i  22312  lnop0  22492  lnopmul  22493  lnfn0i  22568  lnfnmuli  22570  pjclem4  22725  pj3si  22733  hst1h  22753  sumdmdlem  22944
  Copyright terms: Public domain W3C validator