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

Theorem hvmulcl 24430
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 24422 . 2  |-  .h  :
( CC  X.  ~H )
--> ~H
21fovcl 6210 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 1756  (class class class)co 6106   CCcc 9295   ~Hchil 24336    .h csm 24338
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 4428  ax-nul 4436  ax-pr 4546  ax-hfvmul 24422
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 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-iun 4188  df-br 4308  df-opab 4366  df-mpt 4367  df-id 4651  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-fv 5441  df-ov 6109
This theorem is referenced by:  hvmulcli  24431  hvsubf  24432  hvsubcl  24434  hv2neg  24445  hvaddsubval  24450  hvsub4  24454  hvaddsub12  24455  hvpncan  24456  hvaddsubass  24458  hvsubass  24461  hvsubdistr1  24466  hvsubdistr2  24467  hvaddeq0  24486  hvmulcan  24489  hvmulcan2  24490  hvsubcan  24491  his5  24503  his35  24505  hiassdi  24508  his2sub  24509  hilablo  24577  helch  24661  ocsh  24701  h1de2ci  24974  spansncol  24986  spanunsni  24997  mayete3i  25146  mayete3iOLD  25147  homcl  25165  homulcl  25178  unoplin  25339  hmoplin  25361  bramul  25365  bralnfn  25367  brafnmul  25370  kbop  25372  kbmul  25374  lnopmul  25386  lnopaddmuli  25392  lnopsubmuli  25394  lnopmulsubi  25395  0lnfn  25404  nmlnop0iALT  25414  lnopmi  25419  lnophsi  25420  lnopcoi  25422  lnopeq0i  25426  nmbdoplbi  25443  nmcexi  25445  nmcoplbi  25447  lnfnmuli  25463  lnfnaddmuli  25464  nmbdfnlbi  25468  nmcfnlbi  25471  nlelshi  25479  riesz3i  25481  cnlnadjlem2  25487  cnlnadjlem6  25491  adjlnop  25505  nmopcoi  25514  branmfn  25524  cnvbramul  25534  kbass2  25536  kbass5  25539  superpos  25773  cdj1i  25852
  Copyright terms: Public domain W3C validator