Theorem hvmulcl 4990

Description: Closure inference for scalar multiplication.

Hypotheses

Ref	Expression
hvmulcl.1	⊢ A ∈ ℂ
hvmulcl.2	⊢ B ∈ ℋ

Assertion

Ref	Expression
hvmulcl	⊢ (A ·s B) ∈ ℋ

Proof of Theorem hvmulcl

Step	Hyp	Ref	Expression
1		hvmulcl.1	. 2 ⊢ A ∈ ℂ
2		hvmulcl.2	. 2 ⊢ B ∈ ℋ
3		ax-hvmulcl 4989	. 2 ⊢ ((A ∈ ℂ ∧ B ∈ ℋ ) → (A ·s B) ∈ ℋ )
4	1, 2, 3	mp2an 520	1 ⊢ (A ·s B) ∈ ℋ

Syntax hints:   ∈ wcel 1092  (class class class)co 3001  ℂcc 4026   ℋ chil 4958   ·_s csm 4960

This theorem is referenced by:  hv2neg 5010  hvsubdistr1 5024  hvsubass 5027  hvsubsub4 5031  hvnegdi 5034  hvsubeq0 5035  hvsubcan2 5036  hvaddcan 5037  hvsubadd 5038  normlem0 5062  normlem5 5067  normlem8 5071  bcseq 5073  norm-iii 5087  norm3dif 5094  normpar2 5100  occllem1 5180  projlem5 5197  projlem7 5199  projlem18 5210  pjthlem1 5225  pjthlem5 5229  pjthlem14 5238  h1de2 5458  pjmul 5568  pjsub 5569

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-hvmulcl 4989

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org