Metamath Proof Explorer

Theorem selvfval

Description: Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023)

Ref Expression
Hypotheses selvffval.i 
|- ( ph -> I e. V )
selvffval.r 
|- ( ph -> R e. W )
selvfval.j 
|- ( ph -> J C_ I )
Assertion selvfval 
|- ( ph -> ( ( I selectVars R ) ` J ) = ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ J ) mPoly R ) / u ]_ [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 selvffval.i 
 |-  ( ph -> I e. V )
2 selvffval.r 
 |-  ( ph -> R e. W )
3 selvfval.j 
 |-  ( ph -> J C_ I )
4 1 2 selvffval 
 |-  ( ph -> ( I selectVars R ) = ( j e. ~P I |-> ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ j ) mPoly R ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) ) ) )
5 difeq2 
 |-  ( j = J -> ( I \ j ) = ( I \ J ) )
6 5 oveq1d 
 |-  ( j = J -> ( ( I \ j ) mPoly R ) = ( ( I \ J ) mPoly R ) )
7 oveq1 
 |-  ( j = J -> ( j mPoly u ) = ( J mPoly u ) )
8 eleq2 
 |-  ( j = J -> ( x e. j <-> x e. J ) )
9 oveq1 
 |-  ( j = J -> ( j mVar u ) = ( J mVar u ) )
10 9 fveq1d 
 |-  ( j = J -> ( ( j mVar u ) ` x ) = ( ( J mVar u ) ` x ) )
11 5 oveq1d 
 |-  ( j = J -> ( ( I \ j ) mVar R ) = ( ( I \ J ) mVar R ) )
12 11 fveq1d 
 |-  ( j = J -> ( ( ( I \ j ) mVar R ) ` x ) = ( ( ( I \ J ) mVar R ) ` x ) )
13 12 fveq2d 
 |-  ( j = J -> ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) = ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) )
14 8 10 13 ifbieq12d 
 |-  ( j = J -> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) = if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) )
15 14 mpteq2dv 
 |-  ( j = J -> ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) = ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) )
16 15 fveq2d 
 |-  ( j = J -> ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) = ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
17 16 csbeq2dv 
 |-  ( j = J -> [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) = [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
18 17 csbeq2dv 
 |-  ( j = J -> [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) = [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
19 7 18 csbeq12dv 
 |-  ( j = J -> [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) = [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
20 6 19 csbeq12dv 
 |-  ( j = J -> [_ ( ( I \ j ) mPoly R ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) = [_ ( ( I \ J ) mPoly R ) / u ]_ [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
21 20 mpteq2dv 
 |-  ( j = J -> ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ j ) mPoly R ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) ) = ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ J ) mPoly R ) / u ]_ [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )
22 21 adantl 
 |-  ( ( ph /\ j = J ) -> ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ j ) mPoly R ) / u ]_ [_ ( j mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. j , ( ( j mVar u ) ` x ) , ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) ) ) ) ) = ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ J ) mPoly R ) / u ]_ [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )
23 1 3 sselpwd 
 |-  ( ph -> J e. ~P I )
24 fvex 
 |-  ( Base ` ( I mPoly R ) ) e. _V
25 mptexg 
 |-  ( ( Base ` ( I mPoly R ) ) e. _V -> ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ J ) mPoly R ) / u ]_ [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) e. _V )
26 24 25 mp1i 
 |-  ( ph -> ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ J ) mPoly R ) / u ]_ [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) e. _V )
27 4 22 23 26 fvmptd 
 |-  ( ph -> ( ( I selectVars R ) ` J ) = ( f e. ( Base ` ( I mPoly R ) ) |-> [_ ( ( I \ J ) mPoly R ) / u ]_ [_ ( J mPoly u ) / t ]_ [_ ( algSc ` t ) / c ]_ [_ ( c o. ( algSc ` u ) ) / d ]_ ( ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar u ) ` x ) , ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )