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

Axiom ax-hvaddid 21414
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 21329 . . 3  class  ~H
31, 2wcel 1621 . 2  wff  A  e. 
~H
4 c0v 21334 . . . 4  class  0h
5 cva 21330 . . . 4  class  +h
61, 4, 5co 5710 . . 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  21432  hvpncan  21448  hvsubeq0i  21472  hvsubcan2i  21473  hvsubaddi  21475  hvsub0  21485  hvaddsub4  21487  norm3difi  21556  shsel1  21730  shunssi  21777  omlsilem  21811  pjoc1i  21840  pjchi  21841  spansncvi  22079  5oalem1  22081  5oalem2  22082  3oalem2  22090  pjssmii  22108  hoaddid1i  22196  lnop0  22376  lnopmul  22377  lnfn0i  22452  lnfnmuli  22454  pjclem4  22609  pj3si  22617  hst1h  22637  sumdmdlem  22828
  Copyright terms: Public domain W3C validator