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

Axiom ax-hvaddid 21600
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 21515 . . 3  class  ~H
31, 2wcel 1696 . 2  wff  A  e. 
~H
4 c0v 21520 . . . 4  class  0h
5 cva 21516 . . . 4  class  +h
61, 4, 5co 5874 . . 3  class  ( A  +h  0h )
76, 1wceq 1632 . 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  21618  hvpncan  21634  hvsubeq0i  21658  hvsubcan2i  21659  hvsubaddi  21661  hvsub0  21671  hvaddsub4  21673  norm3difi  21742  shsel1  21916  shunssi  21963  omlsilem  21997  pjoc1i  22026  pjchi  22027  spansncvi  22247  5oalem1  22249  5oalem2  22250  3oalem2  22258  pjssmii  22276  hoaddid1i  22382  lnop0  22562  lnopmul  22563  lnfn0i  22638  lnfnmuli  22640  pjclem4  22795  pj3si  22803  hst1h  22823  sumdmdlem  23014
  Copyright terms: Public domain W3C validator