Metamath Proof Explorer

Theorem hvmulcl

Description: Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion hvmulcl 
|- ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )

Proof

Step Hyp Ref Expression
1 ax-hfvmul 
 |-  .h : ( CC X. ~H ) --> ~H
2 1 fovcl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )