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

Theorem hvmulcl 24350
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 24342 . 2  |-  .h  :
( CC  X.  ~H )
--> ~H
21fovcl 6194 1  |-  ( ( A  e.  CC  /\  B  e.  ~H )  ->  ( A  .h  B
)  e.  ~H )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1761  (class class class)co 6090   CCcc 9276   ~Hchil 24256    .h csm 24258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528  ax-hfvmul 24342
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-fv 5423  df-ov 6093
This theorem is referenced by:  hvmulcli  24351  hvsubf  24352  hvsubcl  24354  hv2neg  24365  hvaddsubval  24370  hvsub4  24374  hvaddsub12  24375  hvpncan  24376  hvaddsubass  24378  hvsubass  24381  hvsubdistr1  24386  hvsubdistr2  24387  hvaddeq0  24406  hvmulcan  24409  hvmulcan2  24410  hvsubcan  24411  his5  24423  his35  24425  hiassdi  24428  his2sub  24429  hilablo  24497  helch  24581  ocsh  24621  h1de2ci  24894  spansncol  24906  spanunsni  24917  mayete3i  25066  mayete3iOLD  25067  homcl  25085  homulcl  25098  unoplin  25259  hmoplin  25281  bramul  25285  bralnfn  25287  brafnmul  25290  kbop  25292  kbmul  25294  lnopmul  25306  lnopaddmuli  25312  lnopsubmuli  25314  lnopmulsubi  25315  0lnfn  25324  nmlnop0iALT  25334  lnopmi  25339  lnophsi  25340  lnopcoi  25342  lnopeq0i  25346  nmbdoplbi  25363  nmcexi  25365  nmcoplbi  25367  lnfnmuli  25383  lnfnaddmuli  25384  nmbdfnlbi  25388  nmcfnlbi  25391  nlelshi  25399  riesz3i  25401  cnlnadjlem2  25407  cnlnadjlem6  25411  adjlnop  25425  nmopcoi  25434  branmfn  25444  cnvbramul  25454  kbass2  25456  kbass5  25459  superpos  25693  cdj1i  25772
  Copyright terms: Public domain W3C validator