This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 nn0ex 
 |-  NN0 e. _V
72 71 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> NN0 e. _V )
73 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
74 73 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
75 74 sselda 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c e. ( NN0 ^m I ) )
76 67 72 75 elmaprd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c : I --> NN0 )
77 simpr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
78 22 77 elrabrd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> c finSupp 0 )
79 38 40 60 mulg0 
 |-  ( x e. B -> ( 0 ( .g ` ( mulGrp ` R ) ) x ) = ( 1r ` R ) )
80 79 adantl 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ x e. B ) -> ( 0 ( .g ` ( mulGrp ` R ) ) x ) = ( 1r ` R ) )
81 64 66 67 68 70 76 78 80 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 ) )
82 32 81 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 ) )
83 7 41 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
84 83 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. CMnd )
85 84 cmnmndd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. Mnd )
86 85 adantr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) -> ( mulGrp ` R ) e. Mnd )
87 76 ffvelcdmda 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ i e. I ) -> ( c ` i ) e. NN0 )
88 38 60 86 87 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 )
89 32 88 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 )
90 difss 
 |-  ( I \ { Y } ) C_ I
91 3 90 eqsstri 
 |-  J C_ I
92 91 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> J C_ I )
93 38 40 42 18 63 82 89 92 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 ) ) ) ) )
94 simpr 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. J ) -> i e. J )
95 94 fvresd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. J ) -> ( ( c |` J ) ` i ) = ( c ` i ) )
96 94 fvresd 
 |-  ( ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) /\ i e. J ) -> ( ( A |` J ) ` i ) = ( A ` i ) )
97 95 96 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 ) ) )
98 97 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 ) ) ) )
99 98 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 ) ) ) ) )
100 93 99 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 ) ) ) ) )
101 36 100 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 ) ) ) ) ) )
102 101 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 ) ) ) ) ) ) )
103 102 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 ) ) ) ) ) ) ) )
104 7 crngringd 
 |-  ( ph -> R e. Ring )
105 104 ringcmnd 
 |-  ( ph -> R e. CMnd )
106 ovex 
 |-  ( NN0 ^m I ) e. _V
107 106 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
108 107 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
109 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 ) )
110 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 )
111 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 )
112 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 )
113 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 )
114 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 } )
115 114 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 } )
116 16 17 110 111 112 3 4 113 115 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 ) ) )
117 115 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 } )
118 73 117 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 ) )
119 22 117 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 )
120 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 )
121 119 120 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 ) )
122 28 118 121 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 ) } )
123 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 ) } ) )
124 123 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 ) } )
125 122 124 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 )
126 125 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 ) )
127 109 116 126 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 ) )
128 127 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 ) ) ) ) ) )
129 eqid 
 |-  ( .r ` R ) = ( .r ` R )
130 104 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 )
131 88 fmpttd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( i e. I |-> ( ( c ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) : I --> B )
132 38 40 84 67 131 81 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 )
133 115 132 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 )
134 5 129 17 130 133 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 ) )
135 128 134 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 ) )
136 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
137 eqid 
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
138 16 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
139 16 17 8 104 5 3 4 9 10 137 extvfvcl 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` F ) e. ( Base ` ( I mPoly R ) ) )
140 13 139 eqeltrid 
 |-  ( ph -> ( ( E ` Y ) ` F ) e. ( Base ` ( I mPoly R ) ) )
141 136 5 137 138 140 mplelf 
 |-  ( ph -> ( ( E ` Y ) ` F ) : { h e. ( NN0 ^m I ) | h finSupp 0 } --> B )
142 136 137 17 140 mplelsfi 
 |-  ( ph -> ( ( E ` Y ) ` F ) finSupp ( 0g ` R ) )
143 5 104 108 132 141 142 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 ) )
144 104 adantr 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> R e. Ring )
145 141 ffvelcdmda 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( ( E ` Y ) ` F ) ` c ) e. B )
146 5 129 144 145 132 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 )
147 simpl 
 |-  ( ( h finSupp 0 /\ ( h ` Y ) = 0 ) -> h finSupp 0 )
148 147 a1i 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> ( ( h finSupp 0 /\ ( h ` Y ) = 0 ) -> h finSupp 0 ) )
149 148 ss2rabdv 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } C_ { h e. ( NN0 ^m I ) | h finSupp 0 } )
150 5 17 105 108 135 143 146 149 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 ) ) ) ) ) ) ) )
151 nfcv 
 |-  F/_ b ( ( F ` ( c |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. J |-> ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) ) ) )
152 fveq2 
 |-  ( b = ( c |` J ) -> ( F ` b ) = ( F ` ( c |` J ) ) )
153 fveq1 
 |-  ( b = ( c |` J ) -> ( b ` i ) = ( ( c |` J ) ` i ) )
154 153 oveq1d 
 |-  ( b = ( c |` J ) -> ( ( b ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) = ( ( ( c |` J ) ` i ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` i ) ) )
155 154 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 ) ) ) )
156 155 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 ) ) ) ) )
157 152 156 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 ) ) ) ) ) )
158 ovex 
 |-  ( NN0 ^m J ) e. _V
159 158 rabex 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } e. _V
160 159 a1i 
 |-  ( ph -> { h e. ( NN0 ^m J ) | h finSupp 0 } e. _V )
161 eqid 
 |-  ( J mPoly R ) = ( J mPoly R )
162 eqid 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | h finSupp 0 }
163 162 psrbasfsupp 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | ( `' h " NN ) e. Fin }
164 161 5 4 163 10 mplelf 
 |-  ( ph -> F : { h e. ( NN0 ^m J ) | h finSupp 0 } --> B )
165 164 feqmptd 
 |-  ( ph -> F = ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( F ` b ) ) )
166 161 4 17 10 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` R ) )
167 165 166 eqbrtrrd 
 |-  ( ph -> ( b e. { h e. ( NN0 ^m J ) | h finSupp 0 } |-> ( F ` b ) ) finSupp ( 0g ` R ) )
168 104 adantr 
 |-  ( ( ph /\ x e. B ) -> R e. Ring )
169 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
170 5 129 17 168 169 ringlzd 
 |-  ( ( ph /\ x e. B ) -> ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) )
171 164 ffvelcdmda 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( F ` b ) e. B )
172 83 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. CMnd )
173 91 a1i 
 |-  ( ph -> J C_ I )
174 8 173 ssexd 
 |-  ( ph -> J e. _V )
175 174 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> J e. _V )
176 172 cmnmndd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( mulGrp ` R ) e. Mnd )
177 176 adantr 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ i e. J ) -> ( mulGrp ` R ) e. Mnd )
178 71 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> NN0 e. _V )
179 ssrab2 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } C_ ( NN0 ^m J )
180 179 a1i 
 |-  ( ph -> { h e. ( NN0 ^m J ) | h finSupp 0 } C_ ( NN0 ^m J ) )
181 180 sselda 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b e. ( NN0 ^m J ) )
182 175 178 181 elmaprd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b : J --> NN0 )
183 182 ffvelcdmda 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ i e. J ) -> ( b ` i ) e. NN0 )
184 11 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> A : I --> B )
185 91 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> J C_ I )
186 184 185 fssresd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( A |` J ) : J --> B )
187 186 ffvelcdmda 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ i e. J ) -> ( ( A |` J ) ` i ) e. B )
188 38 60 177 183 187 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 )
189 188 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 )
190 182 feqmptd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b = ( i e. J |-> ( b ` i ) ) )
191 breq1 
 |-  ( h = b -> ( h finSupp 0 <-> b finSupp 0 ) )
192 simpr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
193 191 192 elrabrd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> b finSupp 0 )
194 190 193 eqbrtrrd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( i e. J |-> ( b ` i ) ) finSupp 0 )
195 79 adantl 
 |-  ( ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) /\ x e. B ) -> ( 0 ( .g ` ( mulGrp ` R ) ) x ) = ( 1r ` R ) )
196 fvexd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( 1r ` R ) e. _V )
197 194 195 183 187 196 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 ) )
198 38 40 172 175 189 197 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 )
199 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
200 167 170 171 198 199 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 ) )
201 ssidd 
 |-  ( ph -> B C_ B )
202 104 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> R e. Ring )
203 5 129 202 171 198 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 )
204 breq1 
 |-  ( h = ( c |` J ) -> ( h finSupp 0 <-> ( c |` J ) finSupp 0 ) )
205 25 92 elmapssresd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( c |` J ) e. ( NN0 ^m J ) )
206 65 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> 0 e. NN0 )
207 31 206 fsuppres 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> ( c |` J ) finSupp 0 )
208 204 205 207 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 } )
209 breq1 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( h finSupp 0 <-> ( b u. { <. Y , 0 >. } ) finSupp 0 ) )
210 fveq1 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( h ` Y ) = ( ( b u. { <. Y , 0 >. } ) ` Y ) )
211 210 eqeq1d 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( ( h ` Y ) = 0 <-> ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 ) )
212 209 211 anbi12d 
 |-  ( h = ( b u. { <. Y , 0 >. } ) -> ( ( h finSupp 0 /\ ( h ` Y ) = 0 ) <-> ( ( b u. { <. Y , 0 >. } ) finSupp 0 /\ ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 ) ) )
213 8 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> I e. V )
214 3 uneq1i 
 |-  ( J u. { Y } ) = ( ( I \ { Y } ) u. { Y } )
215 undifr 
 |-  ( { Y } C_ I <-> ( ( I \ { Y } ) u. { Y } ) = I )
216 45 215 sylib 
 |-  ( ph -> ( ( I \ { Y } ) u. { Y } ) = I )
217 214 216 eqtrid 
 |-  ( ph -> ( J u. { Y } ) = I )
218 217 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( J u. { Y } ) = I )
219 65 a1i 
 |-  ( ph -> 0 e. NN0 )
220 9 219 fsnd 
 |-  ( ph -> { <. Y , 0 >. } : { Y } --> NN0 )
221 220 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> { <. Y , 0 >. } : { Y } --> NN0 )
222 3 ineq1i 
 |-  ( J i^i { Y } ) = ( ( I \ { Y } ) i^i { Y } )
223 disjdifr 
 |-  ( ( I \ { Y } ) i^i { Y } ) = (/)
224 222 223 eqtri 
 |-  ( J i^i { Y } ) = (/)
225 224 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( J i^i { Y } ) = (/) )
226 182 221 225 fun2d 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) : ( J u. { Y } ) --> NN0 )
227 218 226 feq2dd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) : I --> NN0 )
228 178 213 227 elmapdd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) e. ( NN0 ^m I ) )
229 9 65 jctir 
 |-  ( ph -> ( Y e. I /\ 0 e. NN0 ) )
230 229 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( Y e. I /\ 0 e. NN0 ) )
231 182 ffund 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> Fun b )
232 neldifsnd 
 |-  ( ph -> -. Y e. ( I \ { Y } ) )
233 3 eleq2i 
 |-  ( Y e. J <-> Y e. ( I \ { Y } ) )
234 232 233 sylnibr 
 |-  ( ph -> -. Y e. J )
235 234 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> -. Y e. J )
236 182 fdmd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> dom b = J )
237 235 236 neleqtrrd 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> -. Y e. dom b )
238 df-nel 
 |-  ( Y e/ dom b <-> -. Y e. dom b )
239 237 238 sylibr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> Y e/ dom b )
240 231 239 jca 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( Fun b /\ Y e/ dom b ) )
241 funsnfsupp 
 |-  ( ( ( Y e. I /\ 0 e. NN0 ) /\ ( Fun b /\ Y e/ dom b ) ) -> ( ( b u. { <. Y , 0 >. } ) finSupp 0 <-> b finSupp 0 ) )
242 241 biimpar 
 |-  ( ( ( ( Y e. I /\ 0 e. NN0 ) /\ ( Fun b /\ Y e/ dom b ) ) /\ b finSupp 0 ) -> ( b u. { <. Y , 0 >. } ) finSupp 0 )
243 230 240 193 242 syl21anc 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( b u. { <. Y , 0 >. } ) finSupp 0 )
244 9 adantr 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> Y e. I )
245 65 a1i 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> 0 e. NN0 )
246 fsnunfv 
 |-  ( ( Y e. I /\ 0 e. NN0 /\ -. Y e. dom b ) -> ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 )
247 244 245 237 246 syl3anc 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 )
248 243 247 jca 
 |-  ( ( ph /\ b e. { h e. ( NN0 ^m J ) | h finSupp 0 } ) -> ( ( b u. { <. Y , 0 >. } ) finSupp 0 /\ ( ( b u. { <. Y , 0 >. } ) ` Y ) = 0 ) )
249 212 228 248 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 ) } )
250 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 ) )
251 250 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 >. } ) )
252 3 reseq2i 
 |-  ( c |` J ) = ( c |` ( I \ { Y } ) )
253 252 uneq1i 
 |-  ( ( c |` J ) u. { <. Y , 0 >. } ) = ( ( c |` ( I \ { Y } ) ) u. { <. Y , 0 >. } )
254 253 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 >. } ) )
255 71 a1i 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> NN0 e. _V )
256 18 255 25 elmaprd 
 |-  ( ( ph /\ c e. { h e. ( NN0 ^m I ) | ( h finSupp 0 /\ ( h ` Y ) = 0 ) } ) -> c : I --> NN0 )
257 256 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 )
258 257 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 )
259 244 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 )
260 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 ) )
261 260 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 )
262 fresunsn 
 |-  ( ( c Fn I /\ Y e. I /\ ( c ` Y ) = 0 ) -> ( ( c |` ( I \ { Y } ) ) u. { <. Y , 0 >. } ) = c )
263 258 259 261 262 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 )
264 251 254 263 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 >. } ) )
265 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 >. } ) )
266 265 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 ) )
267 182 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 )
268 267 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 )
269 235 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 )
270 fsnunres 
 |-  ( ( b Fn J /\ -. Y e. J ) -> ( ( b u. { <. Y , 0 >. } ) |` J ) = b )
271 268 269 270 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 )
272 266 271 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 ) )
273 264 272 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 >. } ) ) )
274 249 273 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 ) )
275 151 5 17 157 105 160 200 201 203 208 274 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 ) ) ) ) ) ) ) )
276 103 150 275 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 ) ) ) ) ) ) ) )
277 1 5 evlval 
 |-  Q = ( ( I evalSub R ) ` B )
278 eqid 
 |-  ( I mPoly ( R |`s B ) ) = ( I mPoly ( R |`s B ) )
279 eqid 
 |-  ( Base ` ( I mPoly ( R |`s B ) ) ) = ( Base ` ( I mPoly ( R |`s B ) ) )
280 eqid 
 |-  ( R |`s B ) = ( R |`s B )
281 5 subrgid 
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
282 104 281 syl 
 |-  ( ph -> B e. ( SubRing ` R ) )
283 5 ressid 
 |-  ( R e. CRing -> ( R |`s B ) = R )
284 7 283 syl 
 |-  ( ph -> ( R |`s B ) = R )
285 284 oveq2d 
 |-  ( ph -> ( I mPoly ( R |`s B ) ) = ( I mPoly R ) )
286 285 fveq2d 
 |-  ( ph -> ( Base ` ( I mPoly ( R |`s B ) ) ) = ( Base ` ( I mPoly R ) ) )
287 140 286 eleqtrrd 
 |-  ( ph -> ( ( E ` Y ) ` F ) e. ( Base ` ( I mPoly ( R |`s B ) ) ) )
288 5 fvexi 
 |-  B e. _V
289 288 a1i 
 |-  ( ph -> B e. _V )
290 289 8 11 elmapdd 
 |-  ( ph -> A e. ( B ^m I ) )
291 277 278 279 280 138 5 37 60 129 8 7 282 287 290 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 ) ) ) ) ) ) ) )
292 2 5 evlval 
 |-  O = ( ( J evalSub R ) ` B )
293 eqid 
 |-  ( J mPoly ( R |`s B ) ) = ( J mPoly ( R |`s B ) )
294 eqid 
 |-  ( Base ` ( J mPoly ( R |`s B ) ) ) = ( Base ` ( J mPoly ( R |`s B ) ) )
295 10 4 eleqtrdi 
 |-  ( ph -> F e. ( Base ` ( J mPoly R ) ) )
296 284 oveq2d 
 |-  ( ph -> ( J mPoly ( R |`s B ) ) = ( J mPoly R ) )
297 296 fveq2d 
 |-  ( ph -> ( Base ` ( J mPoly ( R |`s B ) ) ) = ( Base ` ( J mPoly R ) ) )
298 295 297 eleqtrrd 
 |-  ( ph -> F e. ( Base ` ( J mPoly ( R |`s B ) ) ) )
299 290 173 elmapssresd 
 |-  ( ph -> ( A |` J ) e. ( B ^m J ) )
300 292 293 294 280 163 5 37 60 129 174 7 282 298 299 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 ) ) ) ) ) ) ) )
301 276 291 300 3eqtr4d 
 |-  ( ph -> ( ( Q ` ( ( E ` Y ) ` F ) ) ` A ) = ( ( O ` F ) ` ( A |` J ) ) )