Metamath Proof Explorer

Theorem mrsubff1

Description: When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubvr.v 
|- V = ( mVR ` T )
mrsubvr.r 
|- R = ( mREx ` T )
mrsubvr.s 
|- S = ( mRSubst ` T )
Assertion mrsubff1 
|- ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) )

Proof

Step Hyp Ref Expression
1 mrsubvr.v 
 |-  V = ( mVR ` T )
2 mrsubvr.r 
 |-  R = ( mREx ` T )
3 mrsubvr.s 
 |-  S = ( mRSubst ` T )
4 1 2 3 mrsubff 
 |-  ( T e. W -> S : ( R ^pm V ) --> ( R ^m R ) )
5 mapsspm 
 |-  ( R ^m V ) C_ ( R ^pm V )
6 5 a1i 
 |-  ( T e. W -> ( R ^m V ) C_ ( R ^pm V ) )
7 4 6 fssresd 
 |-  ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) --> ( R ^m R ) )
8 fveq1 
 |-  ( ( S ` f ) = ( S ` g ) -> ( ( S ` f ) ` <" v "> ) = ( ( S ` g ) ` <" v "> ) )
9 simplrl 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> f e. ( R ^m V ) )
10 elmapi 
 |-  ( f e. ( R ^m V ) -> f : V --> R )
11 9 10 syl 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> f : V --> R )
12 ssidd 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> V C_ V )
13 simpr 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> v e. V )
14 1 2 3 mrsubvr 
 |-  ( ( f : V --> R /\ V C_ V /\ v e. V ) -> ( ( S ` f ) ` <" v "> ) = ( f ` v ) )
15 11 12 13 14 syl3anc 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> ( ( S ` f ) ` <" v "> ) = ( f ` v ) )
16 simplrr 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> g e. ( R ^m V ) )
17 elmapi 
 |-  ( g e. ( R ^m V ) -> g : V --> R )
18 16 17 syl 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> g : V --> R )
19 1 2 3 mrsubvr 
 |-  ( ( g : V --> R /\ V C_ V /\ v e. V ) -> ( ( S ` g ) ` <" v "> ) = ( g ` v ) )
20 18 12 13 19 syl3anc 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> ( ( S ` g ) ` <" v "> ) = ( g ` v ) )
21 15 20 eqeq12d 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> ( ( ( S ` f ) ` <" v "> ) = ( ( S ` g ) ` <" v "> ) <-> ( f ` v ) = ( g ` v ) ) )
22 8 21 imbitrid 
 |-  ( ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> ( ( S ` f ) = ( S ` g ) -> ( f ` v ) = ( g ` v ) ) )
23 22 ralrimdva 
 |-  ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( S ` f ) = ( S ` g ) -> A. v e. V ( f ` v ) = ( g ` v ) ) )
24 fvres 
 |-  ( f e. ( R ^m V ) -> ( ( S |` ( R ^m V ) ) ` f ) = ( S ` f ) )
25 fvres 
 |-  ( g e. ( R ^m V ) -> ( ( S |` ( R ^m V ) ) ` g ) = ( S ` g ) )
26 24 25 eqeqan12d 
 |-  ( ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) -> ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) <-> ( S ` f ) = ( S ` g ) ) )
27 26 adantl 
 |-  ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) <-> ( S ` f ) = ( S ` g ) ) )
28 ffn 
 |-  ( f : V --> R -> f Fn V )
29 ffn 
 |-  ( g : V --> R -> g Fn V )
30 eqfnfv 
 |-  ( ( f Fn V /\ g Fn V ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
31 28 29 30 syl2an 
 |-  ( ( f : V --> R /\ g : V --> R ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
32 10 17 31 syl2an 
 |-  ( ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
33 32 adantl 
 |-  ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
34 23 27 33 3imtr4d 
 |-  ( ( T e. W /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) -> f = g ) )
35 34 ralrimivva 
 |-  ( T e. W -> A. f e. ( R ^m V ) A. g e. ( R ^m V ) ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) -> f = g ) )
36 dff13 
 |-  ( ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) <-> ( ( S |` ( R ^m V ) ) : ( R ^m V ) --> ( R ^m R ) /\ A. f e. ( R ^m V ) A. g e. ( R ^m V ) ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) -> f = g ) ) )
37 7 35 36 sylanbrc 
 |-  ( T e. W -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) )