Metamath Proof Explorer

Theorem selvffval

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 )
Assertion 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 ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 selvffval.i 
 |-  ( ph -> I e. V )
2 selvffval.r 
 |-  ( ph -> R e. W )
3 df-selv 
 |-  selectVars = ( i e. _V , r e. _V |-> ( 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 ) ) ) ) ) ) ) )
4 3 a1i 
 |-  ( ph -> selectVars = ( i e. _V , r e. _V |-> ( 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 pweq 
 |-  ( i = I -> ~P i = ~P I )
6 5 adantr 
 |-  ( ( i = I /\ r = R ) -> ~P i = ~P I )
7 oveq12 
 |-  ( ( i = I /\ r = R ) -> ( i mPoly r ) = ( I mPoly R ) )
8 7 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( Base ` ( i mPoly r ) ) = ( Base ` ( I mPoly R ) ) )
9 difeq1 
 |-  ( i = I -> ( i \ j ) = ( I \ j ) )
10 9 adantr 
 |-  ( ( i = I /\ r = R ) -> ( i \ j ) = ( I \ j ) )
11 simpr 
 |-  ( ( i = I /\ r = R ) -> r = R )
12 10 11 oveq12d 
 |-  ( ( i = I /\ r = R ) -> ( ( i \ j ) mPoly r ) = ( ( I \ j ) mPoly R ) )
13 oveq1 
 |-  ( i = I -> ( i evalSub t ) = ( I evalSub t ) )
14 13 adantr 
 |-  ( ( i = I /\ r = R ) -> ( i evalSub t ) = ( I evalSub t ) )
15 14 fveq1d 
 |-  ( ( i = I /\ r = R ) -> ( ( i evalSub t ) ` ran d ) = ( ( I evalSub t ) ` ran d ) )
16 15 fveq1d 
 |-  ( ( i = I /\ r = R ) -> ( ( ( i evalSub t ) ` ran d ) ` ( d o. f ) ) = ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) )
17 simpl 
 |-  ( ( i = I /\ r = R ) -> i = I )
18 10 11 oveq12d 
 |-  ( ( i = I /\ r = R ) -> ( ( i \ j ) mVar r ) = ( ( I \ j ) mVar R ) )
19 18 fveq1d 
 |-  ( ( i = I /\ r = R ) -> ( ( ( i \ j ) mVar r ) ` x ) = ( ( ( I \ j ) mVar R ) ` x ) )
20 19 fveq2d 
 |-  ( ( i = I /\ r = R ) -> ( c ` ( ( ( i \ j ) mVar r ) ` x ) ) = ( c ` ( ( ( I \ j ) mVar R ) ` x ) ) )
21 20 ifeq2d 
 |-  ( ( i = I /\ r = R ) -> 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 ) ) ) )
22 17 21 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( 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 ) ) ) ) )
23 16 22 fveq12d 
 |-  ( ( i = I /\ r = R ) -> ( ( ( ( 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 ) ) ) ) ) )
24 23 csbeq2dv 
 |-  ( ( i = I /\ r = R ) -> [_ ( 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 ) ) ) ) ) )
25 24 csbeq2dv 
 |-  ( ( i = I /\ r = R ) -> [_ ( 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 ) ) ) ) ) )
26 25 csbeq2dv 
 |-  ( ( i = I /\ r = R ) -> [_ ( 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 ) ) ) ) ) )
27 12 26 csbeq12dv 
 |-  ( ( i = I /\ r = 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 ) ) ) ) ) = [_ ( ( 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 ) ) ) ) ) )
28 8 27 mpteq12dv 
 |-  ( ( i = I /\ r = R ) -> ( 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 ) ) ) ) ) ) )
29 6 28 mpteq12dv 
 |-  ( ( i = I /\ r = 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 ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) ) )
30 29 adantl 
 |-  ( ( ph /\ ( i = I /\ r = 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 ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) ) )
31 1 elexd 
 |-  ( ph -> I e. _V )
32 2 elexd 
 |-  ( ph -> R e. _V )
33 1 pwexd 
 |-  ( ph -> ~P I e. _V )
34 33 mptexd 
 |-  ( ph -> ( 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 ) ) ) ) ) ) ) e. _V )
35 4 30 31 32 34 ovmpod 
 |-  ( 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 ) ) ) ) ) ) ) )