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

Axiom ax-hvaddid 21578
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 21493 . . 3  class  ~H
31, 2wcel 1687 . 2  wff  A  e. 
~H
4 c0v 21498 . . . 4  class  0h
5 cva 21494 . . . 4  class  +h
61, 4, 5co 5821 . . 3  class  ( A  +h  0h )
76, 1wceq 1625 . 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  21596  hvpncan  21612  hvsubeq0i  21636  hvsubcan2i  21637  hvsubaddi  21639  hvsub0  21649  hvaddsub4  21651  norm3difi  21720  shsel1  21894  shunssi  21941  omlsilem  21975  pjoc1i  22004  pjchi  22005  spansncvi  22225  5oalem1  22227  5oalem2  22228  3oalem2  22236  pjssmii  22254  hoaddid1i  22360  lnop0  22540  lnopmul  22541  lnfn0i  22616  lnfnmuli  22618  pjclem4  22773  pj3si  22781  hst1h  22801  sumdmdlem  22992
  Copyright terms: Public domain W3C validator