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 nn0ex 
 |-  NN0 e. _V
55 54 a1i 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> NN0 e. _V )
56 3 difexd 
 |-  ( ph -> ( I \ { A } ) e. _V )
57 6 56 eqeltrid 
 |-  ( ph -> J e. _V )
58 57 adantr 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> J e. _V )
59 3 adantr 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> I e. V )
60 ssrab2 
 |-  { y e. D | ( y ` A ) = 0 } C_ D
61 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
62 61 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) )
63 1 62 eqsstrid 
 |-  ( ph -> D C_ ( NN0 ^m I ) )
64 60 63 sstrid 
 |-  ( ph -> { y e. D | ( y ` A ) = 0 } C_ ( NN0 ^m I ) )
65 64 sselda 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> x e. ( NN0 ^m I ) )
66 59 55 65 elmaprd 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> x : I --> NN0 )
67 difssd 
 |-  ( ph -> ( I \ { A } ) C_ I )
68 6 67 eqsstrid 
 |-  ( ph -> J C_ I )
69 68 adantr 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> J C_ I )
70 66 69 fssresd 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> ( x |` J ) : J --> NN0 )
71 55 58 70 elmapdd 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> ( x |` J ) e. ( NN0 ^m J ) )
72 60 a1i 
 |-  ( ph -> { y e. D | ( y ` A ) = 0 } C_ D )
73 72 sselda 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> x e. D )
74 30 psrbagfsupp 
 |-  ( x e. D -> x finSupp 0 )
75 73 74 syl 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> x finSupp 0 )
76 c0ex 
 |-  0 e. _V
77 76 a1i 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> 0 e. _V )
78 75 77 fsuppres 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> ( x |` J ) finSupp 0 )
79 53 71 78 elrabd 
 |-  ( ( ph /\ x e. { y e. D | ( y ` A ) = 0 } ) -> ( x |` J ) e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
80 52 79 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 ) ) ) )
81 80 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. ) )
82 43 mptexd 
 |-  ( ph -> ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) e. _V )
83 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. ) ) )
84 9 82 83 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. ) ) )
85 71 fmpttd 
 |-  ( ph -> ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } --> ( NN0 ^m J ) )
86 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 ) )
87 eqid 
 |-  ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) = ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) )
88 reseq1 
 |-  ( x = u -> ( x |` J ) = ( u |` J ) )
89 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 } )
90 89 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 )
91 87 88 89 90 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 ) )
92 reseq1 
 |-  ( x = v -> ( x |` J ) = ( v |` J ) )
93 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 } )
94 93 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 )
95 87 92 93 94 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 ) )
96 86 91 95 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 ) )
97 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 } ) )
98 97 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 } ) ) )
99 97 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 } ) ) )
100 96 98 99 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 } ) ) )
101 fveq1 
 |-  ( y = u -> ( y ` A ) = ( u ` A ) )
102 101 eqeq1d 
 |-  ( y = u -> ( ( y ` A ) = 0 <-> ( u ` A ) = 0 ) )
103 102 89 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 )
104 fveq1 
 |-  ( y = v -> ( y ` A ) = ( v ` A ) )
105 104 eqeq1d 
 |-  ( y = v -> ( ( y ` A ) = 0 <-> ( v ` A ) = 0 ) )
106 105 93 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 )
107 103 106 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 ) )
108 107 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 ) >. )
109 108 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 ) >. } )
110 100 109 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 ) >. } ) )
111 3 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 ) ) -> I e. V )
112 54 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 ) ) -> NN0 e. _V )
113 63 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 ) )
114 60 89 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 )
115 113 114 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 ) )
116 111 112 115 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 )
117 116 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 )
118 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 )
119 fnsnsplit 
 |-  ( ( u Fn I /\ A e. I ) -> u = ( ( u |` ( I \ { A } ) ) u. { <. A , ( u ` A ) >. } ) )
120 117 118 119 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 ) >. } ) )
121 60 93 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 )
122 113 121 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 ) )
123 111 112 122 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 )
124 123 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 )
125 fnsnsplit 
 |-  ( ( v Fn I /\ A e. I ) -> v = ( ( v |` ( I \ { A } ) ) u. { <. A , ( v ` A ) >. } ) )
126 124 118 125 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 ) >. } ) )
127 110 120 126 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 )
128 127 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 ) )
129 128 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 ) )
130 129 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 ) )
131 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 ) ) )
132 85 130 131 sylanbrc 
 |-  ( ph -> ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) : { y e. D | ( y ` A ) = 0 } -1-1-> ( NN0 ^m J ) )
133 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 ) ) ) )
134 133 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 ) ) )
135 132 134 syl 
 |-  ( ph -> Fun `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) )
136 49 7 2 9 mplelsfi 
 |-  ( ph -> F finSupp .0. )
137 136 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
138 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 )
139 135 137 138 syl2anc 
 |-  ( ph -> ( `' ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) " ( F supp .0. ) ) e. Fin )
140 84 139 eqeltrd 
 |-  ( ph -> ( ( F o. ( x e. { y e. D | ( y ` A ) = 0 } |-> ( x |` J ) ) ) supp .0. ) e. Fin )
141 81 140 eqeltrrd 
 |-  ( ph -> ( ( x e. { y e. D | ( y ` A ) = 0 } |-> ( F ` ( x |` J ) ) ) supp .0. ) e. Fin )
142 fconstmpt 
 |-  ( ( D \ { y e. D | ( y ` A ) = 0 } ) X. { .0. } ) = ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. )
143 142 oveq1i 
 |-  ( ( ( D \ { y e. D | ( y ` A ) = 0 } ) X. { .0. } ) supp .0. ) = ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. )
144 fczsupp0 
 |-  ( ( ( D \ { y e. D | ( y ` A ) = 0 } ) X. { .0. } ) supp .0. ) = (/)
145 143 144 eqtr3i 
 |-  ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) = (/)
146 0fi 
 |-  (/) e. Fin
147 145 146 eqeltri 
 |-  ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) e. Fin
148 147 a1i 
 |-  ( ph -> ( ( x e. ( D \ { y e. D | ( y ` A ) = 0 } ) |-> .0. ) supp .0. ) e. Fin )
149 141 148 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 )
150 48 149 eqeltrd 
 |-  ( ph -> ( ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) supp .0. ) e. Fin )
151 34 35 37 150 isfsuppd 
 |-  ( ph -> ( x e. D |-> if ( ( x ` A ) = 0 , ( F ` ( x |` J ) ) , .0. ) ) finSupp .0. )
152 20 151 eqbrtrd 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) finSupp .0. )
153 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
154 153 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. ) )
155 33 152 154 sylanbrc 
 |-  ( ph -> ( ( ( I extendVars R ) ` A ) ` F ) e. N )