Metamath Proof Explorer

Theorem mrsubfval

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 mrsubfval ⊢ F : A ⟶ R ∧ A ⊆ V → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A 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 1 2 3 4 5 mrsubffval ⊢ T ∈ V → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
7 6 adantr ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e
8 dmeq ⊢ f = F → dom ⁡ f = dom ⁡ F
9 fdm ⊢ F : A ⟶ R → dom ⁡ F = A
10 9 ad2antrl ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → dom ⁡ F = A
11 8 10 sylan9eqr ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → dom ⁡ f = A
12 11 eleq2d ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → v ∈ dom ⁡ f ↔ v ∈ A
13 simpr ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → f = F
14 13 fveq1d ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → f ⁡ v = F ⁡ v
15 12 14 ifbieq1d ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ = if v ∈ A F ⁡ v ⟨“ v ”⟩
16 15 mpteq2dv ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ = v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩
17 16 coeq1d ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e = v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
18 17 oveq2d ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e = ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
19 18 mpteq2dv ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V ∧ f = F → e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ dom ⁡ f f ⁡ v ⟨“ v ”⟩ ∘ e = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
20 3 fvexi ⊢ R ∈ V
21 20 a1i ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → R ∈ V
22 2 fvexi ⊢ V ∈ V
23 22 a1i ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → V ∈ V
24 simprl ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → F : A ⟶ R
25 simprr ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → A ⊆ V
26 elpm2r ⊢ R ∈ V ∧ V ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → F ∈ R ↑ 𝑝𝑚 V
27 21 23 24 25 26 syl22anc ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → F ∈ R ↑ 𝑝𝑚 V
28 20 mptex ⊢ e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e ∈ V
29 28 a1i ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e ∈ V
30 7 19 27 29 fvmptd ⊢ T ∈ V ∧ F : A ⟶ R ∧ A ⊆ V → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
31 30 ex ⊢ T ∈ V → F : A ⟶ R ∧ A ⊆ V → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
32 0fv ⊢ ∅ ⁡ F = ∅
33 fvprc ⊢ ¬ T ∈ V → mRSubst ⁡ T = ∅
34 4 33 eqtrid ⊢ ¬ T ∈ V → S = ∅
35 34 fveq1d ⊢ ¬ T ∈ V → S ⁡ F = ∅ ⁡ F
36 fvprc ⊢ ¬ T ∈ V → mREx ⁡ T = ∅
37 3 36 eqtrid ⊢ ¬ T ∈ V → R = ∅
38 37 mpteq1d ⊢ ¬ T ∈ V → e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e = e ∈ ∅ ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
39 mpt0 ⊢ e ∈ ∅ ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e = ∅
40 38 39 eqtrdi ⊢ ¬ T ∈ V → e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e = ∅
41 32 35 40 3eqtr4a ⊢ ¬ T ∈ V → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
42 41 a1d ⊢ ¬ T ∈ V → F : A ⟶ R ∧ A ⊆ V → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
43 31 42 pm2.61i ⊢ F : A ⟶ R ∧ A ⊆ V → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e