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

Axiom ax-hvaddid 22499
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 22414 . . 3  class  ~H
31, 2wcel 1725 . 2  wff  A  e. 
~H
4 c0v 22419 . . . 4  class  0h
5 cva 22415 . . . 4  class  +h
61, 4, 5co 6073 . . 3  class  ( A  +h  0h )
76, 1wceq 1652 . 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  22517  hvpncan  22533  hvsubeq0i  22557  hvsubcan2i  22558  hvsubaddi  22560  hvsub0  22570  hvaddsub4  22572  norm3difi  22641  shsel1  22815  shunssi  22862  omlsilem  22896  pjoc1i  22925  pjchi  22926  spansncvi  23146  5oalem1  23148  5oalem2  23149  3oalem2  23157  pjssmii  23175  hoaddid1i  23281  lnop0  23461  lnopmul  23462  lnfn0i  23537  lnfnmuli  23539  pjclem4  23694  pj3si  23702  hst1h  23722  sumdmdlem  23913
  Copyright terms: Public domain W3C validator