Metamath Proof Explorer

Theorem extvfvcl

Description: Closure for the "variable extension" function evaluated for converting a given polynomial F by adding a variable with index A . (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses extvfvvcl.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
extvfvvcl.3 
|- .0. = ( 0g ` R )
extvfvvcl.i 
|- ( ph -> I e. V )
extvfvvcl.r 
|- ( ph -> R e. Ring )
extvfvvcl.b 
|- B = ( Base ` R )
extvfvvcl.j 
|- J = ( I \ { A } )
extvfvvcl.m 
|- M = ( Base ` ( J mPoly R ) )
extvfvvcl.1 
|- ( ph -> A e. I )
extvfvvcl.f 
|- ( ph -> F e. M )
extvfvcl.n 
|- N = ( Base ` ( I mPoly R ) )
Assertion extvfvcl 
|- ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N )

Proof

Step Hyp Ref Expression
1 extvfvvcl.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
2 extvfvvcl.3 
 |-  .0. = ( 0g ` R )
3 extvfvvcl.i 
 |-  ( ph -> I e. V )
4 extvfvvcl.r 
 |-  ( ph -> R e. Ring )
5 extvfvvcl.b 
 |-  B = ( Base ` R )
6 extvfvvcl.j 
 |-  J = ( I \ { A } )
7 extvfvvcl.m 
 |-  M = ( Base ` ( J mPoly R ) )
8 extvfvvcl.1 
 |-  ( ph -> A e. I )
9 extvfvvcl.f 
 |-  ( ph -> F e. M )
10 extvfvcl.n 
 |-  N = ( Base ` ( I mPoly R ) )
11 5 fvexi 
 |-  B e. _V
12 11 a1i 
 |-  ( ph -> B e. _V )
13 ovex 
 |-  ( NN0 ^m I ) e. _V
14 1 13 rabex2 
 |-  D e. _V
15 14 a1i 
 |-  ( ph -> D e. _V )
16 fvexd 
 |-  ( ( ph /\ x e. D ) -> ( F ` ( x |` J ) ) e. _V )
17 2 fvexi 
 |-  .0. e. _V
18 17 a1i 
 |-  ( ( ph /\ x e. D ) -> .0. e. _V )
19 16 18 ifcld 
 |-  ( ( ph /\ x e. D ) -> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) e. _V )
20 1 2 3 4 8 6 7 9 extvfv 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) = ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )
21 3 adantr 
 |-  ( ( ph /\ x e. D ) -> I e. V )
22 4 adantr 
 |-  ( ( ph /\ x e. D ) -> R e. Ring )
23 8 adantr 
 |-  ( ( ph /\ x e. D ) -> A e. I )
24 9 adantr 
 |-  ( ( ph /\ x e. D ) -> F e. M )
25 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
26 1 2 21 22 5 6 7 23 24 25 extvfvvcl 
 |-  ( ( ph /\ x e. D ) -> ( ( ( ( I extendVars R ) ` A ) ` F ) ` x ) e. B )
27 19 20 26 fmpt2d 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) : D --> B )
28 12 15 27 elmapdd 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( B ^m D ) )
29 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
30 1 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
31 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
32 29 5 30 31 3 psrbas 
 |-  ( ph -> ( Base ` ( I mPwSer R ) ) = ( B ^m D ) )
33 28 32 eleqtrrd 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) )
34 15 mptexd 
 |-  ( ph -> ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) e. _V )
35 17 a1i 
 |-  ( ph -> .0. e. _V )
36 19 fmpttd 
 |-  ( ph -> ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) : D --> _V )
37 36 ffund 
 |-  ( ph -> Fun ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) )
38 fveq1 
 |-  ( y = x -> ( y ` A ) = ( x ` A ) )
39 38 eqeq1d 
 |-  ( y = x -> ( ( y ` A ) = 0 <-> ( x ` A ) = 0 ) )
40 39 cbvrabv 
 |-  { y e. D | ( y ` A ) = 0 } = { x e. D | ( x ` A ) = 0 }
41 40 partfun2 
 |-  ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) u. ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) )
42 41 oveq1i 
 |-  ( ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) supp .0. ) = ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) u. ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) ) supp .0. )
43 40 15 rabexd 
 |-  ( ph -> { y e. D | ( y ` A ) = 0 } e. _V )
44 43 mptexd 
 |-  ( ph -> ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) e. _V )
45 15 difexd 
 |-  ( ph -> ( D \ { y e. D | ( y ` A ) = 0 } ) e. _V )
46 45 mptexd 
 |-  ( ph -> ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) e. _V )
47 44 46 35 suppun2 
 |-  ( ph -> ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) u. ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) ) supp .0. ) = ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) supp .0. ) u. ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) ) )
48 42 47 eqtrid 
 |-  ( ph -> ( ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) supp .0. ) = ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) supp .0. ) u. ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) ) )
49 eqid 
 |-  ( J mPoly R ) = ( J mPoly R )
50 eqid 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | h finSupp 0 }
51 50 psrbasfsupp 
 |-  { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | ( `' h " NN ) e. Fin }
52 49 5 7 51 9 mplelf 
 |-  ( ph -> F : { h e. ( NN0 ^m J ) | h finSupp 0 } --> B )
53 breq1 
 |-  ( h = ( x |` J ) -> ( h finSupp 0 <-> ( x |` J ) finSupp 0 ) )
54 ssrab2 
 |-  { y e. D | ( y ` A ) = 0 } C_ D
55 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
56 55 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
57 1 56 eqsstrid 
 |-  ( ph -> D C_ ( NN0 ^m I ) )
58 54 57 sstrid 
 |-  ( ph -> { y e. D | ( y ` A ) = 0 } C_ ( NN0 ^m I ) )
59 58 sselda 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> x e. ( NN0 ^m I ) )
60 difssd 
 |-  ( ph -> ( I \ { A } ) C_ I )
61 6 60 eqsstrid 
 |-  ( ph -> J C_ I )
62 61 adantr 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> J C_ I )
63 59 62 elmapssresd 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> ( x |` J ) e. ( NN0 ^m J ) )
64 54 a1i 
 |-  ( ph -> { y e. D | ( y ` A ) = 0 } C_ D )
65 64 sselda 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> x e. D )
66 30 psrbagfsupp 
 |-  ( x e. D -> x finSupp 0 )
67 65 66 syl 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> x finSupp 0 )
68 c0ex 
 |-  0 e. _V
69 68 a1i 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> 0 e. _V )
70 67 69 fsuppres 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> ( x |` J ) finSupp 0 )
71 53 63 70 elrabd 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> ( x |` J ) e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
72 52 71 cofmpt 
 |-  ( ph -> ( F o. ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ) = ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) )
73 72 oveq1d 
 |-  ( ph -> ( ( F o. ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ) supp .0. ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) supp .0. ) )
74 43 mptexd 
 |-  ( ph -> ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) e. _V )
75 suppco 
 |-  ( ( F e. M /\ ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) e. _V ) -> ( ( F o. ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ) supp .0. ) = ( `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) " ( F supp .0. ) ) )
76 9 74 75 syl2anc 
 |-  ( ph -> ( ( F o. ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ) supp .0. ) = ( `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) " ( F supp .0. ) ) )
77 63 fmpttd 
 |-  ( ph -> ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } --> ( NN0 ^m J ) )
78 simpr 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) )
79 eqid 
 |-  ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) = ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) )
80 reseq1 
 |-  ( x = u -> ( x |` J ) = ( u |` J ) )
81 simpllr 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> u e. { y e. D | ( y ` A ) = 0 } )
82 81 resexd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( u |` J ) e. _V )
83 79 80 81 82 fvmptd3 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( u |` J ) )
84 reseq1 
 |-  ( x = v -> ( x |` J ) = ( v |` J ) )
85 simplr 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> v e. { y e. D | ( y ` A ) = 0 } )
86 85 resexd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( v |` J ) e. _V )
87 79 84 85 86 fvmptd3 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) = ( v |` J ) )
88 78 83 87 3eqtr3d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( u |` J ) = ( v |` J ) )
89 6 a1i 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> J = ( I \ { A } ) )
90 89 reseq2d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( u |` J ) = ( u |` ( I \ { A } ) ) )
91 89 reseq2d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( v |` J ) = ( v |` ( I \ { A } ) ) )
92 88 90 91 3eqtr3d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( u |` ( I \ { A } ) ) = ( v |` ( I \ { A } ) ) )
93 fveq1 
 |-  ( y = u -> ( y ` A ) = ( u ` A ) )
94 93 eqeq1d 
 |-  ( y = u -> ( ( y ` A ) = 0 <-> ( u ` A ) = 0 ) )
95 94 81 elrabrd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( u ` A ) = 0 )
96 fveq1 
 |-  ( y = v -> ( y ` A ) = ( v ` A ) )
97 96 eqeq1d 
 |-  ( y = v -> ( ( y ` A ) = 0 <-> ( v ` A ) = 0 ) )
98 97 85 elrabrd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( v ` A ) = 0 )
99 95 98 eqtr4d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( u ` A ) = ( v ` A ) )
100 99 opeq2d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> <. A , ( u ` A ) >. = <. A , ( v ` A ) >. )
101 100 sneqd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> { <. A , ( u ` A ) >. } = { <. A , ( v ` A ) >. } )
102 92 101 uneq12d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> ( ( u |` ( I \ { A } ) ) u. { <. A , ( u ` A ) >. } ) = ( ( v |` ( I \ { A } ) ) u. { <. A , ( v ` A ) >. } ) )
103 57 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> D C_ ( NN0 ^m I ) )
104 54 81 sselid 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> u e. D )
105 103 104 sseldd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> u e. ( NN0 ^m I ) )
106 105 elmaprd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> u : I --> NN0 )
107 106 ffnd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> u Fn I )
108 8 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> A e. I )
109 fnsnsplit 
 |-  ( ( u Fn I /\ A e. I ) -> u = ( ( u |` ( I \ { A } ) ) u. { <. A , ( u ` A ) >. } ) )
110 107 108 109 syl2anc 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> u = ( ( u |` ( I \ { A } ) ) u. { <. A , ( u ` A ) >. } ) )
111 54 85 sselid 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> v e. D )
112 103 111 sseldd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> v e. ( NN0 ^m I ) )
113 112 elmaprd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> v : I --> NN0 )
114 113 ffnd 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> v Fn I )
115 fnsnsplit 
 |-  ( ( v Fn I /\ A e. I ) -> v = ( ( v |` ( I \ { A } ) ) u. { <. A , ( v ` A ) >. } ) )
116 114 108 115 syl2anc 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> v = ( ( v |` ( I \ { A } ) ) u. { <. A , ( v ` A ) >. } ) )
117 102 110 116 3eqtr4d 
 |-  ( ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) /\ ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) ) -> u = v )
118 117 ex 
 |-  ( ( ( ph /\ u e. { y e. D | ( y ` A ) = 0 } ) /\ v e. { y e. D | ( y ` A ) = 0 } ) -> ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) -> u = v ) )
119 118 anasss 
 |-  ( ( ph /\ ( u e. { y e. D | ( y ` A ) = 0 } /\ v e. { y e. D | ( y ` A ) = 0 } ) ) -> ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) -> u = v ) )
120 119 ralrimivva 
 |-  ( ph -> A. u e. { y e. D | ( y ` A ) = 0 } A. v e. { y e. D | ( y ` A ) = 0 } ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) -> u = v ) )
121 dff13 
 |-  ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } -1-1-> ( NN0 ^m J ) <-> ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } --> ( NN0 ^m J ) /\ A. u e. { y e. D | ( y ` A ) = 0 } A. v e. { y e. D | ( y ` A ) = 0 } ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` u ) = ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ` v ) -> u = v ) ) )
122 77 120 121 sylanbrc 
 |-  ( ph -> ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } -1-1-> ( NN0 ^m J ) )
123 df-f1 
 |-  ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } -1-1-> ( NN0 ^m J ) <-> ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } --> ( NN0 ^m J ) /\ Fun `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ) )
124 123 simprbi 
 |-  ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } -1-1-> ( NN0 ^m J ) -> Fun `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) )
125 122 124 syl 
 |-  ( ph -> Fun `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) )
126 49 7 2 9 mplelsfi 
 |-  ( ph -> F finSupp .0. )
127 126 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
128 imafi 
 |-  ( ( Fun `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) /\ ( F supp .0. ) e. Fin ) -> ( `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) " ( F supp .0. ) ) e. Fin )
129 125 127 128 syl2anc 
 |-  ( ph -> ( `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) " ( F supp .0. ) ) e. Fin )
130 76 129 eqeltrd 
 |-  ( ph -> ( ( F o. ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ) supp .0. ) e. Fin )
131 73 130 eqeltrrd 
 |-  ( ph -> ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) supp .0. ) e. Fin )
132 fconstmpt 
 |-  ( ( D \ { y e. D | ( y ` A ) = 0 } ) X. { .0. } ) = ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. )
133 132 oveq1i 
 |-  ( ( ( D \ { y e. D | ( y ` A ) = 0 } ) X. { .0. } ) supp .0. ) = ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. )
134 fczsupp0 
 |-  ( ( ( D \ { y e. D | ( y ` A ) = 0 } ) X. { .0. } ) supp .0. ) = (/)
135 133 134 eqtr3i 
 |-  ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) = (/)
136 0fi 
 |-  (/) e. Fin
137 135 136 eqeltri 
 |-  ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) e. Fin
138 137 a1i 
 |-  ( ph -> ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) e. Fin )
139 131 138 unfid 
 |-  ( ph -> ( ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) supp .0. ) u. ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) ) e. Fin )
140 48 139 eqeltrd 
 |-  ( ph -> ( ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) supp .0. ) e. Fin )
141 34 35 37 140 isfsuppd 
 |-  ( ph -> ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) finSupp .0. )
142 20 141 eqbrtrd 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. )
143 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
144 143 29 31 2 10 mplelbas 
 |-  ( ( ( ( I extendVars R ) ` A ) ` F ) e. N <-> ( ( ( ( I extendVars R ) ` A ) ` F ) e. ( Base ` ( I mPwSer R ) ) /\ ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. ) )
145 33 142 144 sylanbrc 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N )