Theorem 0vfval

Description: Value of the function for the zero vector on a normed complex vector space. (Contributed by NM, 24-Apr-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0vfval.2	|- G = ( +v ` U )
	0vfval.5	|- Z = ( 0vec ` U )
Assertion	0vfval	|- ( U e. V -> Z = ( GId ` G ) )

Proof

Step	Hyp	Ref	Expression
1		0vfval.2	|- G = ( +v ` U )
2		0vfval.5	|- Z = ( 0vec ` U )
3		elex	|- ( U e. V -> U e. _V )
4		fo1st	|- 1st : _V -onto-> _V
5		fofn	|- ( 1st : _V -onto-> _V -> 1st Fn _V )
6	4 5	ax-mp	|- 1st Fn _V
7		ssv	|- ran 1st C_ _V
8		fnco	|- ( ( 1st Fn _V /\ 1st Fn _V /\ ran 1st C_ _V ) -> ( 1st o. 1st ) Fn _V )
9	6 6 7 8	mp3an	|- ( 1st o. 1st ) Fn _V
10		df-va	|- +v = ( 1st o. 1st )
11	10	fneq1i	|- ( +v Fn _V <-> ( 1st o. 1st ) Fn _V )
12	9 11	mpbir	|- +v Fn _V
13		fvco2	|- ( ( +v Fn _V /\ U e. _V ) -> ( ( GId o. +v ) ` U ) = ( GId ` ( +v ` U ) ) )
14	12 13	mpan	|- ( U e. _V -> ( ( GId o. +v ) ` U ) = ( GId ` ( +v ` U ) ) )
15		df-0v	|- 0vec = ( GId o. +v )
16	15	fveq1i	|- ( 0vec ` U ) = ( ( GId o. +v ) ` U )
17	2 16	eqtri	|- Z = ( ( GId o. +v ) ` U )
18	1	fveq2i	|- ( GId ` G ) = ( GId ` ( +v ` U ) )
19	14 17 18	3eqtr4g	|- ( U e. _V -> Z = ( GId ` G ) )
20	3 19	syl	|- ( U e. V -> Z = ( GId ` G ) )