Metamath Proof Explorer

Theorem mrsubcn

Description: A substitution does not change the value of constant substrings. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubccat.s 
|- S = ( mRSubst ` T )
mrsubccat.r 
|- R = ( mREx ` T )
mrsubcn.v 
|- V = ( mVR ` T )
mrsubcn.c 
|- C = ( mCN ` T )
Assertion mrsubcn 
|- ( ( F e. ran S /\ X e. ( C \ V ) ) -> ( F ` <" X "> ) = <" X "> )

Proof

Step Hyp Ref Expression
1 mrsubccat.s 
 |-  S = ( mRSubst ` T )
2 mrsubccat.r 
 |-  R = ( mREx ` T )
3 mrsubcn.v 
 |-  V = ( mVR ` T )
4 mrsubcn.c 
 |-  C = ( mCN ` T )
5 n0i 
 |-  ( F e. ran S -> -. ran S = (/) )
6 1 rnfvprc 
 |-  ( -. T e. _V -> ran S = (/) )
7 5 6 nsyl2 
 |-  ( F e. ran S -> T e. _V )
8 3 2 1 mrsubff 
 |-  ( T e. _V -> S : ( R ^pm V ) --> ( R ^m R ) )
9 ffun 
 |-  ( S : ( R ^pm V ) --> ( R ^m R ) -> Fun S )
10 7 8 9 3syl 
 |-  ( F e. ran S -> Fun S )
11 3 2 1 mrsubrn 
 |-  ran S = ( S " ( R ^m V ) )
12 11 eleq2i 
 |-  ( F e. ran S <-> F e. ( S " ( R ^m V ) ) )
13 12 biimpi 
 |-  ( F e. ran S -> F e. ( S " ( R ^m V ) ) )
14 fvelima 
 |-  ( ( Fun S /\ F e. ( S " ( R ^m V ) ) ) -> E. f e. ( R ^m V ) ( S ` f ) = F )
15 10 13 14 syl2anc 
 |-  ( F e. ran S -> E. f e. ( R ^m V ) ( S ` f ) = F )
16 elmapi 
 |-  ( f e. ( R ^m V ) -> f : V --> R )
17 16 adantl 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> f : V --> R )
18 ssidd 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> V C_ V )
19 eldifi 
 |-  ( X e. ( C \ V ) -> X e. C )
20 elun1 
 |-  ( X e. C -> X e. ( C u. V ) )
21 19 20 syl 
 |-  ( X e. ( C \ V ) -> X e. ( C u. V ) )
22 21 adantr 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> X e. ( C u. V ) )
23 4 3 2 1 mrsubcv 
 |-  ( ( f : V --> R /\ V C_ V /\ X e. ( C u. V ) ) -> ( ( S ` f ) ` <" X "> ) = if ( X e. V , ( f ` X ) , <" X "> ) )
24 17 18 22 23 syl3anc 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> ( ( S ` f ) ` <" X "> ) = if ( X e. V , ( f ` X ) , <" X "> ) )
25 eldifn 
 |-  ( X e. ( C \ V ) -> -. X e. V )
26 25 adantr 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> -. X e. V )
27 26 iffalsed 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> if ( X e. V , ( f ` X ) , <" X "> ) = <" X "> )
28 24 27 eqtrd 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> ( ( S ` f ) ` <" X "> ) = <" X "> )
29 fveq1 
 |-  ( ( S ` f ) = F -> ( ( S ` f ) ` <" X "> ) = ( F ` <" X "> ) )
30 29 eqeq1d 
 |-  ( ( S ` f ) = F -> ( ( ( S ` f ) ` <" X "> ) = <" X "> <-> ( F ` <" X "> ) = <" X "> ) )
31 28 30 syl5ibcom 
 |-  ( ( X e. ( C \ V ) /\ f e. ( R ^m V ) ) -> ( ( S ` f ) = F -> ( F ` <" X "> ) = <" X "> ) )
32 31 rexlimdva 
 |-  ( X e. ( C \ V ) -> ( E. f e. ( R ^m V ) ( S ` f ) = F -> ( F ` <" X "> ) = <" X "> ) )
33 15 32 mpan9 
 |-  ( ( F e. ran S /\ X e. ( C \ V ) ) -> ( F ` <" X "> ) = <" X "> )