Theorem hvmulcl 29354

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7268  ℂcc 10853   ℋchba 29260   ·_ℎ csm 29262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-hfvmul 29346

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-fv 6438  df-ov 7271

This theorem is referenced by:  hvmulcli  29355  hvsubf  29356  hvsubcl  29358  hv2neg  29369  hvaddsubval  29374  hvsub4  29378  hvaddsub12  29379  hvpncan  29380  hvaddsubass  29382  hvsubass  29385  hvsubdistr1  29390  hvsubdistr2  29391  hvaddeq0  29410  hvmulcan  29413  hvmulcan2  29414  hvsubcan  29415  his5  29427  his35  29429  hiassdi  29432  his2sub  29433  hilablo  29501  helch  29584  ocsh  29624  h1de2ci  29897  spansncol  29909  spanunsni  29920  mayete3i  30069  homcl  30087  homulcl  30100  unoplin  30261  hmoplin  30283  bramul  30287  bralnfn  30289  brafnmul  30292  kbop  30294  kbmul  30296  lnopmul  30308  lnopaddmuli  30314  lnopsubmuli  30316  lnopmulsubi  30317  0lnfn  30326  nmlnop0iALT  30336  lnopmi  30341  lnophsi  30342  lnopcoi  30344  lnopeq0i  30348  nmbdoplbi  30365  nmcexi  30367  nmcoplbi  30369  lnfnmuli  30385  lnfnaddmuli  30386  nmbdfnlbi  30390  nmcfnlbi  30393  nlelshi  30401  riesz3i  30403  cnlnadjlem2  30409  cnlnadjlem6  30413  adjlnop  30427  nmopcoi  30436  branmfn  30446  cnvbramul  30456  kbass2  30458  kbass5  30461  superpos  30695  cdj1i  30774