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

Axiom ax-hfvadd 22503
Description: Vector addition is an operation on  ~H. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hfvadd  |-  +h  :
( ~H  X.  ~H )
--> ~H

Detailed syntax breakdown of Axiom ax-hfvadd
StepHypRef Expression
1 chil 22422 . . 3  class  ~H
21, 1cxp 4876 . 2  class  ( ~H 
X.  ~H )
3 cva 22423 . 2  class  +h
42, 1, 3wf 5450 1  wff  +h  :
( ~H  X.  ~H )
--> ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddcl  22515  hilablo  22662  hilid  22663  hilvc  22664  hhnv  22667  hhba  22669  hhph  22680  issh2  22711  hhssabloi  22762  hhssnv  22764  hhshsslem1  22767  hhsssh  22769  shsss  22815  shsel  22816
  Copyright terms: Public domain W3C validator