# 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 𝐶 = ( 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 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )