This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 ) )