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	⊢ 𝐶 = ( mCN ‘ 𝑇 )
	mrsubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrsubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	mrsubffval.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
	mrsubffval.g	⊢ 𝐺 = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) )
Assertion	mrsubval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mrsubffval.c	⊢ 𝐶 = ( mCN ‘ 𝑇 )
2		mrsubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
3		mrsubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
4		mrsubffval.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
5		mrsubffval.g	⊢ 𝐺 = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) )
6	1 2 3 4 5	mrsubfval	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
7	6	3adant3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) → ( 𝑆 ‘ 𝐹 ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
8		simpr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) ∧ 𝑒 = 𝑋 ) → 𝑒 = 𝑋 )
9	8	coeq2d	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) ∧ 𝑒 = 𝑋 ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) = ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) )
10	9	oveq2d	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) ∧ 𝑒 = 𝑋 ) → ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) = ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) )
11		simp3	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) → 𝑋 ∈ 𝑅 )
12		ovexd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) → ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) ∈ V )
13	7 10 11 12	fvmptd	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑋 ) ) )