Theorem hvmulcl 28900

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 28892	. 2 ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
2	1	fovcl 7279	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ℎ 𝐵) ∈ ℋ)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  (class class class)co 7155  ℂcc 10578   ℋchba 28806   ·_ℎ csm 28808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-hfvmul 28892

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-fv 6347  df-ov 7158

This theorem is referenced by:  hvmulcli  28901  hvsubf  28902  hvsubcl  28904  hv2neg  28915  hvaddsubval  28920  hvsub4  28924  hvaddsub12  28925  hvpncan  28926  hvaddsubass  28928  hvsubass  28931  hvsubdistr1  28936  hvsubdistr2  28937  hvaddeq0  28956  hvmulcan  28959  hvmulcan2  28960  hvsubcan  28961  his5  28973  his35  28975  hiassdi  28978  his2sub  28979  hilablo  29047  helch  29130  ocsh  29170  h1de2ci  29443  spansncol  29455  spanunsni  29466  mayete3i  29615  homcl  29633  homulcl  29646  unoplin  29807  hmoplin  29829  bramul  29833  bralnfn  29835  brafnmul  29838  kbop  29840  kbmul  29842  lnopmul  29854  lnopaddmuli  29860  lnopsubmuli  29862  lnopmulsubi  29863  0lnfn  29872  nmlnop0iALT  29882  lnopmi  29887  lnophsi  29888  lnopcoi  29890  lnopeq0i  29894  nmbdoplbi  29911  nmcexi  29913  nmcoplbi  29915  lnfnmuli  29931  lnfnaddmuli  29932  nmbdfnlbi  29936  nmcfnlbi  29939  nlelshi  29947  riesz3i  29949  cnlnadjlem2  29955  cnlnadjlem6  29959  adjlnop  29973  nmopcoi  29982  branmfn  29992  cnvbramul  30002  kbass2  30004  kbass5  30007  superpos  30241  cdj1i  30320