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

Axiom ax-hvaddid 21584
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 21499 . . 3  class  ~H
31, 2wcel 1684 . 2  wff  A  e. 
~H
4 c0v 21504 . . . 4  class  0h
5 cva 21500 . . . 4  class  +h
61, 4, 5co 5858 . . 3  class  ( A  +h  0h )
76, 1wceq 1623 . 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  21602  hvpncan  21618  hvsubeq0i  21642  hvsubcan2i  21643  hvsubaddi  21645  hvsub0  21655  hvaddsub4  21657  norm3difi  21726  shsel1  21900  shunssi  21947  omlsilem  21981  pjoc1i  22010  pjchi  22011  spansncvi  22231  5oalem1  22233  5oalem2  22234  3oalem2  22242  pjssmii  22260  hoaddid1i  22366  lnop0  22546  lnopmul  22547  lnfn0i  22622  lnfnmuli  22624  pjclem4  22779  pj3si  22787  hst1h  22807  sumdmdlem  22998
  Copyright terms: Public domain W3C validator