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