Metamath Proof Explorer

Theorem evlextv

Description: Evaluating a variable-extended polynomial is the same as evaluating the polynomial in the original set of variables (in both cases, the additionial variable is ignored). (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses evlextv.q 
|- Q = ( I eval R )
evlextv.o 
|- O = ( J eval R )
evlextv.j 
|- J = ( I \ { Y } )
evlextv.m 
|- M = ( Base ` ( J mPoly R ) )
evlextv.b 
|- B = ( Base ` R )
evlextv.e 
|- E = ( I extendVars R )
evlextv.r 
|- ( ph -> R e. CRing )
evlextv.i 
|- ( ph -> I e. V )
evlextv.y 
|- ( ph -> Y e. I )
evlextv.f 
|- ( ph -> F e. M )
evlextv.a 
|- ( ph -> A : I --> B )
Assertion evlextv 
|- ( ph -> ( ( Q ` ( ( E ` Y ) ` F ) ) ` A ) = ( ( O ` F ) ` ( A |` J ) ) )

Proof

Step Hyp Ref Expression
1 evlextv.q 
 |-  Q = ( I eval R )
2 evlextv.o 
 |-  O = ( J eval R )
3 evlextv.j 
 |-  J = ( I \ { Y } )
4 evlextv.m 
 |-  M = ( Base ` ( J mPoly R ) )
5 evlextv.b 
 |-  B = ( Base ` R )
6 evlextv.e 
 |-  E = ( I extendVars R )
7 evlextv.r 
 |-  ( ph -> R e. CRing )
8 evlextv.i 
 |-  ( ph -> I e. V )
9 evlextv.y 
 |-  ( ph -> Y e. I )
10 evlextv.f 
 |-  ( ph -> F e. M )
11 evlextv.a 
 |-  ( ph -> A : I --> B )
12 6 fveq1i 
 |-  ( E ` Y ) = ( ( I extendVars R ) ` Y )
13 12 fveq1i 
 |-  ( ( E ` Y ) ` F ) = ( ( ( I extendVars R ) ` Y ) ` F )
14 13 fveq1i 
 |-  ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c )
15 14 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) )
16 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 8 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> I e. V )
19 7 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> R e. CRing )
20 9 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> Y e. I )
21 10 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> F e. M )
22 breq1 
 |-  ( h = c -> ( h finSupp 0 <-> c finSupp 0 ) )
23 ssrab2 
 |-  { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } C_ ( NN0 ^m I )
24 23 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } C_ ( NN0 ^m I ) )
25 24 sselda 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> c e. ( NN0 ^m I ) )
26 fveq1 
 |-  ( h = c -> ( h ` Y ) = ( c ` Y ) )
27 26 eqeq1d 
 |-  ( h = c -> ( ( h ` Y ) = 0 <-> ( c ` Y ) = 0 ) )
28 22 27 anbi12d 
 |-  ( h = c -> ( ( h finSupp 0 /\ ( h ` Y ) = 0 ) <-> ( c finSupp 0 /\ ( c ` Y ) = 0 ) ) )
29 simpr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } )
30 28 29 elrabrd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( c finSupp 0 /\ ( c ` Y ) = 0 ) )
31 30 simpld 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> c finSupp 0 )
32 22 25 31 elrabd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> c e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
33 16 17 18 19 20 3 4 21 32 extvfvv 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) = if ( ( c ` Y ) = 0 , ( F ` ( c |` J ) ) , ( 0g ` R ) ) )
34 30 simprd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( c ` Y ) = 0 )
35 34 iftrued 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> if ( ( c ` Y ) = 0 , ( F ` ( c |` J ) ) , ( 0g ` R ) ) = ( F ` ( c |` J ) ) )
36 15 33 35 3eqtrd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( F ` ( c |` J ) ) )
37 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
38 37 5 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
39 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
40 37 39 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
41 37 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
42 19 41 syl 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( mulGrp ` R ) e. CMnd )
43 simpr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> i e. ( I \ J ) )
44 3 difeq2i 
 |-  ( I \ J ) = ( I \ ( I \ { Y } ) )
45 9 snssd 
 |-  ( ph -> { Y } C_ I )
46 dfss4 
 |-  ( { Y } C_ I <-> ( I \ ( I \ { Y } ) ) = { Y } )
47 45 46 sylib 
 |-  ( ph -> ( I \ ( I \ { Y } ) ) = { Y } )
48 44 47 eqtrid 
 |-  ( ph -> ( I \ J ) = { Y } )
49 48 ad2antrr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( I \ J ) = { Y } )
50 43 49 eleqtrd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> i e. { Y } )
51 50 elsnd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> i = Y )
52 51 fveq2d 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( c ` i ) = ( c ` Y ) )
53 34 adantr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( c ` Y ) = 0 )
54 52 53 eqtrd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( c ` i ) = 0 )
55 54 oveq1d 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) = ( 0 ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) )
56 11 ad2antrr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> A : I --> B )
57 difssd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( I \ J ) C_ I )
58 57 sselda 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> i e. I )
59 56 58 ffvelcdmd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( A ` i ) e. B )
60 eqid 
 |-  ( .g ` ( mulGrp ` R ) ) = ( .g ` ( mulGrp ` R ) )
61 38 40 60 mulg0 
 |-  ( ( A ` i ) e. B -> ( 0 ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) = ( 1r ` R ) )
62 59 61 syl 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( 0 ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) = ( 1r ` R ) )
63 55 62 eqtrd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. ( I \ J ) ) -> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) = ( 1r ` R ) )
64 fvexd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( 1r ` R ) e. _V )
65 0nn0 
 |-  0 e. NN0
66 65 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> 0 e. NN0 )
67 8 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. V )
68 ssidd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I C_ I )
69 11 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> A : I --> B )
70 69 ffvelcdmda 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) -> ( A ` i ) e. B )
71 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
72 71 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
73 72 sselda 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c e. ( NN0 ^m I ) )
74 73 elmaprd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c : I --> NN0 )
75 simpr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
76 22 75 elrabrd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c finSupp 0 )
77 38 40 60 mulg0 
 |-  ( x e. B -> ( 0 ( .g ` ( mulGrp ` R ) ) x ) = ( 1r ` R ) )
78 77 adantl 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ x e. B ) -> ( 0 ( .g ` ( mulGrp ` R ) ) x ) = ( 1r ` R ) )
79 64 66 67 68 70 74 76 78 fisuppov1 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) finSupp ( 1r ` R ) )
80 32 79 syldan 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) finSupp ( 1r ` R ) )
81 7 41 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
82 81 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. CMnd )
83 82 cmnmndd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. Mnd )
84 83 adantr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) -> ( mulGrp ` R ) e. Mnd )
85 74 ffvelcdmda 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) -> ( c ` i ) e. NN0 )
86 38 60 84 85 70 mulgnn0cld 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) -> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) e. B )
87 32 86 syldanl 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. I ) -> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) e. B )
88 difss 
 |-  ( I \ { Y } ) C_ I
89 3 88 eqsstri 
 |-  J C_ I
90 89 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> J C_ I )
91 38 40 42 18 63 80 87 90 gsummptfsres 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) = ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) )
92 simpr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. J ) -> i e. J )
93 92 fvresd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. J ) -> ( ( c |` J ) ` i ) = ( c ` i ) )
94 92 fvresd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. J ) -> ( ( A |` J ) ` i ) = ( A ` i ) )
95 93 94 oveq12d 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. J ) -> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) = ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) )
96 95 mpteq2dva 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) = ( i e. J |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) )
97 96 oveq2d 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) = ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) )
98 91 97 eqtr4d 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) = ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) )
99 36 98 oveq12d 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) = ( ( F ` ( c |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) )
100 99 mpteq2dva 
 |-  ( ph -> ( c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } |-> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) = ( c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } |-> ( ( F ` ( c |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) ) )
101 100 oveq2d 
 |-  ( ph -> ( R gsum ( c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } |-> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) = ( R gsum ( c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } |-> ( ( F ` ( c |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) ) ) )
102 7 crngringd 
 |-  ( ph -> R e. Ring )
103 102 ringcmnd 
 |-  ( ph -> R e. CMnd )
104 ovex 
 |-  ( NN0 ^m I ) e. _V
105 104 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
106 105 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
107 14 a1i 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) )
108 8 adantr 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> I e. V )
109 7 adantr 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> R e. CRing )
110 9 adantr 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> Y e. I )
111 10 adantr 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> F e. M )
112 difssd 
 |-  ( ph -> ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) C_ { h e. ( NN0 ^m I ) | h finSupp 0 } )
113 112 sselda 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> c e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
114 16 17 108 109 110 3 4 111 113 extvfvv 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( ( I extendVars R ) ` Y ) ` F ) ` c ) = if ( ( c ` Y ) = 0 , ( F ` ( c |` J ) ) , ( 0g ` R ) ) )
115 113 adantr 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> c e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
116 71 115 sselid 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> c e. ( NN0 ^m I ) )
117 22 115 elrabrd 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> c finSupp 0 )
118 simpr 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> ( c ` Y ) = 0 )
119 117 118 jca 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> ( c finSupp 0 /\ ( c ` Y ) = 0 ) )
120 28 116 119 elrabd 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } )
121 simplr 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) )
122 121 eldifbd 
 |-  ( ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) /\ ( c ` Y ) = 0 ) -> -. c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } )
123 120 122 pm2.65da 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> -. ( c ` Y ) = 0 )
124 123 iffalsed 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> if ( ( c ` Y ) = 0 , ( F ` ( c |` J ) ) , ( 0g ` R ) ) = ( 0g ` R ) )
125 107 114 124 3eqtrd 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( E ` Y ) ` F ) ` c ) = ( 0g ` R ) )
126 125 oveq1d 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) = ( ( 0g ` R ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) )
127 eqid 
 |-  ( .r ` R ) = ( .r ` R )
128 102 adantr 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> R e. Ring )
129 86 fmpttd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) : I --> B )
130 38 40 82 67 129 79 gsumcl 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) e. B )
131 113 130 syldan 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) e. B )
132 5 127 17 128 131 ringlzd 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( 0g ` R ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) = ( 0g ` R ) )
133 126 132 eqtrd 
 |-  ( ( ph /\ c e. ( { h e. ( NN0 ^m I ) | h finSupp 0 } \ { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) ) -> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) = ( 0g ` R ) )
134 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
135 eqid 
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
136 16 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
137 16 17 8 102 5 3 4 9 10 135 extvfvcl 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` F ) e. ( Base ` ( I mPoly R ) ) )
138 13 137 eqeltrid 
 |-  ( ph -> ( ( E ` Y ) ` F ) e. ( Base ` ( I mPoly R ) ) )
139 134 5 135 136 138 mplelf 
 |-  ( ph -> ( ( E ` Y ) ` F ) : { h e. ( NN0 ^m I ) | h finSupp 0 } --> B )
140 134 135 17 138 mplelsfi 
 |-  ( ph -> ( ( E ` Y ) ` F ) finSupp ( 0g ` R ) )
141 5 102 106 130 139 140 rmfsupp2 
 |-  ( ph -> ( c e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) finSupp ( 0g ` R ) )
142 102 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> R e. Ring )
143 139 ffvelcdmda 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( ( E ` Y ) ` F ) ` c ) e. B )
144 5 127 142 143 130 ringcld 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) e. B )
145 simpl 
 |-  ( ( h finSupp 0 /\ ( h ` Y ) = 0 ) -> h finSupp 0 )
146 145 a1i 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> ( ( h finSupp 0 /\ ( h ` Y ) = 0 ) -> h finSupp 0 ) )
147 146 ss2rabdv 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } C_ { h e. ( NN0 ^m I ) | h finSupp 0 } )
148 5 17 103 106 133 141 144 147 gsummptfsres 
 |-  ( ph -> ( R gsum ( c e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) = ( R gsum ( c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } |-> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) )
149 nfcv 
 |-  F/_ b ( ( F ` ( c |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) )
150 fveq2 
 |-  ( b = ( c |` J ) -> ( F ` b ) = ( F ` ( c |` J ) ) )
151 fveq1 
 |-  ( b = ( c |` J ) -> ( b ` i ) = ( ( c |` J ) ` i ) )
152 151 oveq1d 
 |-  ( b = ( c |` J ) -> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) = ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) )
153 152 mpteq2dv 
 |-  ( b = ( c |` J ) -> ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) = ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) )
154 153 oveq2d 
 |-  ( b = ( c |` J ) -> ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) = ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) )
155 150 154 oveq12d 
 |-  ( b = ( c |` J ) -> ( ( F ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) = ( ( F ` ( c |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) )
156 ovex 
 |-  ( NN0 ^m J ) e. _V
157 156 rabex 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } e. _V
158 157 a1i 
 |-  ( ph -> { h e. ( NN0 ^m J ) | h finSupp 0 } e. _V )
159 eqid 
 |-  ( J mPoly R ) = ( J mPoly R )
160 eqid 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | h finSupp 0 }
161 160 psrbasfsupp 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | ( `' h " NN ) e. Fin }
162 159 5 4 161 10 mplelf 
 |-  ( ph -> F : { h e. ( NN0 ^m J ) | h finSupp 0 } --> B )
163 162 feqmptd 
 |-  ( ph -> F = ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( F ` b ) ) )
164 159 4 17 10 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` R ) )
165 163 164 eqbrtrrd 
 |-  ( ph -> ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( F ` b ) ) finSupp ( 0g ` R ) )
166 102 adantr 
 |-  ( ( ph /\ x e. B ) -> R e. Ring )
167 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
168 5 127 17 166 167 ringlzd 
 |-  ( ( ph /\ x e. B ) -> ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) )
169 162 ffvelcdmda 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( F ` b ) e. B )
170 81 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. CMnd )
171 89 a1i 
 |-  ( ph -> J C_ I )
172 8 171 ssexd 
 |-  ( ph -> J e. _V )
173 172 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> J e. _V )
174 170 cmnmndd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. Mnd )
175 174 adantr 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ i e. J ) -> ( mulGrp ` R ) e. Mnd )
176 ssrab2 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } C_ ( NN0 ^m J )
177 176 a1i 
 |-  ( ph -> { h e. ( NN0 ^m J ) | h finSupp 0 } C_ ( NN0 ^m J ) )
178 177 sselda 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b e. ( NN0 ^m J ) )
179 178 elmaprd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b : J --> NN0 )
180 179 ffvelcdmda 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ i e. J ) -> ( b ` i ) e. NN0 )
181 11 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> A : I --> B )
182 89 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> J C_ I )
183 181 182 fssresd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( A |` J ) : J --> B )
184 183 ffvelcdmda 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ i e. J ) -> ( ( A |` J ) ` i ) e. B )
185 38 60 175 180 184 mulgnn0cld 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ i e. J ) -> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) e. B )
186 185 fmpttd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) : J --> B )
187 179 feqmptd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b = ( i e. J |-> ( b ` i ) ) )
188 breq1 
 |-  ( h = b -> ( h finSupp 0 <-> b finSupp 0 ) )
189 simpr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
190 188 189 elrabrd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b finSupp 0 )
191 187 190 eqbrtrrd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( i e. J |-> ( b ` i ) ) finSupp 0 )
192 77 adantl 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ x e. B ) -> ( 0 ( .g ` ( mulGrp ` R ) ) x ) = ( 1r ` R ) )
193 fvexd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( 1r ` R ) e. _V )
194 191 192 180 184 193 fsuppssov1 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) finSupp ( 1r ` R ) )
195 38 40 170 173 186 194 gsumcl 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) e. B )
196 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
197 165 168 169 195 196 fsuppssov1 
 |-  ( ph -> ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( ( F ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) ) finSupp ( 0g ` R ) )
198 ssidd 
 |-  ( ph -> B C_ B )
199 102 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> R e. Ring )
200 5 127 199 169 195 ringcld 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( ( F ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) e. B )
201 breq1 
 |-  ( h = ( c |` J ) -> ( h finSupp 0 <-> ( c |` J ) finSupp 0 ) )
202 25 90 elmapssresd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( c |` J ) e. ( NN0 ^m J ) )
203 65 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> 0 e. NN0 )
204 31 203 fsuppres 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( c |` J ) finSupp 0 )
205 201 202 204 elrabd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( c |` J ) e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
206 breq1 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( h finSupp 0 <-> ( b u. { <. Y , 0 >. } ) finSupp 0 ) )
207 fveq1 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( h ` Y ) = ( ( b u. { <. Y , 0 >. } ) ` Y ) )
208 207 eqeq1d 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( ( h ` Y ) = 0 <-> ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 ) )
209 206 208 anbi12d 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( ( h finSupp 0 /\ ( h ` Y ) = 0 ) <-> ( ( b u. { <. Y , 0 >. } ) finSupp 0 /\ ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 ) ) )
210 nn0ex 
 |-  NN0 e. _V
211 210 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> NN0 e. _V )
212 8 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> I e. V )
213 3 uneq1i 
 |-  ( J u. { Y } ) = ( ( I \ { Y } ) u. { Y } )
214 undifr 
 |-  ( { Y } C_ I <-> ( ( I \ { Y } ) u. { Y } ) = I )
215 45 214 sylib 
 |-  ( ph -> ( ( I \ { Y } ) u. { Y } ) = I )
216 213 215 eqtrid 
 |-  ( ph -> ( J u. { Y } ) = I )
217 216 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( J u. { Y } ) = I )
218 65 a1i 
 |-  ( ph -> 0 e. NN0 )
219 9 218 fsnd 
 |-  ( ph -> { <. Y , 0 >. } : { Y } --> NN0 )
220 219 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> { <. Y , 0 >. } : { Y } --> NN0 )
221 3 ineq1i 
 |-  ( J i^i { Y } ) = ( ( I \ { Y } ) i^i { Y } )
222 disjdifr 
 |-  ( ( I \ { Y } ) i^i { Y } ) = (/)
223 221 222 eqtri 
 |-  ( J i^i { Y } ) = (/)
224 223 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( J i^i { Y } ) = (/) )
225 179 220 224 fun2d 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) : ( J u. { Y } ) --> NN0 )
226 217 225 feq2dd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) : I --> NN0 )
227 211 212 226 elmapdd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) e. ( NN0 ^m I ) )
228 9 65 jctir 
 |-  ( ph -> ( Y e. I /\ 0 e. NN0 ) )
229 228 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( Y e. I /\ 0 e. NN0 ) )
230 179 ffund 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> Fun b )
231 neldifsnd 
 |-  ( ph -> -. Y e. ( I \ { Y } ) )
232 3 eleq2i 
 |-  ( Y e. J <-> Y e. ( I \ { Y } ) )
233 231 232 sylnibr 
 |-  ( ph -> -. Y e. J )
234 233 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> -. Y e. J )
235 179 fdmd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> dom b = J )
236 234 235 neleqtrrd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> -. Y e. dom b )
237 df-nel 
 |-  ( Y e/ dom b <-> -. Y e. dom b )
238 236 237 sylibr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> Y e/ dom b )
239 230 238 jca 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( Fun b /\ Y e/ dom b ) )
240 funsnfsupp 
 |-  ( ( ( Y e. I /\ 0 e. NN0 ) /\ ( Fun b /\ Y e/ dom b ) ) -> ( ( b u. { <. Y , 0 >. } ) finSupp 0 <-> b finSupp 0 ) )
241 240 biimpar 
 |-  ( ( ( ( Y e. I /\ 0 e. NN0 ) /\ ( Fun b /\ Y e/ dom b ) ) /\ b finSupp 0 ) -> ( b u. { <. Y , 0 >. } ) finSupp 0 )
242 229 239 190 241 syl21anc 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) finSupp 0 )
243 9 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> Y e. I )
244 65 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> 0 e. NN0 )
245 fsnunfv 
 |-  ( ( Y e. I /\ 0 e. NN0 /\ -. Y e. dom b ) -> ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 )
246 243 244 236 245 syl3anc 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 )
247 242 246 jca 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( ( b u. { <. Y , 0 >. } ) finSupp 0 /\ ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 ) )
248 209 227 247 elrabd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } )
249 simpr 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> b = ( c |` J ) )
250 249 uneq1d 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> ( b u. { <. Y , 0 >. } ) = ( ( c |` J ) u. { <. Y , 0 >. } ) )
251 3 reseq2i 
 |-  ( c |` J ) = ( c |` ( I \ { Y } ) )
252 251 uneq1i 
 |-  ( ( c |` J ) u. { <. Y , 0 >. } ) = ( ( c |` ( I \ { Y } ) ) u. { <. Y , 0 >. } )
253 252 a1i 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> ( ( c |` J ) u. { <. Y , 0 >. } ) = ( ( c |` ( I \ { Y } ) ) u. { <. Y , 0 >. } ) )
254 25 elmaprd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> c : I --> NN0 )
255 254 ad4ant13 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> c : I --> NN0 )
256 255 ffnd 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> c Fn I )
257 243 ad2antrr 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> Y e. I )
258 30 ad4ant13 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> ( c finSupp 0 /\ ( c ` Y ) = 0 ) )
259 258 simprd 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> ( c ` Y ) = 0 )
260 fresunsn 
 |-  ( ( c Fn I /\ Y e. I /\ ( c ` Y ) = 0 ) -> ( ( c |` ( I \ { Y } ) ) u. { <. Y , 0 >. } ) = c )
261 256 257 259 260 syl3anc 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> ( ( c |` ( I \ { Y } ) ) u. { <. Y , 0 >. } ) = c )
262 250 253 261 3eqtrrd 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ b = ( c |` J ) ) -> c = ( b u. { <. Y , 0 >. } ) )
263 simpr 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ c = ( b u. { <. Y , 0 >. } ) ) -> c = ( b u. { <. Y , 0 >. } ) )
264 263 reseq1d 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ c = ( b u. { <. Y , 0 >. } ) ) -> ( c |` J ) = ( ( b u. { <. Y , 0 >. } ) |` J ) )
265 179 ad2antrr 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ c = ( b u. { <. Y , 0 >. } ) ) -> b : J --> NN0 )
266 265 ffnd 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ c = ( b u. { <. Y , 0 >. } ) ) -> b Fn J )
267 234 ad2antrr 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ c = ( b u. { <. Y , 0 >. } ) ) -> -. Y e. J )
268 fsnunres 
 |-  ( ( b Fn J /\ -. Y e. J ) -> ( ( b u. { <. Y , 0 >. } ) |` J ) = b )
269 266 267 268 syl2anc 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ c = ( b u. { <. Y , 0 >. } ) ) -> ( ( b u. { <. Y , 0 >. } ) |` J ) = b )
270 264 269 eqtr2d 
 |-  ( ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ c = ( b u. { <. Y , 0 >. } ) ) -> b = ( c |` J ) )
271 262 270 impbida 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( b = ( c |` J ) <-> c = ( b u. { <. Y , 0 >. } ) ) )
272 248 271 reu6dv 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> E! c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } b = ( c |` J ) )
273 149 5 17 155 103 158 197 198 200 205 272 gsummptfsf1o 
 |-  ( ph -> ( R gsum ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( ( F ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) ) ) = ( R gsum ( c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } |-> ( ( F ` ( c |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) ) ) )
274 101 148 273 3eqtr4d 
 |-  ( ph -> ( R gsum ( c e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) = ( R gsum ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( ( F ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) ) ) )
275 1 5 evlval 
 |-  Q = ( ( I evalSub R ) ` B )
276 eqid 
 |-  ( I mPoly ( R |`s B ) ) = ( I mPoly ( R |`s B ) )
277 eqid 
 |-  ( Base ` ( I mPoly ( R |`s B ) ) ) = ( Base ` ( I mPoly ( R |`s B ) ) )
278 eqid 
 |-  ( R |`s B ) = ( R |`s B )
279 5 subrgid 
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
280 102 279 syl 
 |-  ( ph -> B e. ( SubRing ` R ) )
281 5 ressid 
 |-  ( R e. CRing -> ( R |`s B ) = R )
282 7 281 syl 
 |-  ( ph -> ( R |`s B ) = R )
283 282 oveq2d 
 |-  ( ph -> ( I mPoly ( R |`s B ) ) = ( I mPoly R ) )
284 283 fveq2d 
 |-  ( ph -> ( Base ` ( I mPoly ( R |`s B ) ) ) = ( Base ` ( I mPoly R ) ) )
285 138 284 eleqtrrd 
 |-  ( ph -> ( ( E ` Y ) ` F ) e. ( Base ` ( I mPoly ( R |`s B ) ) ) )
286 5 fvexi 
 |-  B e. _V
287 286 a1i 
 |-  ( ph -> B e. _V )
288 287 8 11 elmapdd 
 |-  ( ph -> A e. ( B ^m I ) )
289 275 276 277 278 136 5 37 60 127 8 7 280 285 288 evlsvvval 
 |-  ( ph -> ( ( Q ` ( ( E ` Y ) ` F ) ) ` A ) = ( R gsum ( c e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ( ( E ` Y ) ` F ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) )
290 2 5 evlval 
 |-  O = ( ( J evalSub R ) ` B )
291 eqid 
 |-  ( J mPoly ( R |`s B ) ) = ( J mPoly ( R |`s B ) )
292 eqid 
 |-  ( Base ` ( J mPoly ( R |`s B ) ) ) = ( Base ` ( J mPoly ( R |`s B ) ) )
293 10 4 eleqtrdi 
 |-  ( ph -> F e. ( Base ` ( J mPoly R ) ) )
294 282 oveq2d 
 |-  ( ph -> ( J mPoly ( R |`s B ) ) = ( J mPoly R ) )
295 294 fveq2d 
 |-  ( ph -> ( Base ` ( J mPoly ( R |`s B ) ) ) = ( Base ` ( J mPoly R ) ) )
296 293 295 eleqtrrd 
 |-  ( ph -> F e. ( Base ` ( J mPoly ( R |`s B ) ) ) )
297 288 171 elmapssresd 
 |-  ( ph -> ( A |` J ) e. ( B ^m J ) )
298 290 291 292 278 161 5 37 60 127 172 7 280 296 297 evlsvvval 
 |-  ( ph -> ( ( O ` F ) ` ( A |` J ) ) = ( R gsum ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( ( F ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) ) ) ) )
299 274 289 298 3eqtr4d 
 |-  ( ph -> ( ( Q ` ( ( E ` Y ) ` F ) ) ` A ) = ( ( O ` F ) ` ( A |` J ) ) )