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

Definition df-mrsub 30128
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 30108 . 2  class mRSubst
2 vt . . 3  setvar  t
3 cvv 3045 . . 3  class  _V
4 vf . . . 4  setvar  f
52cv 1443 . . . . . 6  class  t
6 cmrex 30104 . . . . . 6  class mREx
75, 6cfv 5582 . . . . 5  class  (mREx `  t )
8 cmvar 30099 . . . . . 6  class mVR
95, 8cfv 5582 . . . . 5  class  (mVR `  t )
10 cpm 7473 . . . . 5  class  ^pm
117, 9, 10co 6290 . . . 4  class  ( (mREx `  t )  ^pm  (mVR `  t ) )
12 ve . . . . 5  setvar  e
13 cmcn 30098 . . . . . . . . 9  class mCN
145, 13cfv 5582 . . . . . . . 8  class  (mCN `  t )
1514, 9cun 3402 . . . . . . 7  class  ( (mCN
`  t )  u.  (mVR `  t )
)
16 cfrmd 16631 . . . . . . 7  class freeMnd
1715, 16cfv 5582 . . . . . 6  class  (freeMnd `  (
(mCN `  t )  u.  (mVR `  t )
) )
18 vv . . . . . . . 8  setvar  v
1918cv 1443 . . . . . . . . . 10  class  v
204cv 1443 . . . . . . . . . . 11  class  f
2120cdm 4834 . . . . . . . . . 10  class  dom  f
2219, 21wcel 1887 . . . . . . . . 9  wff  v  e. 
dom  f
2319, 20cfv 5582 . . . . . . . . 9  class  ( f `
 v )
2419cs1 12659 . . . . . . . . 9  class  <" v ">
2522, 23, 24cif 3881 . . . . . . . 8  class  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
2618, 15, 25cmpt 4461 . . . . . . 7  class  ( v  e.  ( (mCN `  t )  u.  (mVR `  t ) )  |->  if ( v  e.  dom  f ,  ( f `  v ) ,  <" v "> )
)
2712cv 1443 . . . . . . 7  class  e
2826, 27ccom 4838 . . . . . 6  class  ( ( v  e.  ( (mCN
`  t )  u.  (mVR `  t )
)  |->  if ( v  e.  dom  f ,  ( f `  v
) ,  <" v "> ) )  o.  e )
29 cgsu 15339 . . . . . 6  class  gsumg
3017, 28, 29co 6290 . . . . 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 4461 . . . 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 4461 . . 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 4461 . 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 1444 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  30145
  Copyright terms: Public domain W3C validator