This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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