Metamath Proof Explorer

Theorem selvval

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

Ref Expression
Hypotheses selvval.p 
|- P = ( I mPoly R )
selvval.b 
|- B = ( Base ` P )
selvval.u 
|- U = ( ( I \ J ) mPoly R )
selvval.t 
|- T = ( J mPoly U )
selvval.c 
|- C = ( algSc ` T )
selvval.d 
|- D = ( C o. ( algSc ` U ) )
selvval.i 
|- ( ph -> I e. V )
selvval.r 
|- ( ph -> R e. W )
selvval.j 
|- ( ph -> J C_ I )
selvval.f 
|- ( ph -> F e. B )
Assertion selvval 
|- ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( ( 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 selvval.p 
 |-  P = ( I mPoly R )
2 selvval.b 
 |-  B = ( Base ` P )
3 selvval.u 
 |-  U = ( ( I \ J ) mPoly R )
4 selvval.t 
 |-  T = ( J mPoly U )
5 selvval.c 
 |-  C = ( algSc ` T )
6 selvval.d 
 |-  D = ( C o. ( algSc ` U ) )
7 selvval.i 
 |-  ( ph -> I e. V )
8 selvval.r 
 |-  ( ph -> R e. W )
9 selvval.j 
 |-  ( ph -> J C_ I )
10 selvval.f 
 |-  ( ph -> F e. B )
11 7 8 9 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 ) ) ) ) ) ) )
12 coeq2 
 |-  ( f = F -> ( d o. f ) = ( d o. F ) )
13 12 fveq2d 
 |-  ( f = F -> ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) = ( ( ( I evalSub t ) ` ran d ) ` ( d o. F ) ) )
14 13 fveq1d 
 |-  ( f = F -> ( ( ( ( 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 ) ) ) ) ) )
15 14 csbeq2dv 
 |-  ( f = F -> [_ ( 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 ) ) ) ) ) )
16 15 csbeq2dv 
 |-  ( f = F -> [_ ( 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 ) ) ) ) ) )
17 16 csbeq2dv 
 |-  ( f = F -> [_ ( 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 ) ) ) ) ) )
18 17 csbeq2dv 
 |-  ( f = F -> [_ ( ( 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 ) ) ) ) ) )
19 18 adantl 
 |-  ( ( ph /\ f = F ) -> [_ ( ( 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 ) ) ) ) ) )
20 1 fveq2i 
 |-  ( Base ` P ) = ( Base ` ( I mPoly R ) )
21 2 20 eqtri 
 |-  B = ( Base ` ( I mPoly R ) )
22 10 21 eleqtrdi 
 |-  ( ph -> F e. ( Base ` ( I mPoly R ) ) )
23 fvex 
 |-  ( ( ( ( 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
24 23 csbex 
 |-  [_ ( 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
25 24 csbex 
 |-  [_ ( 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 25 csbex 
 |-  [_ ( 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 26 csbex 
 |-  [_ ( ( 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
28 27 a1i 
 |-  ( ph -> [_ ( ( 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 )
29 11 19 22 28 fvmptd 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = [_ ( ( 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 ovex 
 |-  ( ( I \ J ) mPoly R ) e. _V
31 3 eqeq2i 
 |-  ( u = U <-> u = ( ( I \ J ) mPoly R ) )
32 oveq2 
 |-  ( u = U -> ( J mPoly u ) = ( J mPoly U ) )
33 fveq2 
 |-  ( u = U -> ( algSc ` u ) = ( algSc ` U ) )
34 33 coeq2d 
 |-  ( u = U -> ( c o. ( algSc ` u ) ) = ( c o. ( algSc ` U ) ) )
35 oveq2 
 |-  ( u = U -> ( J mVar u ) = ( J mVar U ) )
36 35 fveq1d 
 |-  ( u = U -> ( ( J mVar u ) ` x ) = ( ( J mVar U ) ` x ) )
37 36 ifeq1d 
 |-  ( u = U -> 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 ) ) ) )
38 37 mpteq2dv 
 |-  ( u = U -> ( 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 ) ) ) ) )
39 38 fveq2d 
 |-  ( u = U -> ( ( ( ( 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 ) ) ) ) ) )
40 34 39 csbeq12dv 
 |-  ( u = U -> [_ ( 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 ) ) ) ) ) )
41 40 csbeq2dv 
 |-  ( u = U -> [_ ( 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 ) ) ) ) ) )
42 32 41 csbeq12dv 
 |-  ( u = 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 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 ) ) ) ) ) )
43 ovex 
 |-  ( J mPoly U ) e. _V
44 4 eqeq2i 
 |-  ( t = T <-> t = ( J mPoly U ) )
45 fveq2 
 |-  ( t = T -> ( algSc ` t ) = ( algSc ` T ) )
46 oveq2 
 |-  ( t = T -> ( I evalSub t ) = ( I evalSub T ) )
47 46 fveq1d 
 |-  ( t = T -> ( ( I evalSub t ) ` ran d ) = ( ( I evalSub T ) ` ran d ) )
48 47 fveq1d 
 |-  ( t = T -> ( ( ( I evalSub t ) ` ran d ) ` ( d o. F ) ) = ( ( ( I evalSub T ) ` ran d ) ` ( d o. F ) ) )
49 48 fveq1d 
 |-  ( t = T -> ( ( ( ( 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 ) ) ) ) ) )
50 49 csbeq2dv 
 |-  ( t = T -> [_ ( 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 ) ) ) ) ) )
51 45 50 csbeq12dv 
 |-  ( t = 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 ) ) ) ) ) = [_ ( 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 ) ) ) ) ) )
52 fvex 
 |-  ( algSc ` T ) e. _V
53 5 eqeq2i 
 |-  ( c = C <-> c = ( algSc ` T ) )
54 coeq1 
 |-  ( c = C -> ( c o. ( algSc ` U ) ) = ( C o. ( algSc ` U ) ) )
55 fveq1 
 |-  ( c = C -> ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) = ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) )
56 55 ifeq2d 
 |-  ( c = C -> 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 ) ) ) )
57 56 mpteq2dv 
 |-  ( c = C -> ( 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 ) ) ) ) )
58 57 fveq2d 
 |-  ( c = C -> ( ( ( ( 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 ) ) ) ) ) )
59 54 58 csbeq12dv 
 |-  ( c = 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 ) ) ) ) ) = [_ ( 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 ) ) ) ) ) )
60 5 fvexi 
 |-  C e. _V
61 fvex 
 |-  ( algSc ` U ) e. _V
62 60 61 coex 
 |-  ( C o. ( algSc ` U ) ) e. _V
63 6 eqeq2i 
 |-  ( d = D <-> d = ( C o. ( algSc ` U ) ) )
64 rneq 
 |-  ( d = D -> ran d = ran D )
65 64 fveq2d 
 |-  ( d = D -> ( ( I evalSub T ) ` ran d ) = ( ( I evalSub T ) ` ran D ) )
66 coeq1 
 |-  ( d = D -> ( d o. F ) = ( D o. F ) )
67 65 66 fveq12d 
 |-  ( d = D -> ( ( ( I evalSub T ) ` ran d ) ` ( d o. F ) ) = ( ( ( I evalSub T ) ` ran D ) ` ( D o. F ) ) )
68 67 fveq1d 
 |-  ( d = 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
69 63 68 sylbir 
 |-  ( d = ( C o. ( algSc ` U ) ) -> ( ( ( ( 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 ) ) ) ) ) )
70 62 69 csbie 
 |-  [_ ( 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) )
71 59 70 eqtrdi 
 |-  ( c = 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
72 53 71 sylbir 
 |-  ( c = ( algSc ` T ) -> [_ ( 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
73 52 72 csbie 
 |-  [_ ( 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) )
74 51 73 eqtrdi 
 |-  ( t = 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
75 44 74 sylbir 
 |-  ( t = ( J mPoly U ) -> [_ ( 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
76 43 75 csbie 
 |-  [_ ( 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) )
77 42 76 eqtrdi 
 |-  ( u = 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
78 31 77 sylbir 
 |-  ( u = ( ( I \ J ) mPoly 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 ) ) ) ) ) = ( ( ( ( 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 ) ) ) ) ) )
79 30 78 csbie 
 |-  [_ ( ( 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 evalSub T ) ` ran D ) ` ( D o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) )
80 29 79 eqtrdi 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( ( 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 ) ) ) ) ) )