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 )