Theorem smfval

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

	Ref	Expression
Hypothesis	smfval.4	|- S = ( .sOLD ` U )
Assertion	smfval	|- S = ( 2nd ` ( 1st ` U ) )

Proof

Step	Hyp	Ref	Expression
1		smfval.4	|- S = ( .sOLD ` U )
2		df-sm	|- .sOLD = ( 2nd o. 1st )
3	2	fveq1i	|- ( .sOLD ` U ) = ( ( 2nd 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 ) -> ( ( 2nd o. 1st ) ` U ) = ( 2nd ` ( 1st ` U ) ) )
8	6 7	mpan	|- ( U e. _V -> ( ( 2nd o. 1st ) ` U ) = ( 2nd ` ( 1st ` U ) ) )
9	3 8	syl5eq	|- ( U e. _V -> ( .sOLD ` U ) = ( 2nd ` ( 1st ` U ) ) )
10		fvprc	|- ( -. U e. _V -> ( .sOLD ` U ) = (/) )
11		fvprc	|- ( -. U e. _V -> ( 1st ` U ) = (/) )
12	11	fveq2d	|- ( -. U e. _V -> ( 2nd ` ( 1st ` U ) ) = ( 2nd ` (/) ) )
13		2nd0	|- ( 2nd ` (/) ) = (/)
14	12 13	eqtr2di	|- ( -. U e. _V -> (/) = ( 2nd ` ( 1st ` U ) ) )
15	10 14	eqtrd	|- ( -. U e. _V -> ( .sOLD ` U ) = ( 2nd ` ( 1st ` U ) ) )
16	9 15	pm2.61i	|- ( .sOLD ` U ) = ( 2nd ` ( 1st ` U ) )
17	1 16	eqtri	|- S = ( 2nd ` ( 1st ` U ) )