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

Theorem hvmulcl 28704
Description: Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
hvmulcl ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 · 𝐵) ∈ ℋ)

Proof of Theorem hvmulcl
StepHypRef Expression
1 ax-hfvmul 28696 . 2 · :(ℂ × ℋ)⟶ ℋ
21fovcl 7269 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 · 𝐵) ∈ ℋ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  (class class class)co 7148  cc 10524  chba 28610   · csm 28612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326  ax-hfvmul 28696
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-fv 6360  df-ov 7151
This theorem is referenced by:  hvmulcli  28705  hvsubf  28706  hvsubcl  28708  hv2neg  28719  hvaddsubval  28724  hvsub4  28728  hvaddsub12  28729  hvpncan  28730  hvaddsubass  28732  hvsubass  28735  hvsubdistr1  28740  hvsubdistr2  28741  hvaddeq0  28760  hvmulcan  28763  hvmulcan2  28764  hvsubcan  28765  his5  28777  his35  28779  hiassdi  28782  his2sub  28783  hilablo  28851  helch  28934  ocsh  28974  h1de2ci  29247  spansncol  29259  spanunsni  29270  mayete3i  29419  homcl  29437  homulcl  29450  unoplin  29611  hmoplin  29633  bramul  29637  bralnfn  29639  brafnmul  29642  kbop  29644  kbmul  29646  lnopmul  29658  lnopaddmuli  29664  lnopsubmuli  29666  lnopmulsubi  29667  0lnfn  29676  nmlnop0iALT  29686  lnopmi  29691  lnophsi  29692  lnopcoi  29694  lnopeq0i  29698  nmbdoplbi  29715  nmcexi  29717  nmcoplbi  29719  lnfnmuli  29735  lnfnaddmuli  29736  nmbdfnlbi  29740  nmcfnlbi  29743  nlelshi  29751  riesz3i  29753  cnlnadjlem2  29759  cnlnadjlem6  29763  adjlnop  29777  nmopcoi  29786  branmfn  29796  cnvbramul  29806  kbass2  29808  kbass5  29811  superpos  30045  cdj1i  30124
  Copyright terms: Public domain W3C validator