Theorem hvmulcl 28204

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

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2144  (class class class)co 6792  ℂcc 10135   ℋchil 28110   ·_ℎ csm 28112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034  ax-hfvmul 28196

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039  df-ov 6795

This theorem is referenced by:  hvmulcli  28205  hvsubf  28206  hvsubcl  28208  hv2neg  28219  hvaddsubval  28224  hvsub4  28228  hvaddsub12  28229  hvpncan  28230  hvaddsubass  28232  hvsubass  28235  hvsubdistr1  28240  hvsubdistr2  28241  hvaddeq0  28260  hvmulcan  28263  hvmulcan2  28264  hvsubcan  28265  his5  28277  his35  28279  hiassdi  28282  his2sub  28283  hilablo  28351  helch  28434  ocsh  28476  h1de2ci  28749  spansncol  28761  spanunsni  28772  mayete3i  28921  homcl  28939  homulcl  28952  unoplin  29113  hmoplin  29135  bramul  29139  bralnfn  29141  brafnmul  29144  kbop  29146  kbmul  29148  lnopmul  29160  lnopaddmuli  29166  lnopsubmuli  29168  lnopmulsubi  29169  0lnfn  29178  nmlnop0iALT  29188  lnopmi  29193  lnophsi  29194  lnopcoi  29196  lnopeq0i  29200  nmbdoplbi  29217  nmcexi  29219  nmcoplbi  29221  lnfnmuli  29237  lnfnaddmuli  29238  nmbdfnlbi  29242  nmcfnlbi  29245  nlelshi  29253  riesz3i  29255  cnlnadjlem2  29261  cnlnadjlem6  29265  adjlnop  29279  nmopcoi  29288  branmfn  29298  cnvbramul  29308  kbass2  29310  kbass5  29313  superpos  29547  cdj1i  29626