Theorem vafval

Description: Value of the function for the vector addition (group) operation on a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	vafval.2	|- G = ( +v ` U )
Assertion	vafval	|- G = ( 1st ` ( 1st ` U ) )

Proof

Step	Hyp	Ref	Expression
1		vafval.2	|- G = ( +v ` U )
2		df-va	|- +v = ( 1st o. 1st )
3	2	fveq1i	|- ( +v ` U ) = ( ( 1st o. 1st ) ` U )
4		fo1st	|- 1st : _V -onto-> _V
5		fof	|- ( 1st : _V -onto-> _V -> 1st : _V --> _V )
6	4 5	ax-mp	|- 1st : _V --> _V
7		fvco3	|- ( ( 1st : _V --> _V /\ U e. _V ) -> ( ( 1st o. 1st ) ` U ) = ( 1st ` ( 1st ` U ) ) )
8	6 7	mpan	|- ( U e. _V -> ( ( 1st o. 1st ) ` U ) = ( 1st ` ( 1st ` U ) ) )
9	3 8	syl5eq	|- ( U e. _V -> ( +v ` U ) = ( 1st ` ( 1st ` U ) ) )
10		fvprc	|- ( -. U e. _V -> ( +v ` U ) = (/) )
11		fvprc	|- ( -. U e. _V -> ( 1st ` U ) = (/) )
12	11	fveq2d	|- ( -. U e. _V -> ( 1st ` ( 1st ` U ) ) = ( 1st ` (/) ) )
13		1st0	|- ( 1st ` (/) ) = (/)
14	12 13	eqtr2di	|- ( -. U e. _V -> (/) = ( 1st ` ( 1st ` U ) ) )
15	10 14	eqtrd	|- ( -. U e. _V -> ( +v ` U ) = ( 1st ` ( 1st ` U ) ) )
16	9 15	pm2.61i	|- ( +v ` U ) = ( 1st ` ( 1st ` U ) )
17	1 16	eqtri	|- G = ( 1st ` ( 1st ` U ) )