Theorem hvmulcl 31365

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   ℋchba 31271   ·_ℎ csm 31273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-hfvmul 31357

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413

This theorem is referenced by:  hvmulcli  31366  hvsubf  31367  hvsubcl  31369  hv2neg  31380  hvaddsubval  31385  hvsub4  31389  hvaddsub12  31390  hvpncan  31391  hvaddsubass  31393  hvsubass  31396  hvsubdistr1  31401  hvsubdistr2  31402  hvaddeq0  31421  hvmulcan  31424  hvmulcan2  31425  hvsubcan  31426  his5  31438  his35  31440  hiassdi  31443  his2sub  31444  hilablo  31512  helch  31595  ocsh  31635  h1de2ci  31908  spansncol  31920  spanunsni  31931  mayete3i  32080  homcl  32098  homulcl  32111  unoplin  32272  hmoplin  32294  bramul  32298  bralnfn  32300  brafnmul  32303  kbop  32305  kbmul  32307  lnopmul  32319  lnopaddmuli  32325  lnopsubmuli  32327  lnopmulsubi  32328  0lnfn  32337  nmlnop0iALT  32347  lnopmi  32352  lnophsi  32353  lnopcoi  32355  lnopeq0i  32359  nmbdoplbi  32376  nmcexi  32378  nmcoplbi  32380  lnfnmuli  32396  lnfnaddmuli  32397  nmbdfnlbi  32401  nmcfnlbi  32404  nlelshi  32412  riesz3i  32414  cnlnadjlem2  32420  cnlnadjlem6  32424  adjlnop  32438  nmopcoi  32447  branmfn  32457  cnvbramul  32467  kbass2  32469  kbass5  32472  superpos  32706  cdj1i  32785