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

Metamath Proof Explorer

Theorem nvmf

Description: Mapping for the vector subtraction operation. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvmf.1 
|- X = ( BaseSet ` U )
nvmf.3 
|- M = ( -v ` U )
Assertion nvmf 
|- ( U e. NrmCVec -> M : ( X X. X ) --> X )

Proof

Step Hyp Ref Expression
1 nvmf.1 
 |-  X = ( BaseSet ` U )
2 nvmf.3 
 |-  M = ( -v ` U )
3 simpl 
 |-  ( ( U e. NrmCVec /\ ( x e. X /\ y e. X ) ) -> U e. NrmCVec )
4 simprl 
 |-  ( ( U e. NrmCVec /\ ( x e. X /\ y e. X ) ) -> x e. X )
5 neg1cn 
 |-  -u 1 e. CC
6 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
7 1 6 nvscl 
 |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ y e. X ) -> ( -u 1 ( .sOLD ` U ) y ) e. X )
8 5 7 mp3an2 
 |-  ( ( U e. NrmCVec /\ y e. X ) -> ( -u 1 ( .sOLD ` U ) y ) e. X )
9 8 adantrl 
 |-  ( ( U e. NrmCVec /\ ( x e. X /\ y e. X ) ) -> ( -u 1 ( .sOLD ` U ) y ) e. X )
10 eqid 
 |-  ( +v ` U ) = ( +v ` U )
11 1 10 nvgcl 
 |-  ( ( U e. NrmCVec /\ x e. X /\ ( -u 1 ( .sOLD ` U ) y ) e. X ) -> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) e. X )
12 3 4 9 11 syl3anc 
 |-  ( ( U e. NrmCVec /\ ( x e. X /\ y e. X ) ) -> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) e. X )
13 12 ralrimivva 
 |-  ( U e. NrmCVec -> A. x e. X A. y e. X ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) e. X )
14 eqid 
 |-  ( x e. X , y e. X |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) = ( x e. X , y e. X |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) )
15 14 fmpo 
 |-  ( A. x e. X A. y e. X ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) e. X <-> ( x e. X , y e. X |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) : ( X X. X ) --> X )
16 13 15 sylib 
 |-  ( U e. NrmCVec -> ( x e. X , y e. X |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) : ( X X. X ) --> X )
17 1 10 6 2 nvmfval 
 |-  ( U e. NrmCVec -> M = ( x e. X , y e. X |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) )
18 17 feq1d 
 |-  ( U e. NrmCVec -> ( M : ( X X. X ) --> X <-> ( x e. X , y e. X |-> ( x ( +v ` U ) ( -u 1 ( .sOLD ` U ) y ) ) ) : ( X X. X ) --> X ) )
19 16 18 mpbird 
 |-  ( U e. NrmCVec -> M : ( X X. X ) --> X )