Theorem hvmulcl 31436

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113   ℋchba 31342   ·_ℎ csm 31344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-hfvmul 31428

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422

This theorem is used by:  hvmulcli  31437  hvsubf  31438  hvsubcl  31440  hv2neg  31451  hvaddsubval  31456  hvsub4  31460  hvaddsub12  31461  hvpncan  31462  hvaddsubass  31464  hvsubass  31467  hvsubdistr1  31472  hvsubdistr2  31473  hvaddeq0  31492  hvmulcan  31495  hvmulcan2  31496  hvsubcan  31497  his5  31509  his35  31511  hiassdi  31514  his2sub  31515  hilablo  31583  helch  31666  ocsh  31706  h1de2ci  31979  spansncol  31991  spanunsni  32002  mayete3i  32151  homcl  32169  homulcl  32182  unoplin  32343  hmoplin  32365  bramul  32369  bralnfn  32371  brafnmul  32374  kbop  32376  kbmul  32378  lnopmul  32390  lnopaddmuli  32396  lnopsubmuli  32398  lnopmulsubi  32399  0lnfn  32408  nmlnop0iALT  32418  lnopmi  32423  lnophsi  32424  lnopcoi  32426  lnopeq0i  32430  nmbdoplbi  32447  nmcexi  32449  nmcoplbi  32451  lnfnmuli  32467  lnfnaddmuli  32468  nmbdfnlbi  32472  nmcfnlbi  32475  nlelshi  32483  riesz3i  32485  cnlnadjlem2  32491  cnlnadjlem6  32495  adjlnop  32509  nmopcoi  32518  branmfn  32528  cnvbramul  32538  kbass2  32540  kbass5  32543  superpos  32777  cdj1i  32856