Metamath Proof Explorer

Theorem mrsubval

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 mrsubval ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R → S ⁡ F ⁡ X = ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ X

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 mrsubfval ⊢ F : A ⟶ R ∧ A ⊆ V → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
7 6 3adant3 ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R → S ⁡ F = e ∈ R ⟼ ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e
8 simpr ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R ∧ e = X → e = X
9 8 coeq2d ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R ∧ e = X → v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e = v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ X
10 9 oveq2d ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R ∧ e = X → ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ e = ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ X
11 simp3 ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R → X ∈ R
12 ovexd ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R → ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ X ∈ V
13 7 10 11 12 fvmptd ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ R → S ⁡ F ⁡ X = ∑ G v ∈ C ∪ V ⟼ if v ∈ A F ⁡ v ⟨“ v ”⟩ ∘ X