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 ran S F =

Proof

Step Hyp Ref Expression
1 mrsubccat.s S = mRSubst T
2 n0i F ran S ¬ ran S =
3 1 rnfvprc ¬ T V ran S =
4 2 3 nsyl2 F ran S T V
5 eqid mVR T = mVR T
6 eqid mREx T = mREx T
7 5 6 1 mrsubff T V S : mREx T 𝑝𝑚 mVR T mREx T mREx T
8 ffun S : mREx T 𝑝𝑚 mVR T mREx T mREx T Fun S
9 4 7 8 3syl F ran S Fun S
10 5 6 1 mrsubrn ran S = S mREx T mVR T
11 10 eleq2i F ran S F S mREx T mVR T
12 11 biimpi F ran S F S mREx T mVR T
13 fvelima Fun S F S mREx T mVR T f mREx T mVR T S f = F
14 9 12 13 syl2anc F ran S f mREx T mVR T S f = F
15 elmapi f mREx T mVR T f : mVR T mREx T
16 15 adantl T V f mREx T mVR T f : mVR T mREx T
17 ssidd T V f mREx T mVR T mVR T mVR T
18 wrd0 Word mCN T mVR T
19 eqid mCN T = mCN T
20 19 5 6 mrexval T V mREx T = Word mCN T mVR T
21 20 adantr T V f mREx T mVR T mREx T = Word mCN T mVR T
22 18 21 eleqtrrid T V f mREx T mVR T mREx T
23 eqid freeMnd mCN T mVR T = freeMnd mCN T mVR T
24 19 5 6 1 23 mrsubval f : mVR T mREx T mVR T mVR T mREx T S f = freeMnd mCN T mVR T v mCN T mVR T if v mVR T f v ⟨“ v ”⟩
25 16 17 22 24 syl3anc T V f mREx T mVR T S f = freeMnd mCN T mVR T v mCN T mVR T if v mVR T f v ⟨“ v ”⟩
26 co02 v mCN T mVR T if v mVR T f v ⟨“ v ”⟩ =
27 26 oveq2i freeMnd mCN T mVR T v mCN T mVR T if v mVR T f v ⟨“ v ”⟩ = freeMnd mCN T mVR T
28 23 frmd0 = 0 freeMnd mCN T mVR T
29 28 gsum0 freeMnd mCN T mVR T =
30 27 29 eqtri freeMnd mCN T mVR T v mCN T mVR T if v mVR T f v ⟨“ v ”⟩ =
31 25 30 syl6eq T V f mREx T 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 V f mREx T mVR T S f = F F =
35 34 rexlimdva T V f mREx T mVR T S f = F F =
36 4 14 35 sylc F ran S F =