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

Theorem hvaddcl 21706
Description: Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
hvaddcl  |-  ( ( A  e.  ~H  /\  B  e.  ~H )  ->  ( A  +h  B
)  e.  ~H )

Proof of Theorem hvaddcl
StepHypRef Expression
1 ax-hfvadd 21694 . 2  |-  +h  :
( ~H  X.  ~H )
--> ~H
21fovcl 6036 1  |-  ( ( A  e.  ~H  /\  B  e.  ~H )  ->  ( A  +h  B
)  e.  ~H )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1710  (class class class)co 5945   ~Hchil 21613    +h cva 21614
This theorem is referenced by:  hvsubf  21709  hvsubcl  21711  hvaddcli  21712  hvadd4  21729  hvsub4  21730  hvpncan  21732  hvaddsubass  21734  hvsubass  21737  hv2times  21754  hvaddsub4  21771  his7  21783  normpyc  21839  hhph  21871  hlimadd  21886  helch  21937  ocsh  21976  spanunsni  22272  3oalem1  22355  pjcompi  22365  mayete3i  22421  mayete3iOLD  22422  hoscl  22439  hoaddcl  22452  unoplin  22614  hmoplin  22636  braadd  22639  0lnfn  22679  lnopmi  22694  lnophsi  22695  lnopcoi  22697  lnopeq0i  22701  nlelshi  22754  cnlnadjlem2  22762  cnlnadjlem6  22766  adjlnop  22780  superpos  23048  cdj3lem2b  23131  cdj3i  23135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295  ax-hfvadd 21694
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-fv 5345  df-ov 5948
  Copyright terms: Public domain W3C validator