Theorem hvmulcl 30942

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   ℋchba 30848   ·_ℎ csm 30850

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-hfvmul 30934

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390

This theorem is referenced by:  hvmulcli  30943  hvsubf  30944  hvsubcl  30946  hv2neg  30957  hvaddsubval  30962  hvsub4  30966  hvaddsub12  30967  hvpncan  30968  hvaddsubass  30970  hvsubass  30973  hvsubdistr1  30978  hvsubdistr2  30979  hvaddeq0  30998  hvmulcan  31001  hvmulcan2  31002  hvsubcan  31003  his5  31015  his35  31017  hiassdi  31020  his2sub  31021  hilablo  31089  helch  31172  ocsh  31212  h1de2ci  31485  spansncol  31497  spanunsni  31508  mayete3i  31657  homcl  31675  homulcl  31688  unoplin  31849  hmoplin  31871  bramul  31875  bralnfn  31877  brafnmul  31880  kbop  31882  kbmul  31884  lnopmul  31896  lnopaddmuli  31902  lnopsubmuli  31904  lnopmulsubi  31905  0lnfn  31914  nmlnop0iALT  31924  lnopmi  31929  lnophsi  31930  lnopcoi  31932  lnopeq0i  31936  nmbdoplbi  31953  nmcexi  31955  nmcoplbi  31957  lnfnmuli  31973  lnfnaddmuli  31974  nmbdfnlbi  31978  nmcfnlbi  31981  nlelshi  31989  riesz3i  31991  cnlnadjlem2  31997  cnlnadjlem6  32001  adjlnop  32015  nmopcoi  32024  branmfn  32034  cnvbramul  32044  kbass2  32046  kbass5  32049  superpos  32283  cdj1i  32362