Theorem nvgf

Description: Mapping for the vector addition operation. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvgf.1	|- X = ( BaseSet ` U )
	nvgf.2	|- G = ( +v ` U )
Assertion	nvgf	|- ( U e. NrmCVec -> G : ( X X. X ) --> X )

Proof

Step	Hyp	Ref	Expression
1		nvgf.1	|- X = ( BaseSet ` U )
2		nvgf.2	|- G = ( +v ` U )
3	2	nvgrp	|- ( U e. NrmCVec -> G e. GrpOp )
4	1 2	bafval	|- X = ran G
5	4	grpofo	|- ( G e. GrpOp -> G : ( X X. X ) -onto-> X )
6		fof	|- ( G : ( X X. X ) -onto-> X -> G : ( X X. X ) --> X )
7	3 5 6	3syl	|- ( U e. NrmCVec -> G : ( X X. X ) --> X )