Metamath Proof Explorer


Theorem hvmulcli

Description: Closure inference for scalar multiplication. (Contributed by NM, 1-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvmulcl.1 โŠข ๐ด โˆˆ โ„‚
hvmulcl.2 โŠข ๐ต โˆˆ โ„‹
Assertion hvmulcli ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹

Proof

Step Hyp Ref Expression
1 hvmulcl.1 โŠข ๐ด โˆˆ โ„‚
2 hvmulcl.2 โŠข ๐ต โˆˆ โ„‹
3 hvmulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹ )
4 1 2 3 mp2an โŠข ( ๐ด ยทโ„Ž ๐ต ) โˆˆ โ„‹