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	⊢ 𝐶 = ( mCN ‘ 𝑇 )
	mrsubffval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrsubffval.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	mrsubffval.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
	mrsubffval.g	⊢ 𝐺 = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) )
Assertion	mrsubffval	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )

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		elex	⊢ ( 𝑇 ∈ 𝑊 → 𝑇 ∈ V )
7		fveq2	⊢ ( 𝑡 = 𝑇 → ( mREx ‘ 𝑡 ) = ( mREx ‘ 𝑇 ) )
8	7 3	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mREx ‘ 𝑡 ) = 𝑅 )
9		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = ( mVR ‘ 𝑇 ) )
10	9 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = 𝑉 )
11	8 10	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) ) = ( 𝑅 ↑pm 𝑉 ) )
12		fveq2	⊢ ( 𝑡 = 𝑇 → ( mCN ‘ 𝑡 ) = ( mCN ‘ 𝑇 ) )
13	12 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mCN ‘ 𝑡 ) = 𝐶 )
14	13 10	uneq12d	⊢ ( 𝑡 = 𝑇 → ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) = ( 𝐶 ∪ 𝑉 ) )
15	14	fveq2d	⊢ ( 𝑡 = 𝑇 → ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) )
16	15 5	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) = 𝐺 )
17	14	mpteq1d	⊢ ( 𝑡 = 𝑇 → ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) )
18	17	coeq1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) = ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) )
19	16 18	oveq12d	⊢ ( 𝑡 = 𝑇 → ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) = ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) )
20	8 19	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) = ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
21	11 20	mpteq12dv	⊢ ( 𝑡 = 𝑇 → ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
22		df-mrsub	⊢ mRSubst = ( 𝑡 ∈ V ↦ ( 𝑓 ∈ ( ( mREx ‘ 𝑡 ) ↑pm ( mVR ‘ 𝑡 ) ) ↦ ( 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑡 ) ∪ ( mVR ‘ 𝑡 ) ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
23		ovex	⊢ ( 𝑅 ↑pm 𝑉 ) ∈ V
24	23	mptex	⊢ ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) ∈ V
25	21 22 24	fvmpt	⊢ ( 𝑇 ∈ V → ( mRSubst ‘ 𝑇 ) = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
26	6 25	syl	⊢ ( 𝑇 ∈ 𝑊 → ( mRSubst ‘ 𝑇 ) = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
27	4 26	syl5eq	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ 𝑅 ↦ ( 𝐺 Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )