Metamath Proof Explorer

Theorem mrsubrn

Description: Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (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 mrsubrn 
|- ran S = ( S " ( R ^m V ) )

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. _V -> S : ( R ^pm V ) --> ( R ^m R ) )
5 4 ffnd 
 |-  ( T e. _V -> S Fn ( R ^pm V ) )
6 eleq1w 
 |-  ( x = v -> ( x e. dom f <-> v e. dom f ) )
7 fveq2 
 |-  ( x = v -> ( f ` x ) = ( f ` v ) )
8 s1eq 
 |-  ( x = v -> <" x "> = <" v "> )
9 6 7 8 ifbieq12d 
 |-  ( x = v -> if ( x e. dom f , ( f ` x ) , <" x "> ) = if ( v e. dom f , ( f ` v ) , <" v "> ) )
10 eqid 
 |-  ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) = ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) )
11 fvex 
 |-  ( f ` v ) e. _V
12 s1cli 
 |-  <" v "> e. Word _V
13 12 elexi 
 |-  <" v "> e. _V
14 11 13 ifex 
 |-  if ( v e. dom f , ( f ` v ) , <" v "> ) e. _V
15 9 10 14 fvmpt 
 |-  ( v e. V -> ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) = if ( v e. dom f , ( f ` v ) , <" v "> ) )
16 15 adantl 
 |-  ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ v e. V ) -> ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) = if ( v e. dom f , ( f ` v ) , <" v "> ) )
17 16 ifeq1da 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) = if ( v e. V , if ( v e. dom f , ( f ` v ) , <" v "> ) , <" v "> ) )
18 ifan 
 |-  if ( ( v e. V /\ v e. dom f ) , ( f ` v ) , <" v "> ) = if ( v e. V , if ( v e. dom f , ( f ` v ) , <" v "> ) , <" v "> )
19 17 18 eqtr4di 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) = if ( ( v e. V /\ v e. dom f ) , ( f ` v ) , <" v "> ) )
20 elpmi 
 |-  ( f e. ( R ^pm V ) -> ( f : dom f --> R /\ dom f C_ V ) )
21 20 adantl 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( f : dom f --> R /\ dom f C_ V ) )
22 21 simprd 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> dom f C_ V )
23 22 sseld 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( v e. dom f -> v e. V ) )
24 23 pm4.71rd 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( v e. dom f <-> ( v e. V /\ v e. dom f ) ) )
25 24 bicomd 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( ( v e. V /\ v e. dom f ) <-> v e. dom f ) )
26 25 ifbid 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> if ( ( v e. V /\ v e. dom f ) , ( f ` v ) , <" v "> ) = if ( v e. dom f , ( f ` v ) , <" v "> ) )
27 19 26 eqtr2d 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> if ( v e. dom f , ( f ` v ) , <" v "> ) = if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) )
28 27 mpteq2dv 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) = ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) ) )
29 28 coeq1d 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) = ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) ) o. e ) )
30 29 oveq2d 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) = ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) ) o. e ) ) )
31 30 mpteq2dv 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) = ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) ) o. e ) ) ) )
32 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
33 eqid 
 |-  ( freeMnd ` ( ( mCN ` T ) u. V ) ) = ( freeMnd ` ( ( mCN ` T ) u. V ) )
34 32 1 2 3 33 mrsubfval 
 |-  ( ( f : dom f --> R /\ dom f C_ V ) -> ( S ` f ) = ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) )
35 21 34 syl 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( S ` f ) = ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) )
36 21 simpld 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> f : dom f --> R )
37 36 adantr 
 |-  ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ x e. V ) -> f : dom f --> R )
38 37 ffvelrnda 
 |-  ( ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ x e. V ) /\ x e. dom f ) -> ( f ` x ) e. R )
39 elun2 
 |-  ( x e. V -> x e. ( ( mCN ` T ) u. V ) )
40 39 ad2antlr 
 |-  ( ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ x e. V ) /\ -. x e. dom f ) -> x e. ( ( mCN ` T ) u. V ) )
41 40 s1cld 
 |-  ( ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ x e. V ) /\ -. x e. dom f ) -> <" x "> e. Word ( ( mCN ` T ) u. V ) )
42 32 1 2 mrexval 
 |-  ( T e. _V -> R = Word ( ( mCN ` T ) u. V ) )
43 42 ad3antrrr 
 |-  ( ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ x e. V ) /\ -. x e. dom f ) -> R = Word ( ( mCN ` T ) u. V ) )
44 41 43 eleqtrrd 
 |-  ( ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ x e. V ) /\ -. x e. dom f ) -> <" x "> e. R )
45 38 44 ifclda 
 |-  ( ( ( T e. _V /\ f e. ( R ^pm V ) ) /\ x e. V ) -> if ( x e. dom f , ( f ` x ) , <" x "> ) e. R )
46 45 fmpttd 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) : V --> R )
47 ssid 
 |-  V C_ V
48 32 1 2 3 33 mrsubfval 
 |-  ( ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) : V --> R /\ V C_ V ) -> ( S ` ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ) = ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) ) o. e ) ) ) )
49 46 47 48 sylancl 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( S ` ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ) = ( e e. R |-> ( ( freeMnd ` ( ( mCN ` T ) u. V ) ) gsum ( ( v e. ( ( mCN ` T ) u. V ) |-> if ( v e. V , ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ` v ) , <" v "> ) ) o. e ) ) ) )
50 31 35 49 3eqtr4d 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( S ` f ) = ( S ` ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ) )
51 5 adantr 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> S Fn ( R ^pm V ) )
52 mapsspm 
 |-  ( R ^m V ) C_ ( R ^pm V )
53 52 a1i 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( R ^m V ) C_ ( R ^pm V ) )
54 2 fvexi 
 |-  R e. _V
55 1 fvexi 
 |-  V e. _V
56 54 55 elmap 
 |-  ( ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) e. ( R ^m V ) <-> ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) : V --> R )
57 46 56 sylibr 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) e. ( R ^m V ) )
58 fnfvima 
 |-  ( ( S Fn ( R ^pm V ) /\ ( R ^m V ) C_ ( R ^pm V ) /\ ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) e. ( R ^m V ) ) -> ( S ` ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ) e. ( S " ( R ^m V ) ) )
59 51 53 57 58 syl3anc 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( S ` ( x e. V |-> if ( x e. dom f , ( f ` x ) , <" x "> ) ) ) e. ( S " ( R ^m V ) ) )
60 50 59 eqeltrd 
 |-  ( ( T e. _V /\ f e. ( R ^pm V ) ) -> ( S ` f ) e. ( S " ( R ^m V ) ) )
61 60 ralrimiva 
 |-  ( T e. _V -> A. f e. ( R ^pm V ) ( S ` f ) e. ( S " ( R ^m V ) ) )
62 ffnfv 
 |-  ( S : ( R ^pm V ) --> ( S " ( R ^m V ) ) <-> ( S Fn ( R ^pm V ) /\ A. f e. ( R ^pm V ) ( S ` f ) e. ( S " ( R ^m V ) ) ) )
63 5 61 62 sylanbrc 
 |-  ( T e. _V -> S : ( R ^pm V ) --> ( S " ( R ^m V ) ) )
64 63 frnd 
 |-  ( T e. _V -> ran S C_ ( S " ( R ^m V ) ) )
65 3 rnfvprc 
 |-  ( -. T e. _V -> ran S = (/) )
66 0ss 
 |-  (/) C_ ( S " ( R ^m V ) )
67 65 66 eqsstrdi 
 |-  ( -. T e. _V -> ran S C_ ( S " ( R ^m V ) ) )
68 64 67 pm2.61i 
 |-  ran S C_ ( S " ( R ^m V ) )
69 imassrn 
 |-  ( S " ( R ^m V ) ) C_ ran S
70 68 69 eqssi 
 |-  ran S = ( S " ( R ^m V ) )