Step | Hyp | Ref
| Expression |
1 | | mrsubffval.s |
. 2
β’ π = (mRSubstβπ) |
2 | | elex 3465 |
. . 3
β’ (π β π β π β V) |
3 | | fveq2 6846 |
. . . . . . 7
β’ (π‘ = π β (mRExβπ‘) = (mRExβπ)) |
4 | | mrsubffval.r |
. . . . . . 7
β’ π
= (mRExβπ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . 6
β’ (π‘ = π β (mRExβπ‘) = π
) |
6 | | fveq2 6846 |
. . . . . . 7
β’ (π‘ = π β (mVRβπ‘) = (mVRβπ)) |
7 | | mrsubffval.v |
. . . . . . 7
β’ π = (mVRβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . 6
β’ (π‘ = π β (mVRβπ‘) = π) |
9 | 5, 8 | oveq12d 7379 |
. . . . 5
β’ (π‘ = π β ((mRExβπ‘) βpm (mVRβπ‘)) = (π
βpm π)) |
10 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π‘ = π β (mCNβπ‘) = (mCNβπ)) |
11 | | mrsubffval.c |
. . . . . . . . . . 11
β’ πΆ = (mCNβπ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π‘ = π β (mCNβπ‘) = πΆ) |
13 | 12, 8 | uneq12d 4128 |
. . . . . . . . 9
β’ (π‘ = π β ((mCNβπ‘) βͺ (mVRβπ‘)) = (πΆ βͺ π)) |
14 | 13 | fveq2d 6850 |
. . . . . . . 8
β’ (π‘ = π β (freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) = (freeMndβ(πΆ βͺ π))) |
15 | | mrsubffval.g |
. . . . . . . 8
β’ πΊ = (freeMndβ(πΆ βͺ π)) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . . 7
β’ (π‘ = π β (freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) = πΊ) |
17 | 13 | mpteq1d 5204 |
. . . . . . . 8
β’ (π‘ = π β (π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) = (π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©))) |
18 | 17 | coeq1d 5821 |
. . . . . . 7
β’ (π‘ = π β ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π) = ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)) |
19 | 16, 18 | oveq12d 7379 |
. . . . . 6
β’ (π‘ = π β ((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g
((π£ β
((mCNβπ‘) βͺ
(mVRβπ‘)) β¦
if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)) = (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))) |
20 | 5, 19 | mpteq12dv 5200 |
. . . . 5
β’ (π‘ = π β (π β (mRExβπ‘) β¦ ((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g
((π£ β
((mCNβπ‘) βͺ
(mVRβπ‘)) β¦
if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))) = (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)))) |
21 | 9, 20 | mpteq12dv 5200 |
. . . 4
β’ (π‘ = π β (π β ((mRExβπ‘) βpm (mVRβπ‘)) β¦ (π β (mRExβπ‘) β¦ ((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g
((π£ β
((mCNβπ‘) βͺ
(mVRβπ‘)) β¦
if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)))) = (π β (π
βpm π) β¦ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |
22 | | df-mrsub 34148 |
. . . 4
β’ mRSubst =
(π‘ β V β¦ (π β ((mRExβπ‘) βpm
(mVRβπ‘)) β¦
(π β (mRExβπ‘) β¦
((freeMndβ((mCNβπ‘) βͺ (mVRβπ‘))) Ξ£g ((π£ β ((mCNβπ‘) βͺ (mVRβπ‘)) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |
23 | | ovex 7394 |
. . . . 5
β’ (π
βpm π) β V |
24 | 23 | mptex 7177 |
. . . 4
β’ (π β (π
βpm π) β¦ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)))) β V |
25 | 21, 22, 24 | fvmpt 6952 |
. . 3
β’ (π β V β
(mRSubstβπ) = (π β (π
βpm π) β¦ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |
26 | 2, 25 | syl 17 |
. 2
β’ (π β π β (mRSubstβπ) = (π β (π
βpm π) β¦ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |
27 | 1, 26 | eqtrid 2785 |
1
β’ (π β π β π = (π β (π
βpm π) β¦ (π β π
β¦ (πΊ Ξ£g ((π£ β (πΆ βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))))) |