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 eqtrdi ⊢ 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 ⁡ ∅ = ∅