Theorem hvmulcl 28790

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   ℋchba 28696   ·_ℎ csm 28698

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-hfvmul 28782

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159

This theorem is referenced by:  hvmulcli  28791  hvsubf  28792  hvsubcl  28794  hv2neg  28805  hvaddsubval  28810  hvsub4  28814  hvaddsub12  28815  hvpncan  28816  hvaddsubass  28818  hvsubass  28821  hvsubdistr1  28826  hvsubdistr2  28827  hvaddeq0  28846  hvmulcan  28849  hvmulcan2  28850  hvsubcan  28851  his5  28863  his35  28865  hiassdi  28868  his2sub  28869  hilablo  28937  helch  29020  ocsh  29060  h1de2ci  29333  spansncol  29345  spanunsni  29356  mayete3i  29505  homcl  29523  homulcl  29536  unoplin  29697  hmoplin  29719  bramul  29723  bralnfn  29725  brafnmul  29728  kbop  29730  kbmul  29732  lnopmul  29744  lnopaddmuli  29750  lnopsubmuli  29752  lnopmulsubi  29753  0lnfn  29762  nmlnop0iALT  29772  lnopmi  29777  lnophsi  29778  lnopcoi  29780  lnopeq0i  29784  nmbdoplbi  29801  nmcexi  29803  nmcoplbi  29805  lnfnmuli  29821  lnfnaddmuli  29822  nmbdfnlbi  29826  nmcfnlbi  29829  nlelshi  29837  riesz3i  29839  cnlnadjlem2  29845  cnlnadjlem6  29849  adjlnop  29863  nmopcoi  29872  branmfn  29882  cnvbramul  29892  kbass2  29894  kbass5  29897  superpos  30131  cdj1i  30210