Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mrsub Structured version   Unicode version

Definition df-mrsub 29114
Description: Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mrsub  |- mRSubst  =  ( t  e.  _V  |->  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mREx `  t )  |->  ( (freeMnd `  ( (mCN `  t
)  u.  (mVR `  t ) ) ) 
gsumg  ( ( v  e.  ( (mCN `  t
)  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)  o.  e ) ) ) ) )
Distinct variable group:    e, f, t, v

Detailed syntax breakdown of Definition df-mrsub
StepHypRef Expression
1 cmrsub 29094 . 2  class mRSubst
2 vt . . 3  setvar  t
3 cvv 3106 . . 3  class  _V
4 vf . . . 4  setvar  f
52cv 1397 . . . . . 6  class  t
6 cmrex 29090 . . . . . 6  class mREx
75, 6cfv 5570 . . . . 5  class  (mREx `  t )
8 cmvar 29085 . . . . . 6  class mVR
95, 8cfv 5570 . . . . 5  class  (mVR `  t )
10 cpm 7413 . . . . 5  class  ^pm
117, 9, 10co 6270 . . . 4  class  ( (mREx `  t )  ^pm  (mVR `  t ) )
12 ve . . . . 5  setvar  e
13 cmcn 29084 . . . . . . . . 9  class mCN
145, 13cfv 5570 . . . . . . . 8  class  (mCN `  t )
1514, 9cun 3459 . . . . . . 7  class  ( (mCN
`  t )  u.  (mVR `  t )
)
16 cfrmd 16214 . . . . . . 7  class freeMnd
1715, 16cfv 5570 . . . . . 6  class  (freeMnd `  (
(mCN `  t )  u.  (mVR `  t )
) )
18 vv . . . . . . . 8  setvar  v
1918cv 1397 . . . . . . . . . 10  class  v
204cv 1397 . . . . . . . . . . 11  class  f
2120cdm 4988 . . . . . . . . . 10  class  dom  f
2219, 21wcel 1823 . . . . . . . . 9  wff  v  e. 
dom  f
2319, 20cfv 5570 . . . . . . . . 9  class  ( f `
 v )
2419cs1 12521 . . . . . . . . 9  class  <" v ">
2522, 23, 24cif 3929 . . . . . . . 8  class  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
2618, 15, 25cmpt 4497 . . . . . . 7  class  ( v  e.  ( (mCN `  t )  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)
2712cv 1397 . . . . . . 7  class  e
2826, 27ccom 4992 . . . . . 6  class  ( ( v  e.  ( (mCN
`  t )  u.  (mVR `  t )
)  |->  if ( v  e.  dom  f ,  ( f `  v
) ,  <" v "> ) )  o.  e )
29 cgsu 14930 . . . . . 6  class  gsumg
3017, 28, 29co 6270 . . . . 5  class  ( (freeMnd `  ( (mCN `  t
)  u.  (mVR `  t ) ) ) 
gsumg  ( ( v  e.  ( (mCN `  t
)  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)  o.  e ) )
3112, 7, 30cmpt 4497 . . . 4  class  ( e  e.  (mREx `  t
)  |->  ( (freeMnd `  (
(mCN `  t )  u.  (mVR `  t )
) )  gsumg  ( ( v  e.  ( (mCN `  t
)  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)  o.  e ) ) )
324, 11, 31cmpt 4497 . . 3  class  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mREx `  t )  |->  ( (freeMnd `  ( (mCN `  t
)  u.  (mVR `  t ) ) ) 
gsumg  ( ( v  e.  ( (mCN `  t
)  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)  o.  e ) ) ) )
332, 3, 32cmpt 4497 . 2  class  ( t  e.  _V  |->  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mREx `  t )  |->  ( (freeMnd `  ( (mCN `  t
)  u.  (mVR `  t ) ) ) 
gsumg  ( ( v  e.  ( (mCN `  t
)  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)  o.  e ) ) ) ) )
341, 33wceq 1398 1  wff mRSubst  =  ( t  e.  _V  |->  ( f  e.  ( (mREx `  t )  ^pm  (mVR `  t ) )  |->  ( e  e.  (mREx `  t )  |->  ( (freeMnd `  ( (mCN `  t
)  u.  (mVR `  t ) ) ) 
gsumg  ( ( v  e.  ( (mCN `  t
)  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)  o.  e ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  mrsubffval  29131
  Copyright terms: Public domain W3C validator