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

Axiom ax-hvaddid 22356
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 22271 . . 3  class  ~H
31, 2wcel 1717 . 2  wff  A  e. 
~H
4 c0v 22276 . . . 4  class  0h
5 cva 22272 . . . 4  class  +h
61, 4, 5co 6021 . . 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  22374  hvpncan  22390  hvsubeq0i  22414  hvsubcan2i  22415  hvsubaddi  22417  hvsub0  22427  hvaddsub4  22429  norm3difi  22498  shsel1  22672  shunssi  22719  omlsilem  22753  pjoc1i  22782  pjchi  22783  spansncvi  23003  5oalem1  23005  5oalem2  23006  3oalem2  23014  pjssmii  23032  hoaddid1i  23138  lnop0  23318  lnopmul  23319  lnfn0i  23394  lnfnmuli  23396  pjclem4  23551  pj3si  23559  hst1h  23579  sumdmdlem  23770
  Copyright terms: Public domain W3C validator