Theorem hvmulcl 31088

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   ℋchba 30994   ·_ℎ csm 30996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-hfvmul 31080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361

This theorem is referenced by:  hvmulcli  31089  hvsubf  31090  hvsubcl  31092  hv2neg  31103  hvaddsubval  31108  hvsub4  31112  hvaddsub12  31113  hvpncan  31114  hvaddsubass  31116  hvsubass  31119  hvsubdistr1  31124  hvsubdistr2  31125  hvaddeq0  31144  hvmulcan  31147  hvmulcan2  31148  hvsubcan  31149  his5  31161  his35  31163  hiassdi  31166  his2sub  31167  hilablo  31235  helch  31318  ocsh  31358  h1de2ci  31631  spansncol  31643  spanunsni  31654  mayete3i  31803  homcl  31821  homulcl  31834  unoplin  31995  hmoplin  32017  bramul  32021  bralnfn  32023  brafnmul  32026  kbop  32028  kbmul  32030  lnopmul  32042  lnopaddmuli  32048  lnopsubmuli  32050  lnopmulsubi  32051  0lnfn  32060  nmlnop0iALT  32070  lnopmi  32075  lnophsi  32076  lnopcoi  32078  lnopeq0i  32082  nmbdoplbi  32099  nmcexi  32101  nmcoplbi  32103  lnfnmuli  32119  lnfnaddmuli  32120  nmbdfnlbi  32124  nmcfnlbi  32127  nlelshi  32135  riesz3i  32137  cnlnadjlem2  32143  cnlnadjlem6  32147  adjlnop  32161  nmopcoi  32170  branmfn  32180  cnvbramul  32190  kbass2  32192  kbass5  32195  superpos  32429  cdj1i  32508