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

Theorem hvaddcl 24419
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 24407 . 2  |-  +h  :
( ~H  X.  ~H )
--> ~H
21fovcl 6200 1  |-  ( ( A  e.  ~H  /\  B  e.  ~H )  ->  ( A  +h  B
)  e.  ~H )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756  (class class class)co 6096   ~Hchil 24326    +h cva 24327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536  ax-hfvadd 24407
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-iun 4178  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-fv 5431  df-ov 6099
This theorem is referenced by:  hvsubf  24422  hvsubcl  24424  hvaddcli  24425  hvadd4  24443  hvsub4  24444  hvpncan  24446  hvaddsubass  24448  hvsubass  24451  hv2times  24468  hvaddsub4  24485  his7  24497  normpyc  24553  hhph  24585  hlimadd  24600  helch  24651  ocsh  24691  spanunsni  24987  3oalem1  25070  pjcompi  25080  mayete3i  25136  mayete3iOLD  25137  hoscl  25154  hoaddcl  25167  unoplin  25329  hmoplin  25351  braadd  25354  0lnfn  25394  lnopmi  25409  lnophsi  25410  lnopcoi  25412  lnopeq0i  25416  nlelshi  25469  cnlnadjlem2  25477  cnlnadjlem6  25481  adjlnop  25495  superpos  25763  cdj3lem2b  25846  cdj3i  25850
  Copyright terms: Public domain W3C validator