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 ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ 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 ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ = v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩
18 17 coeq1d ⊢ t = T → v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e = v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
19 16 18 oveq12d ⊢ t = T → ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e = ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
20 8 19 mpteq12dv ⊢ t = T → e ∈ mREx ⁡ t ⟼ ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
21 11 20 mpteq12dv ⊢ t = T → f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mREx ⁡ t ⟼ ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
22 df-mrsub ⊢ mRSubst = t ∈ V ⟼ f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mREx ⁡ t ⟼ ∑ freeMnd ⁡ mCN ⁡ t ∪ mVR ⁡ t v ∈ mCN ⁡ t ∪ mVR ⁡ t ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
23 ovex ⊢ R ↑ 𝑝𝑚 V ∈ V
24 23 mptex ⊢ f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e ∈ V
25 21 22 24 fvmpt ⊢ T ∈ V → mRSubst ⁡ T = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
26 6 25 syl ⊢ T ∈ W → mRSubst ⁡ T = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
27 4 26 syl5eq ⊢ T ∈ W → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e