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

Theorem hvaddcl 28801
Description: Closure of vector addition. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
hvaddcl ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) ∈ ℋ)

Proof of Theorem hvaddcl
StepHypRef Expression
1 ax-hfvadd 28789 . 2 + :( ℋ × ℋ)⟶ ℋ
21fovcl 7273 1 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 + 𝐵) ∈ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115  (class class class)co 7150  chba 28708   + cva 28709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pr 5318  ax-hfvadd 28789
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-v 3483  df-sbc 3760  df-csb 3868  df-dif 3923  df-un 3925  df-in 3927  df-ss 3937  df-nul 4278  df-if 4452  df-sn 4552  df-pr 4554  df-op 4558  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-fv 6352  df-ov 7153
This theorem is referenced by:  hvsubf  28804  hvsubcl  28806  hvaddcli  28807  hvadd4  28825  hvsub4  28826  hvpncan  28828  hvaddsubass  28830  hvsubass  28833  hv2times  28850  hvaddsub4  28867  his7  28879  normpyc  28935  hhph  28967  hlimadd  28982  helch  29032  ocsh  29072  spanunsni  29368  3oalem1  29451  pjcompi  29461  mayete3i  29517  hoscl  29534  hoaddcl  29547  unoplin  29709  hmoplin  29731  braadd  29734  0lnfn  29774  lnopmi  29789  lnophsi  29790  lnopcoi  29792  lnopeq0i  29796  nlelshi  29849  cnlnadjlem2  29857  cnlnadjlem6  29861  adjlnop  29875  superpos  30143  cdj3lem2b  30226  cdj3i  30230
  Copyright terms: Public domain W3C validator