Metamath Proof Explorer

Theorem mrsub0

Description: The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis mrsubccat.s 
|- S = ( mRSubst ` T )
Assertion mrsub0 
|- ( F e. ran S -> ( F ` (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 mrsubccat.s 
 |-  S = ( mRSubst ` T )
2 n0i 
 |-  ( F e. ran S -> -. ran S = (/) )
3 1 rnfvprc 
 |-  ( -. T e. _V -> ran S = (/) )
4 2 3 nsyl2 
 |-  ( F e. ran S -> T e. _V )
5 eqid 
 |-  ( mVR ` T ) = ( mVR ` T )
6 eqid 
 |-  ( mREx ` T ) = ( mREx ` T )
7 5 6 1 mrsubff 
 |-  ( T e. _V -> S : ( ( mREx ` T ) ^pm ( mVR ` T ) ) --> ( ( mREx ` T ) ^m ( mREx ` T ) ) )
8 ffun 
 |-  ( S : ( ( mREx ` T ) ^pm ( mVR ` T ) ) --> ( ( mREx ` T ) ^m ( mREx ` T ) ) -> Fun S )
9 4 7 8 3syl 
 |-  ( F e. ran S -> Fun S )
10 5 6 1 mrsubrn 
 |-  ran S = ( S " ( ( mREx ` T ) ^m ( mVR ` T ) ) )
11 10 eleq2i 
 |-  ( F e. ran S <-> F e. ( S " ( ( mREx ` T ) ^m ( mVR ` T ) ) ) )
12 11 biimpi 
 |-  ( F e. ran S -> F e. ( S " ( ( mREx ` T ) ^m ( mVR ` T ) ) ) )
13 fvelima 
 |-  ( ( Fun S /\ F e. ( S " ( ( mREx ` T ) ^m ( mVR ` T ) ) ) ) -> E. f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ( S ` f ) = F )
14 9 12 13 syl2anc 
 |-  ( F e. ran S -> E. f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ( S ` f ) = F )
15 elmapi 
 |-  ( f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) -> f : ( mVR ` T ) --> ( mREx ` T ) )
16 15 adantl 
 |-  ( ( T e. _V /\ f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ) -> f : ( mVR ` T ) --> ( mREx ` T ) )
17 ssidd 
 |-  ( ( T e. _V /\ f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ) -> ( mVR ` T ) C_ ( mVR ` T ) )
18 wrd0 
 |-  (/) e. Word ( ( mCN ` T ) u. ( mVR ` T ) )
19 eqid 
 |-  ( mCN ` T ) = ( mCN ` T )
20 19 5 6 mrexval 
 |-  ( T e. _V -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
21 20 adantr 
 |-  ( ( T e. _V /\ f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ) -> ( mREx ` T ) = Word ( ( mCN ` T ) u. ( mVR ` T ) ) )
22 18 21 eleqtrrid 
 |-  ( ( T e. _V /\ f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ) -> (/) e. ( mREx ` T ) )
23 eqid 
 |-  ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) = ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) )
24 19 5 6 1 23 mrsubval 
 |-  ( ( f : ( mVR ` T ) --> ( mREx ` T ) /\ ( mVR ` T ) C_ ( mVR ` T ) /\ (/) e. ( mREx ` T ) ) -> ( ( S ` f ) ` (/) ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. (/) ) ) )
25 16 17 22 24 syl3anc 
 |-  ( ( T e. _V /\ f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ) -> ( ( S ` f ) ` (/) ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. (/) ) ) )
26 co02 
 |-  ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. (/) ) = (/)
27 26 oveq2i 
 |-  ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. (/) ) ) = ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum (/) )
28 23 frmd0 
 |-  (/) = ( 0g ` ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) )
29 28 gsum0 
 |-  ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum (/) ) = (/)
30 27 29 eqtri 
 |-  ( ( freeMnd ` ( ( mCN ` T ) u. ( mVR ` T ) ) ) gsum ( ( v e. ( ( mCN ` T ) u. ( mVR ` T ) ) |-> if ( v e. ( mVR ` T ) , ( f ` v ) , <" v "> ) ) o. (/) ) ) = (/)
31 25 30 eqtrdi 
 |-  ( ( T e. _V /\ f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ) -> ( ( S ` f ) ` (/) ) = (/) )
32 fveq1 
 |-  ( ( S ` f ) = F -> ( ( S ` f ) ` (/) ) = ( F ` (/) ) )
33 32 eqeq1d 
 |-  ( ( S ` f ) = F -> ( ( ( S ` f ) ` (/) ) = (/) <-> ( F ` (/) ) = (/) ) )
34 31 33 syl5ibcom 
 |-  ( ( T e. _V /\ f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ) -> ( ( S ` f ) = F -> ( F ` (/) ) = (/) ) )
35 34 rexlimdva 
 |-  ( T e. _V -> ( E. f e. ( ( mREx ` T ) ^m ( mVR ` T ) ) ( S ` f ) = F -> ( F ` (/) ) = (/) ) )
36 4 14 35 sylc 
 |-  ( F e. ran S -> ( F ` (/) ) = (/) )