Metamath Proof Explorer

Theorem mrsubffval

Description: The substitution of some variables for expressions in a raw expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubffval.c ⊢C=mCN⁡T
mrsubffval.v ⊢V=mVR⁡T
mrsubffval.r ⊢R=mREx⁡T
mrsubffval.s ⊢S=mRSubst⁡T
mrsubffval.g ⊢G=freeMnd⁡C∪V
Assertion mrsubffval ⊢T∈W→S=f∈R↑𝑝𝑚V⟼e∈R⟼∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e

Proof

Step Hyp Ref Expression
1 mrsubffval.c ⊢C=mCN⁡T
2 mrsubffval.v ⊢V=mVR⁡T
3 mrsubffval.r ⊢R=mREx⁡T
4 mrsubffval.s ⊢S=mRSubst⁡T
5 mrsubffval.g ⊢G=freeMnd⁡C∪V
6 elex ⊢T∈W→T∈V
7 fveq2 ⊢t=T→mREx⁡t=mREx⁡T
8 7 3 eqtr4di ⊢t=T→mREx⁡t=R
9 fveq2 ⊢t=T→mVR⁡t=mVR⁡T
10 9 2 eqtr4di ⊢t=T→mVR⁡t=V
11 8 10 oveq12d ⊢t=T→mREx⁡t↑𝑝𝑚mVR⁡t=R↑𝑝𝑚V
12 fveq2 ⊢t=T→mCN⁡t=mCN⁡T
13 12 1 eqtr4di ⊢t=T→mCN⁡t=C
14 13 10 uneq12d ⊢t=T→mCN⁡t∪mVR⁡t=C∪V
15 14 fveq2d ⊢t=T→freeMnd⁡mCN⁡t∪mVR⁡t=freeMnd⁡C∪V
16 15 5 eqtr4di ⊢t=T→freeMnd⁡mCN⁡t∪mVR⁡t=G
17 14 mpteq1d ⊢t=T→v∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩=v∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩
18 17 coeq1d ⊢t=T→v∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e=v∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
19 16 18 oveq12d ⊢t=T→∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e=∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
20 8 19 mpteq12dv ⊢t=T→e∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e=e∈R⟼∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
21 11 20 mpteq12dv ⊢t=T→f∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e=f∈R↑𝑝𝑚V⟼e∈R⟼∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
22 df-mrsub ⊢mRSubst=t∈V⟼f∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mREx⁡t⟼∑freeMnd⁡mCN⁡t∪mVR⁡tv∈mCN⁡t∪mVR⁡t⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
23 ovex ⊢R↑𝑝𝑚V∈V
24 23 mptex ⊢f∈R↑𝑝𝑚V⟼e∈R⟼∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e∈V
25 21 22 24 fvmpt ⊢T∈V→mRSubst⁡T=f∈R↑𝑝𝑚V⟼e∈R⟼∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
26 6 25 syl ⊢T∈W→mRSubst⁡T=f∈R↑𝑝𝑚V⟼e∈R⟼∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e
27 4 26 eqtrid ⊢T∈W→S=f∈R↑𝑝𝑚V⟼e∈R⟼∑Gv∈C∪V⟼ifv∈dom⁡ff⁡v⟨“v”⟩∘e