Theorem hvsubcl

Description: Closure of vector subtraction. (Contributed by NM, 17-Aug-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hvsubval	|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) = ( A +h ( -u 1 .h B ) ) )
2		neg1cn	|- -u 1 e. CC
3		hvmulcl	|- ( ( -u 1 e. CC /\ B e. ~H ) -> ( -u 1 .h B ) e. ~H )
4	2 3	mpan	|- ( B e. ~H -> ( -u 1 .h B ) e. ~H )
5		hvaddcl	|- ( ( A e. ~H /\ ( -u 1 .h B ) e. ~H ) -> ( A +h ( -u 1 .h B ) ) e. ~H )
6	4 5	sylan2	|- ( ( A e. ~H /\ B e. ~H ) -> ( A +h ( -u 1 .h B ) ) e. ~H )
7	1 6	eqeltrd	|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) e. ~H )