Metamath Proof Explorer

Definition df-mrsub

Description: Define a substitution of raw expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mrsub 
|- mRSubst = ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmrsub 
 |-  mRSubst
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vf 
 |-  f
4 cmrex 
 |-  mREx
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mREx ` t )
7 cpm 
 |-  ^pm
8 cmvar 
 |-  mVR
9 5 8 cfv 
 |-  ( mVR ` t )
10 6 9 7 co 
 |-  ( ( mREx ` t ) ^pm ( mVR ` t ) )
11 ve 
 |-  e
12 cfrmd 
 |-  freeMnd
13 cmcn 
 |-  mCN
14 5 13 cfv 
 |-  ( mCN ` t )
15 14 9 cun 
 |-  ( ( mCN ` t ) u. ( mVR ` t ) )
16 15 12 cfv 
 |-  ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) )
17 cgsu 
 |-  gsum
18 vv 
 |-  v
19 18 cv 
 |-  v
20 3 cv 
 |-  f
21 20 cdm 
 |-  dom f
22 19 21 wcel 
 |-  v e. dom f
23 19 20 cfv 
 |-  ( f ` v )
24 19 cs1 
 |-  <" v ">
25 22 23 24 cif 
 |-  if ( v e. dom f , ( f ` v ) , <" v "> )
26 18 15 25 cmpt 
 |-  ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) )
27 11 cv 
 |-  e
28 26 27 ccom 
 |-  ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e )
29 16 28 17 co 
 |-  ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) )
30 11 6 29 cmpt 
 |-  ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) )
31 3 10 30 cmpt 
 |-  ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) )
32 1 2 31 cmpt 
 |-  ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )
33 0 32 wceq 
 |-  mRSubst = ( t e. _V |-> ( f e. ( ( mREx ` t ) ^pm ( mVR ` t ) ) |-> ( e e. ( mREx ` t ) |-> ( ( freeMnd ` ( ( mCN ` t ) u. ( mVR ` t ) ) ) gsum ( ( v e. ( ( mCN ` t ) u. ( mVR ` t ) ) |-> if ( v e. dom f , ( f ` v ) , <" v "> ) ) o. e ) ) ) ) )