Theorem hvmulcl 30985

Description: Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007.) (New usage is discouraged.)

Assertion

Ref	Expression
hvmulcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ)

Proof of Theorem hvmulcl

Step	Hyp	Ref	Expression
1		ax-hfvmul 30977	. 2 ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
2	1	fovcl 7469	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  (class class class)co 7341  ℂcc 10999   ℋchba 30891   ·_ℎ csm 30893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-hfvmul 30977

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-fv 6484  df-ov 7344

This theorem is referenced by:  hvmulcli  30986  hvsubf  30987  hvsubcl  30989  hv2neg  31000  hvaddsubval  31005  hvsub4  31009  hvaddsub12  31010  hvpncan  31011  hvaddsubass  31013  hvsubass  31016  hvsubdistr1  31021  hvsubdistr2  31022  hvaddeq0  31041  hvmulcan  31044  hvmulcan2  31045  hvsubcan  31046  his5  31058  his35  31060  hiassdi  31063  his2sub  31064  hilablo  31132  helch  31215  ocsh  31255  h1de2ci  31528  spansncol  31540  spanunsni  31551  mayete3i  31700  homcl  31718  homulcl  31731  unoplin  31892  hmoplin  31914  bramul  31918  bralnfn  31920  brafnmul  31923  kbop  31925  kbmul  31927  lnopmul  31939  lnopaddmuli  31945  lnopsubmuli  31947  lnopmulsubi  31948  0lnfn  31957  nmlnop0iALT  31967  lnopmi  31972  lnophsi  31973  lnopcoi  31975  lnopeq0i  31979  nmbdoplbi  31996  nmcexi  31998  nmcoplbi  32000  lnfnmuli  32016  lnfnaddmuli  32017  nmbdfnlbi  32021  nmcfnlbi  32024  nlelshi  32032  riesz3i  32034  cnlnadjlem2  32040  cnlnadjlem6  32044  adjlnop  32058  nmopcoi  32067  branmfn  32077  cnvbramul  32087  kbass2  32089  kbass5  32092  superpos  32326  cdj1i  32405