Metamath Proof Explorer

Theorem hvaddcl

Description: Closure of vector addition. (Contributed by NM, 18-Apr-2007) (New usage is discouraged.)

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

Proof

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