Theorem hvsubf

Description: Mapping domain and codomain of vector subtraction. (Contributed by NM, 6-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	hvsubf	|- -h : ( ~H X. ~H ) --> ~H

Proof

Step	Hyp	Ref	Expression
1		neg1cn	|- -u 1 e. CC
2		hvmulcl	|- ( ( -u 1 e. CC /\ y e. ~H ) -> ( -u 1 .h y ) e. ~H )
3	1 2	mpan	|- ( y e. ~H -> ( -u 1 .h y ) e. ~H )
4		hvaddcl	|- ( ( x e. ~H /\ ( -u 1 .h y ) e. ~H ) -> ( x +h ( -u 1 .h y ) ) e. ~H )
5	3 4	sylan2	|- ( ( x e. ~H /\ y e. ~H ) -> ( x +h ( -u 1 .h y ) ) e. ~H )
6	5	rgen2	|- A. x e. ~H A. y e. ~H ( x +h ( -u 1 .h y ) ) e. ~H
7		df-hvsub	|- -h = ( x e. ~H , y e. ~H |-> ( x +h ( -u 1 .h y ) ) )
8	7	fmpo	|- ( A. x e. ~H A. y e. ~H ( x +h ( -u 1 .h y ) ) e. ~H <-> -h : ( ~H X. ~H ) --> ~H )
9	6 8	mpbi	|- -h : ( ~H X. ~H ) --> ~H