Theorem hvmulcl 30940

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   ℋchba 30846   ·_ℎ csm 30848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-hfvmul 30932

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538  df-ov 7406

This theorem is referenced by:  hvmulcli  30941  hvsubf  30942  hvsubcl  30944  hv2neg  30955  hvaddsubval  30960  hvsub4  30964  hvaddsub12  30965  hvpncan  30966  hvaddsubass  30968  hvsubass  30971  hvsubdistr1  30976  hvsubdistr2  30977  hvaddeq0  30996  hvmulcan  30999  hvmulcan2  31000  hvsubcan  31001  his5  31013  his35  31015  hiassdi  31018  his2sub  31019  hilablo  31087  helch  31170  ocsh  31210  h1de2ci  31483  spansncol  31495  spanunsni  31506  mayete3i  31655  homcl  31673  homulcl  31686  unoplin  31847  hmoplin  31869  bramul  31873  bralnfn  31875  brafnmul  31878  kbop  31880  kbmul  31882  lnopmul  31894  lnopaddmuli  31900  lnopsubmuli  31902  lnopmulsubi  31903  0lnfn  31912  nmlnop0iALT  31922  lnopmi  31927  lnophsi  31928  lnopcoi  31930  lnopeq0i  31934  nmbdoplbi  31951  nmcexi  31953  nmcoplbi  31955  lnfnmuli  31971  lnfnaddmuli  31972  nmbdfnlbi  31976  nmcfnlbi  31979  nlelshi  31987  riesz3i  31989  cnlnadjlem2  31995  cnlnadjlem6  31999  adjlnop  32013  nmopcoi  32022  branmfn  32032  cnvbramul  32042  kbass2  32044  kbass5  32047  superpos  32281  cdj1i  32360