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

Theorem hvmulcl 26344
Description: Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
hvmulcl  |-  ( ( A  e.  CC  /\  B  e.  ~H )  ->  ( A  .h  B
)  e.  ~H )

Proof of Theorem hvmulcl
StepHypRef Expression
1 ax-hfvmul 26336 . 2  |-  .h  :
( CC  X.  ~H )
--> ~H
21fovcl 6388 1  |-  ( ( A  e.  CC  /\  B  e.  ~H )  ->  ( A  .h  B
)  e.  ~H )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1842  (class class class)co 6278   CCcc 9520   ~Hchil 26250    .h csm 26252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630  ax-hfvmul 26336
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-fv 5577  df-ov 6281
This theorem is referenced by:  hvmulcli  26345  hvsubf  26346  hvsubcl  26348  hv2neg  26359  hvaddsubval  26364  hvsub4  26368  hvaddsub12  26369  hvpncan  26370  hvaddsubass  26372  hvsubass  26375  hvsubdistr1  26380  hvsubdistr2  26381  hvaddeq0  26400  hvmulcan  26403  hvmulcan2  26404  hvsubcan  26405  his5  26417  his35  26419  hiassdi  26422  his2sub  26423  hilablo  26491  helch  26575  ocsh  26615  h1de2ci  26888  spansncol  26900  spanunsni  26911  mayete3i  27060  homcl  27078  homulcl  27091  unoplin  27252  hmoplin  27274  bramul  27278  bralnfn  27280  brafnmul  27283  kbop  27285  kbmul  27287  lnopmul  27299  lnopaddmuli  27305  lnopsubmuli  27307  lnopmulsubi  27308  0lnfn  27317  nmlnop0iALT  27327  lnopmi  27332  lnophsi  27333  lnopcoi  27335  lnopeq0i  27339  nmbdoplbi  27356  nmcexi  27358  nmcoplbi  27360  lnfnmuli  27376  lnfnaddmuli  27377  nmbdfnlbi  27381  nmcfnlbi  27384  nlelshi  27392  riesz3i  27394  cnlnadjlem2  27400  cnlnadjlem6  27404  adjlnop  27418  nmopcoi  27427  branmfn  27437  cnvbramul  27447  kbass2  27449  kbass5  27452  superpos  27686  cdj1i  27765
  Copyright terms: Public domain W3C validator