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.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.j 
 |-  ( ph -> J C_ I )
8 selvval.f 
 |-  ( ph -> F e. B )
9 coeq2 
 |-  ( f = F -> ( d o. f ) = ( d o. F ) )
10 9 fveq2d 
 |-  ( f = F -> ( ( ( I evalSub t ) ` ran d ) ` ( d o. f ) ) = ( ( ( I evalSub t ) ` ran d ) ` ( d o. F ) ) )
11 10 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 ) ) ) ) ) )
12 11 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 ) ) ) ) ) )
13 12 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 ) ) ) ) ) )
14 13 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 ) ) ) ) ) )
15 14 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 ) ) ) ) ) )
16 reldmmpl 
 |-  Rel dom mPoly
17 16 1 2 elbasov 
 |-  ( F e. B -> ( I e. _V /\ R e. _V ) )
18 8 17 syl 
 |-  ( ph -> ( I e. _V /\ R e. _V ) )
19 18 simpld 
 |-  ( ph -> I e. _V )
20 18 simprd 
 |-  ( ph -> R e. _V )
21 19 20 7 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 ) ) ) ) ) ) )
22 1 fveq2i 
 |-  ( Base ` P ) = ( Base ` ( I mPoly R ) )
23 2 22 eqtri 
 |-  B = ( Base ` ( I mPoly R ) )
24 8 23 eleqtrdi 
 |-  ( ph -> F e. ( Base ` ( I mPoly R ) ) )
25 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
26 25 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
27 26 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
28 27 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
29 28 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
30 29 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 )
31 15 21 24 30 fvmptd4 
 |-  ( 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 ) ) ) ) ) )
32 ovex 
 |-  ( ( I \ J ) mPoly R ) e. _V
33 3 eqeq2i 
 |-  ( u = U <-> u = ( ( I \ J ) mPoly R ) )
34 oveq2 
 |-  ( u = U -> ( J mPoly u ) = ( J mPoly U ) )
35 fveq2 
 |-  ( u = U -> ( algSc ` u ) = ( algSc ` U ) )
36 35 coeq2d 
 |-  ( u = U -> ( c o. ( algSc ` u ) ) = ( c o. ( algSc ` U ) ) )
37 oveq2 
 |-  ( u = U -> ( J mVar u ) = ( J mVar U ) )
38 37 fveq1d 
 |-  ( u = U -> ( ( J mVar u ) ` x ) = ( ( J mVar U ) ` x ) )
39 38 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 ) ) ) )
40 39 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 ) ) ) ) )
41 40 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 ) ) ) ) ) )
42 36 41 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 ) ) ) ) ) )
43 42 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 ) ) ) ) ) )
44 34 43 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 ) ) ) ) ) )
45 ovex 
 |-  ( J mPoly U ) e. _V
46 4 eqeq2i 
 |-  ( t = T <-> t = ( J mPoly U ) )
47 fveq2 
 |-  ( t = T -> ( algSc ` t ) = ( algSc ` T ) )
48 oveq2 
 |-  ( t = T -> ( I evalSub t ) = ( I evalSub T ) )
49 48 fveq1d 
 |-  ( t = T -> ( ( I evalSub t ) ` ran d ) = ( ( I evalSub T ) ` ran d ) )
50 49 fveq1d 
 |-  ( t = T -> ( ( ( I evalSub t ) ` ran d ) ` ( d o. F ) ) = ( ( ( I evalSub T ) ` ran d ) ` ( d o. F ) ) )
51 50 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 ) ) ) ) ) )
52 51 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 ) ) ) ) ) )
53 47 52 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 ) ) ) ) ) )
54 fvex 
 |-  ( algSc ` T ) e. _V
55 5 eqeq2i 
 |-  ( c = C <-> c = ( algSc ` T ) )
56 coeq1 
 |-  ( c = C -> ( c o. ( algSc ` U ) ) = ( C o. ( algSc ` U ) ) )
57 fveq1 
 |-  ( c = C -> ( c ` ( ( ( I \ J ) mVar R ) ` x ) ) = ( C ` ( ( ( I \ J ) mVar R ) ` x ) ) )
58 57 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 ) ) ) )
59 58 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 ) ) ) ) )
60 59 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 ) ) ) ) ) )
61 56 60 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 ) ) ) ) ) )
62 5 fvexi 
 |-  C e. _V
63 fvex 
 |-  ( algSc ` U ) e. _V
64 62 63 coex 
 |-  ( C o. ( algSc ` U ) ) e. _V
65 6 eqeq2i 
 |-  ( d = D <-> d = ( C o. ( algSc ` U ) ) )
66 rneq 
 |-  ( d = D -> ran d = ran D )
67 66 fveq2d 
 |-  ( d = D -> ( ( I evalSub T ) ` ran d ) = ( ( I evalSub T ) ` ran D ) )
68 coeq1 
 |-  ( d = D -> ( d o. F ) = ( D o. F ) )
69 67 68 fveq12d 
 |-  ( d = D -> ( ( ( I evalSub T ) ` ran d ) ` ( d o. F ) ) = ( ( ( I evalSub T ) ` ran D ) ` ( D o. F ) ) )
70 69 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 ) ) ) ) ) )
71 65 70 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 ) ) ) ) ) )
72 64 71 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 ) ) ) ) )
73 61 72 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 ) ) ) ) ) )
74 55 73 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 ) ) ) ) ) )
75 54 74 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 ) ) ) ) )
76 53 75 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 ) ) ) ) ) )
77 46 76 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 ) ) ) ) ) )
78 45 77 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 ) ) ) ) )
79 44 78 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 ) ) ) ) ) )
80 33 79 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 ) ) ) ) ) )
81 32 80 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 ) ) ) ) )
82 31 81 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 ) ) ) ) ) )