Metamath Proof Explorer

Theorem esplyind

Description: A recursive formula for the elementary symmetric polynomials. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Hypotheses esplyind.w 
|- W = ( I mPoly R )
esplyind.v 
|- V = ( I mVar R )
esplyind.p 
|- .+ = ( +g ` W )
esplyind.m 
|- .x. = ( .r ` W )
esplyind.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
esplyind.g 
|- G = ( ( I extendVars R ) ` Y )
esplyind.i 
|- ( ph -> I e. Fin )
esplyind.r 
|- ( ph -> R e. Ring )
esplyind.y 
|- ( ph -> Y e. I )
esplyind.j 
|- J = ( I \ { Y } )
esplyind.e 
|- E = ( J eSymPoly R )
esplyind.k 
|- ( ph -> K e. ( 1 ... ( # ` I ) ) )
esplyind.1 
|- C = { h e. ( NN0 ^m J ) | h finSupp 0 }
Assertion esplyind 
|- ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) .+ ( G ` ( E ` K ) ) ) )

Proof

Step Hyp Ref Expression
1 esplyind.w 
 |-  W = ( I mPoly R )
2 esplyind.v 
 |-  V = ( I mVar R )
3 esplyind.p 
 |-  .+ = ( +g ` W )
4 esplyind.m 
 |-  .x. = ( .r ` W )
5 esplyind.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
6 esplyind.g 
 |-  G = ( ( I extendVars R ) ` Y )
7 esplyind.i 
 |-  ( ph -> I e. Fin )
8 esplyind.r 
 |-  ( ph -> R e. Ring )
9 esplyind.y 
 |-  ( ph -> Y e. I )
10 esplyind.j 
 |-  J = ( I \ { Y } )
11 esplyind.e 
 |-  E = ( J eSymPoly R )
12 esplyind.k 
 |-  ( ph -> K e. ( 1 ... ( # ` I ) ) )
13 esplyind.1 
 |-  C = { h e. ( NN0 ^m J ) | h finSupp 0 }
14 ovif12 
 |-  ( if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ( +g ` R ) if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( ( f ` Y ) = 0 , ( ( 0g ` R ) ( +g ` R ) if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) , ( ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ( +g ` R ) ( 0g ` R ) ) )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 eqid 
 |-  ( +g ` R ) = ( +g ` R )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 8 ringgrpd 
 |-  ( ph -> R e. Grp )
19 18 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> R e. Grp )
20 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
21 15 20 8 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
22 21 adantr 
 |-  ( ( ph /\ f e. D ) -> ( 1r ` R ) e. ( Base ` R ) )
23 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
24 15 17 grpidcl 
 |-  ( R e. Grp -> ( 0g ` R ) e. ( Base ` R ) )
25 8 23 24 3syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
26 25 adantr 
 |-  ( ( ph /\ f e. D ) -> ( 0g ` R ) e. ( Base ` R ) )
27 22 26 ifcld 
 |-  ( ( ph /\ f e. D ) -> if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
28 27 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
29 15 16 17 19 28 grplidd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( 0g ` R ) ( +g ` R ) if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
30 snsspr1 
 |-  { 0 } C_ { 0 , 1 }
31 30 biantru 
 |-  ( ran ( f |` J ) C_ { 0 , 1 } <-> ( ran ( f |` J ) C_ { 0 , 1 } /\ { 0 } C_ { 0 , 1 } ) )
32 unss 
 |-  ( ( ran ( f |` J ) C_ { 0 , 1 } /\ { 0 } C_ { 0 , 1 } ) <-> ( ran ( f |` J ) u. { 0 } ) C_ { 0 , 1 } )
33 31 32 bitri 
 |-  ( ran ( f |` J ) C_ { 0 , 1 } <-> ( ran ( f |` J ) u. { 0 } ) C_ { 0 , 1 } )
34 5 ssrab3 
 |-  D C_ ( NN0 ^m I )
35 34 a1i 
 |-  ( ph -> D C_ ( NN0 ^m I ) )
36 35 sselda 
 |-  ( ( ph /\ f e. D ) -> f e. ( NN0 ^m I ) )
37 36 elmaprd 
 |-  ( ( ph /\ f e. D ) -> f : I --> NN0 )
38 37 freld 
 |-  ( ( ph /\ f e. D ) -> Rel f )
39 37 ffnd 
 |-  ( ( ph /\ f e. D ) -> f Fn I )
40 39 fndmd 
 |-  ( ( ph /\ f e. D ) -> dom f = I )
41 10 uneq1i 
 |-  ( J u. { Y } ) = ( ( I \ { Y } ) u. { Y } )
42 9 snssd 
 |-  ( ph -> { Y } C_ I )
43 undifr 
 |-  ( { Y } C_ I <-> ( ( I \ { Y } ) u. { Y } ) = I )
44 42 43 sylib 
 |-  ( ph -> ( ( I \ { Y } ) u. { Y } ) = I )
45 41 44 eqtr2id 
 |-  ( ph -> I = ( J u. { Y } ) )
46 45 adantr 
 |-  ( ( ph /\ f e. D ) -> I = ( J u. { Y } ) )
47 40 46 eqtrd 
 |-  ( ( ph /\ f e. D ) -> dom f = ( J u. { Y } ) )
48 reldmun 
 |-  ( ( Rel f /\ dom f = ( J u. { Y } ) ) -> f = ( ( f |` J ) u. ( f |` { Y } ) ) )
49 38 47 48 syl2anc 
 |-  ( ( ph /\ f e. D ) -> f = ( ( f |` J ) u. ( f |` { Y } ) ) )
50 49 rneqd 
 |-  ( ( ph /\ f e. D ) -> ran f = ran ( ( f |` J ) u. ( f |` { Y } ) ) )
51 rnun 
 |-  ran ( ( f |` J ) u. ( f |` { Y } ) ) = ( ran ( f |` J ) u. ran ( f |` { Y } ) )
52 50 51 eqtr2di 
 |-  ( ( ph /\ f e. D ) -> ( ran ( f |` J ) u. ran ( f |` { Y } ) ) = ran f )
53 39 fnfund 
 |-  ( ( ph /\ f e. D ) -> Fun f )
54 9 adantr 
 |-  ( ( ph /\ f e. D ) -> Y e. I )
55 54 40 eleqtrrd 
 |-  ( ( ph /\ f e. D ) -> Y e. dom f )
56 rnressnsn 
 |-  ( ( Fun f /\ Y e. dom f ) -> ran ( f |` { Y } ) = { ( f ` Y ) } )
57 53 55 56 syl2anc 
 |-  ( ( ph /\ f e. D ) -> ran ( f |` { Y } ) = { ( f ` Y ) } )
58 57 uneq2d 
 |-  ( ( ph /\ f e. D ) -> ( ran ( f |` J ) u. ran ( f |` { Y } ) ) = ( ran ( f |` J ) u. { ( f ` Y ) } ) )
59 52 58 eqtr3d 
 |-  ( ( ph /\ f e. D ) -> ran f = ( ran ( f |` J ) u. { ( f ` Y ) } ) )
60 59 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ran f = ( ran ( f |` J ) u. { ( f ` Y ) } ) )
61 simpr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( f ` Y ) = 0 )
62 61 sneqd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> { ( f ` Y ) } = { 0 } )
63 62 uneq2d 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ran ( f |` J ) u. { ( f ` Y ) } ) = ( ran ( f |` J ) u. { 0 } ) )
64 60 63 eqtrd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ran f = ( ran ( f |` J ) u. { 0 } ) )
65 64 sseq1d 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ran f C_ { 0 , 1 } <-> ( ran ( f |` J ) u. { 0 } ) C_ { 0 , 1 } ) )
66 33 65 bitr4id 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ran ( f |` J ) C_ { 0 , 1 } <-> ran f C_ { 0 , 1 } ) )
67 49 oveq1d 
 |-  ( ( ph /\ f e. D ) -> ( f supp 0 ) = ( ( ( f |` J ) u. ( f |` { Y } ) ) supp 0 ) )
68 36 resexd 
 |-  ( ( ph /\ f e. D ) -> ( f |` J ) e. _V )
69 36 resexd 
 |-  ( ( ph /\ f e. D ) -> ( f |` { Y } ) e. _V )
70 0nn0 
 |-  0 e. NN0
71 70 a1i 
 |-  ( ( ph /\ f e. D ) -> 0 e. NN0 )
72 68 69 71 suppun2 
 |-  ( ( ph /\ f e. D ) -> ( ( ( f |` J ) u. ( f |` { Y } ) ) supp 0 ) = ( ( ( f |` J ) supp 0 ) u. ( ( f |` { Y } ) supp 0 ) ) )
73 67 72 eqtrd 
 |-  ( ( ph /\ f e. D ) -> ( f supp 0 ) = ( ( ( f |` J ) supp 0 ) u. ( ( f |` { Y } ) supp 0 ) ) )
74 73 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( f supp 0 ) = ( ( ( f |` J ) supp 0 ) u. ( ( f |` { Y } ) supp 0 ) ) )
75 fnressn 
 |-  ( ( f Fn I /\ Y e. I ) -> ( f |` { Y } ) = { <. Y , ( f ` Y ) >. } )
76 39 54 75 syl2anc 
 |-  ( ( ph /\ f e. D ) -> ( f |` { Y } ) = { <. Y , ( f ` Y ) >. } )
77 76 oveq1d 
 |-  ( ( ph /\ f e. D ) -> ( ( f |` { Y } ) supp 0 ) = ( { <. Y , ( f ` Y ) >. } supp 0 ) )
78 37 54 ffvelcdmd 
 |-  ( ( ph /\ f e. D ) -> ( f ` Y ) e. NN0 )
79 eqid 
 |-  { <. Y , ( f ` Y ) >. } = { <. Y , ( f ` Y ) >. }
80 79 suppsnop 
 |-  ( ( Y e. I /\ ( f ` Y ) e. NN0 /\ 0 e. NN0 ) -> ( { <. Y , ( f ` Y ) >. } supp 0 ) = if ( ( f ` Y ) = 0 , (/) , { Y } ) )
81 54 78 71 80 syl3anc 
 |-  ( ( ph /\ f e. D ) -> ( { <. Y , ( f ` Y ) >. } supp 0 ) = if ( ( f ` Y ) = 0 , (/) , { Y } ) )
82 77 81 eqtrd 
 |-  ( ( ph /\ f e. D ) -> ( ( f |` { Y } ) supp 0 ) = if ( ( f ` Y ) = 0 , (/) , { Y } ) )
83 82 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( f |` { Y } ) supp 0 ) = if ( ( f ` Y ) = 0 , (/) , { Y } ) )
84 61 iftrued 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> if ( ( f ` Y ) = 0 , (/) , { Y } ) = (/) )
85 83 84 eqtrd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( f |` { Y } ) supp 0 ) = (/) )
86 85 uneq2d 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( ( f |` J ) supp 0 ) u. ( ( f |` { Y } ) supp 0 ) ) = ( ( ( f |` J ) supp 0 ) u. (/) ) )
87 un0 
 |-  ( ( ( f |` J ) supp 0 ) u. (/) ) = ( ( f |` J ) supp 0 )
88 86 87 eqtrdi 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( ( f |` J ) supp 0 ) u. ( ( f |` { Y } ) supp 0 ) ) = ( ( f |` J ) supp 0 ) )
89 74 88 eqtr2d 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( f |` J ) supp 0 ) = ( f supp 0 ) )
90 89 fveqeq2d 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( # ` ( ( f |` J ) supp 0 ) ) = K <-> ( # ` ( f supp 0 ) ) = K ) )
91 66 90 anbi12d 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) <-> ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) ) )
92 91 ifbid 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
93 29 92 eqtrd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( 0g ` R ) ( +g ` R ) if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
94 18 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> R e. Grp )
95 eqid 
 |-  ( Base ` W ) = ( Base ` W )
96 5 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
97 6 fveq1i 
 |-  ( G ` ( E ` ( K - 1 ) ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) )
98 eqid 
 |-  ( Base ` ( J mPoly R ) ) = ( Base ` ( J mPoly R ) )
99 1 fveq2i 
 |-  ( Base ` W ) = ( Base ` ( I mPoly R ) )
100 5 17 7 8 15 10 98 9 99 extvfvalf 
 |-  ( ph -> ( ( I extendVars R ) ` Y ) : ( Base ` ( J mPoly R ) ) --> ( Base ` W ) )
101 11 fveq1i 
 |-  ( E ` ( K - 1 ) ) = ( ( J eSymPoly R ) ` ( K - 1 ) )
102 difssd 
 |-  ( ph -> ( I \ { Y } ) C_ I )
103 10 102 eqsstrid 
 |-  ( ph -> J C_ I )
104 7 103 ssfid 
 |-  ( ph -> J e. Fin )
105 elfznn 
 |-  ( K e. ( 1 ... ( # ` I ) ) -> K e. NN )
106 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
107 12 105 106 3syl 
 |-  ( ph -> ( K - 1 ) e. NN0 )
108 13 104 8 107 98 esplympl 
 |-  ( ph -> ( ( J eSymPoly R ) ` ( K - 1 ) ) e. ( Base ` ( J mPoly R ) ) )
109 101 108 eqeltrid 
 |-  ( ph -> ( E ` ( K - 1 ) ) e. ( Base ` ( J mPoly R ) ) )
110 100 109 ffvelcdmd 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) e. ( Base ` W ) )
111 97 110 eqeltrid 
 |-  ( ph -> ( G ` ( E ` ( K - 1 ) ) ) e. ( Base ` W ) )
112 1 15 95 96 111 mplelf 
 |-  ( ph -> ( G ` ( E ` ( K - 1 ) ) ) : D --> ( Base ` R ) )
113 112 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( G ` ( E ` ( K - 1 ) ) ) : D --> ( Base ` R ) )
114 simplr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> f e. D )
115 indf 
 |-  ( ( I e. Fin /\ { Y } C_ I ) -> ( ( _Ind ` I ) ` { Y } ) : I --> { 0 , 1 } )
116 7 42 115 syl2anc 
 |-  ( ph -> ( ( _Ind ` I ) ` { Y } ) : I --> { 0 , 1 } )
117 70 a1i 
 |-  ( ph -> 0 e. NN0 )
118 1nn0 
 |-  1 e. NN0
119 118 a1i 
 |-  ( ph -> 1 e. NN0 )
120 117 119 prssd 
 |-  ( ph -> { 0 , 1 } C_ NN0 )
121 116 120 fssd 
 |-  ( ph -> ( ( _Ind ` I ) ` { Y } ) : I --> NN0 )
122 121 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( _Ind ` I ) ` { Y } ) : I --> NN0 )
123 7 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> I e. Fin )
124 123 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> I e. Fin )
125 42 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> { Y } C_ I )
126 velsn 
 |-  ( x e. { Y } <-> x = Y )
127 126 bilanri 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> x e. { Y } )
128 ind1 
 |-  ( ( I e. Fin /\ { Y } C_ I /\ x e. { Y } ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) = 1 )
129 124 125 127 128 syl3anc 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) = 1 )
130 37 ad3antrrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> f : I --> NN0 )
131 simplr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> x e. I )
132 130 131 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> ( f ` x ) e. NN0 )
133 simpr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> x = Y )
134 133 fveq2d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> ( f ` x ) = ( f ` Y ) )
135 simpllr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> -. ( f ` Y ) = 0 )
136 135 neqned 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> ( f ` Y ) =/= 0 )
137 134 136 eqnetrd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> ( f ` x ) =/= 0 )
138 elnnne0 
 |-  ( ( f ` x ) e. NN <-> ( ( f ` x ) e. NN0 /\ ( f ` x ) =/= 0 ) )
139 132 137 138 sylanbrc 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> ( f ` x ) e. NN )
140 139 nnge1d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> 1 <_ ( f ` x ) )
141 129 140 eqbrtrd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x = Y ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) <_ ( f ` x ) )
142 123 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> I e. Fin )
143 42 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> { Y } C_ I )
144 simplr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> x e. I )
145 simpr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> x =/= Y )
146 144 145 eldifsnd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> x e. ( I \ { Y } ) )
147 ind0 
 |-  ( ( I e. Fin /\ { Y } C_ I /\ x e. ( I \ { Y } ) ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) = 0 )
148 142 143 146 147 syl3anc 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) = 0 )
149 37 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> f : I --> NN0 )
150 149 ffvelcdmda 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) -> ( f ` x ) e. NN0 )
151 150 adantr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> ( f ` x ) e. NN0 )
152 151 nn0ge0d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> 0 <_ ( f ` x ) )
153 148 152 eqbrtrd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) /\ x =/= Y ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) <_ ( f ` x ) )
154 141 153 pm2.61dane 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) <_ ( f ` x ) )
155 154 ralrimiva 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> A. x e. I ( ( ( _Ind ` I ) ` { Y } ) ` x ) <_ ( f ` x ) )
156 122 ffnd 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( _Ind ` I ) ` { Y } ) Fn I )
157 39 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> f Fn I )
158 inidm 
 |-  ( I i^i I ) = I
159 eqidd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) = ( ( ( _Ind ` I ) ` { Y } ) ` x ) )
160 eqidd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ x e. I ) -> ( f ` x ) = ( f ` x ) )
161 156 157 123 123 158 159 160 ofrfval 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( ( _Ind ` I ) ` { Y } ) oR <_ f <-> A. x e. I ( ( ( _Ind ` I ) ` { Y } ) ` x ) <_ ( f ` x ) ) )
162 155 161 mpbird 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( _Ind ` I ) ` { Y } ) oR <_ f )
163 96 psrbagcon 
 |-  ( ( f e. D /\ ( ( _Ind ` I ) ` { Y } ) : I --> NN0 /\ ( ( _Ind ` I ) ` { Y } ) oR <_ f ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) e. D /\ ( f oF - ( ( _Ind ` I ) ` { Y } ) ) oR <_ f ) )
164 163 simpld 
 |-  ( ( f e. D /\ ( ( _Ind ` I ) ` { Y } ) : I --> NN0 /\ ( ( _Ind ` I ) ` { Y } ) oR <_ f ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) e. D )
165 114 122 162 164 syl3anc 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) e. D )
166 113 165 ffvelcdmd 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) e. ( Base ` R ) )
167 15 16 17 94 166 grpridd 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ( +g ` R ) ( 0g ` R ) ) = ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) )
168 97 fveq1i 
 |-  ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) )
169 168 a1i 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) )
170 8 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> R e. Ring )
171 9 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> Y e. I )
172 109 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( E ` ( K - 1 ) ) e. ( Base ` ( J mPoly R ) ) )
173 5 17 123 170 171 10 98 172 165 extvfvv 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = if ( ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 , ( ( E ` ( K - 1 ) ) ` ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) , ( 0g ` R ) ) )
174 13 104 8 107 17 20 esplyfval3 
 |-  ( ph -> ( ( J eSymPoly R ) ` ( K - 1 ) ) = ( z e. C |-> if ( ( ran z C_ { 0 , 1 } /\ ( # ` ( z supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
175 101 174 eqtrid 
 |-  ( ph -> ( E ` ( K - 1 ) ) = ( z e. C |-> if ( ( ran z C_ { 0 , 1 } /\ ( # ` ( z supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
176 175 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( E ` ( K - 1 ) ) = ( z e. C |-> if ( ( ran z C_ { 0 , 1 } /\ ( # ` ( z supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
177 52 ad4antr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ( ran ( f |` J ) u. ran ( f |` { Y } ) ) = ran f )
178 simpr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) )
179 116 ffnd 
 |-  ( ph -> ( ( _Ind ` I ) ` { Y } ) Fn I )
180 179 adantr 
 |-  ( ( ph /\ f e. D ) -> ( ( _Ind ` I ) ` { Y } ) Fn I )
181 7 adantr 
 |-  ( ( ph /\ f e. D ) -> I e. Fin )
182 39 180 181 181 158 offn 
 |-  ( ( ph /\ f e. D ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) Fn I )
183 182 ad3antrrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) Fn I )
184 103 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> J C_ I )
185 183 184 fnssresd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) Fn J )
186 fneq1 
 |-  ( z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) -> ( z Fn J <-> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) Fn J ) )
187 186 biimpar 
 |-  ( ( z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) Fn J ) -> z Fn J )
188 178 185 187 syl2anc 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> z Fn J )
189 39 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> f Fn I )
190 103 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> J C_ I )
191 189 190 fnssresd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f |` J ) Fn J )
192 191 adantr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ( f |` J ) Fn J )
193 simplr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) )
194 193 fveq1d 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( z ` x ) = ( ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ` x ) )
195 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> x e. J )
196 195 fvresd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ` x ) = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` x ) )
197 189 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> f Fn I )
198 156 adantr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( _Ind ` I ) ` { Y } ) Fn I )
199 198 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( _Ind ` I ) ` { Y } ) Fn I )
200 181 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> I e. Fin )
201 200 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> I e. Fin )
202 184 sselda 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> x e. I )
203 fnfvof 
 |-  ( ( ( f Fn I /\ ( ( _Ind ` I ) ` { Y } ) Fn I ) /\ ( I e. Fin /\ x e. I ) ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` x ) = ( ( f ` x ) - ( ( ( _Ind ` I ) ` { Y } ) ` x ) ) )
204 197 199 201 202 203 syl22anc 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` x ) = ( ( f ` x ) - ( ( ( _Ind ` I ) ` { Y } ) ` x ) ) )
205 42 ad5antr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> { Y } C_ I )
206 195 10 eleqtrdi 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> x e. ( I \ { Y } ) )
207 201 205 206 147 syl3anc 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( ( _Ind ` I ) ` { Y } ) ` x ) = 0 )
208 207 oveq2d 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( f ` x ) - ( ( ( _Ind ` I ) ` { Y } ) ` x ) ) = ( ( f ` x ) - 0 ) )
209 149 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> f : I --> NN0 )
210 209 202 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( f ` x ) e. NN0 )
211 210 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( f ` x ) e. CC )
212 211 subid1d 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( f ` x ) - 0 ) = ( f ` x ) )
213 195 fvresd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( f |` J ) ` x ) = ( f ` x ) )
214 212 213 eqtr4d 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( f ` x ) - 0 ) = ( ( f |` J ) ` x ) )
215 204 208 214 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` x ) = ( ( f |` J ) ` x ) )
216 194 196 215 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ x e. J ) -> ( z ` x ) = ( ( f |` J ) ` x ) )
217 188 192 216 eqfnfvd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> z = ( f |` J ) )
218 217 rneqd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ran z = ran ( f |` J ) )
219 218 adantr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ran z = ran ( f |` J ) )
220 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ran z C_ { 0 , 1 } )
221 219 220 eqsstrrd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ran ( f |` J ) C_ { 0 , 1 } )
222 53 ad4antr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> Fun f )
223 55 ad4antr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> Y e. dom f )
224 222 223 56 syl2anc 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ran ( f |` { Y } ) = { ( f ` Y ) } )
225 78 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f ` Y ) e. NN0 )
226 225 nn0cnd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f ` Y ) e. CC )
227 116 9 ffvelcdmd 
 |-  ( ph -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) e. { 0 , 1 } )
228 120 227 sseldd 
 |-  ( ph -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) e. NN0 )
229 228 nn0cnd 
 |-  ( ph -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) e. CC )
230 229 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) e. CC )
231 171 adantr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> Y e. I )
232 fnfvof 
 |-  ( ( ( f Fn I /\ ( ( _Ind ` I ) ` { Y } ) Fn I ) /\ ( I e. Fin /\ Y e. I ) ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = ( ( f ` Y ) - ( ( ( _Ind ` I ) ` { Y } ) ` Y ) ) )
233 189 198 200 231 232 syl22anc 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = ( ( f ` Y ) - ( ( ( _Ind ` I ) ` { Y } ) ` Y ) ) )
234 simpr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 )
235 233 234 eqtr3d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f ` Y ) - ( ( ( _Ind ` I ) ` { Y } ) ` Y ) ) = 0 )
236 226 230 235 subeq0d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f ` Y ) = ( ( ( _Ind ` I ) ` { Y } ) ` Y ) )
237 snidg 
 |-  ( Y e. I -> Y e. { Y } )
238 9 237 syl 
 |-  ( ph -> Y e. { Y } )
239 ind1 
 |-  ( ( I e. Fin /\ { Y } C_ I /\ Y e. { Y } ) -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) = 1 )
240 7 42 238 239 syl3anc 
 |-  ( ph -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) = 1 )
241 240 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) = 1 )
242 236 241 eqtrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f ` Y ) = 1 )
243 242 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ( f ` Y ) = 1 )
244 243 sneqd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> { ( f ` Y ) } = { 1 } )
245 224 244 eqtrd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ran ( f |` { Y } ) = { 1 } )
246 snsspr2 
 |-  { 1 } C_ { 0 , 1 }
247 245 246 eqsstrdi 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ran ( f |` { Y } ) C_ { 0 , 1 } )
248 221 247 unssd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ( ran ( f |` J ) u. ran ( f |` { Y } ) ) C_ { 0 , 1 } )
249 177 248 eqsstrrd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran z C_ { 0 , 1 } ) -> ran f C_ { 0 , 1 } )
250 217 adantr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran f C_ { 0 , 1 } ) -> z = ( f |` J ) )
251 250 rneqd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran f C_ { 0 , 1 } ) -> ran z = ran ( f |` J ) )
252 rnresss 
 |-  ran ( f |` J ) C_ ran f
253 simpr 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran f C_ { 0 , 1 } ) -> ran f C_ { 0 , 1 } )
254 252 253 sstrid 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran f C_ { 0 , 1 } ) -> ran ( f |` J ) C_ { 0 , 1 } )
255 251 254 eqsstrd 
 |-  ( ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) /\ ran f C_ { 0 , 1 } ) -> ran z C_ { 0 , 1 } )
256 249 255 impbida 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ( ran z C_ { 0 , 1 } <-> ran f C_ { 0 , 1 } ) )
257 217 oveq1d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ( z supp 0 ) = ( ( f |` J ) supp 0 ) )
258 257 fveqeq2d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ( ( # ` ( z supp 0 ) ) = ( K - 1 ) <-> ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) ) )
259 256 258 anbi12d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> ( ( ran z C_ { 0 , 1 } /\ ( # ` ( z supp 0 ) ) = ( K - 1 ) ) <-> ( ran f C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) ) ) )
260 259 ifbid 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ z = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) -> if ( ( ran z C_ { 0 , 1 } /\ ( # ` ( z supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
261 breq1 
 |-  ( h = ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) -> ( h finSupp 0 <-> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) finSupp 0 ) )
262 34 165 sselid 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) e. ( NN0 ^m I ) )
263 262 adantr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) e. ( NN0 ^m I ) )
264 263 190 elmapssresd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) e. ( NN0 ^m J ) )
265 breq1 
 |-  ( h = ( f oF - ( ( _Ind ` I ) ` { Y } ) ) -> ( h finSupp 0 <-> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) finSupp 0 ) )
266 165 adantr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) e. D )
267 266 5 eleqtrdi 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
268 265 267 elrabrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f oF - ( ( _Ind ` I ) ` { Y } ) ) finSupp 0 )
269 70 a1i 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> 0 e. NN0 )
270 268 269 fsuppres 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) finSupp 0 )
271 261 264 270 elrabd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
272 271 13 eleqtrrdi 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) e. C )
273 22 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( 1r ` R ) e. ( Base ` R ) )
274 26 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( 0g ` R ) e. ( Base ` R ) )
275 273 274 ifcld 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
276 176 260 272 275 fvmptd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( E ` ( K - 1 ) ) ` ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
277 eqcom 
 |-  ( ( K - 1 ) = ( # ` ( ( f |` J ) supp 0 ) ) <-> ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) )
278 fz1ssfz0 
 |-  ( 1 ... ( # ` I ) ) C_ ( 0 ... ( # ` I ) )
279 fz0ssnn0 
 |-  ( 0 ... ( # ` I ) ) C_ NN0
280 278 279 sstri 
 |-  ( 1 ... ( # ` I ) ) C_ NN0
281 280 12 sselid 
 |-  ( ph -> K e. NN0 )
282 281 nn0cnd 
 |-  ( ph -> K e. CC )
283 282 ad3antrrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> K e. CC )
284 1cnd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> 1 e. CC )
285 c0ex 
 |-  0 e. _V
286 285 a1i 
 |-  ( ( ph /\ f e. D ) -> 0 e. _V )
287 37 181 286 fidmfisupp 
 |-  ( ( ph /\ f e. D ) -> f finSupp 0 )
288 287 286 fsuppres 
 |-  ( ( ph /\ f e. D ) -> ( f |` J ) finSupp 0 )
289 288 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f |` J ) finSupp 0 )
290 289 fsuppimpd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f |` J ) supp 0 ) e. Fin )
291 hashcl 
 |-  ( ( ( f |` J ) supp 0 ) e. Fin -> ( # ` ( ( f |` J ) supp 0 ) ) e. NN0 )
292 290 291 syl 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( # ` ( ( f |` J ) supp 0 ) ) e. NN0 )
293 292 nn0cnd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( # ` ( ( f |` J ) supp 0 ) ) e. CC )
294 283 284 293 subadd2d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( K - 1 ) = ( # ` ( ( f |` J ) supp 0 ) ) <-> ( ( # ` ( ( f |` J ) supp 0 ) ) + 1 ) = K ) )
295 277 294 bitr3id 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) <-> ( ( # ` ( ( f |` J ) supp 0 ) ) + 1 ) = K ) )
296 73 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f supp 0 ) = ( ( ( f |` J ) supp 0 ) u. ( ( f |` { Y } ) supp 0 ) ) )
297 82 ad2antrr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f |` { Y } ) supp 0 ) = if ( ( f ` Y ) = 0 , (/) , { Y } ) )
298 simplr 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> -. ( f ` Y ) = 0 )
299 298 iffalsed 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> if ( ( f ` Y ) = 0 , (/) , { Y } ) = { Y } )
300 297 299 eqtrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f |` { Y } ) supp 0 ) = { Y } )
301 300 uneq2d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( ( f |` J ) supp 0 ) u. ( ( f |` { Y } ) supp 0 ) ) = ( ( ( f |` J ) supp 0 ) u. { Y } ) )
302 296 301 eqtrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( f supp 0 ) = ( ( ( f |` J ) supp 0 ) u. { Y } ) )
303 302 fveq2d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( # ` ( f supp 0 ) ) = ( # ` ( ( ( f |` J ) supp 0 ) u. { Y } ) ) )
304 suppssdm 
 |-  ( ( f |` J ) supp 0 ) C_ dom ( f |` J )
305 resdmss 
 |-  dom ( f |` J ) C_ J
306 304 305 sstri 
 |-  ( ( f |` J ) supp 0 ) C_ J
307 306 a1i 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( f |` J ) supp 0 ) C_ J )
308 10 eqimssi 
 |-  J C_ ( I \ { Y } )
309 ssdifsn 
 |-  ( J C_ ( I \ { Y } ) <-> ( J C_ I /\ -. Y e. J ) )
310 308 309 mpbi 
 |-  ( J C_ I /\ -. Y e. J )
311 310 simpri 
 |-  -. Y e. J
312 311 a1i 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> -. Y e. J )
313 307 312 ssneldd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> -. Y e. ( ( f |` J ) supp 0 ) )
314 hashunsng 
 |-  ( Y e. I -> ( ( ( ( f |` J ) supp 0 ) e. Fin /\ -. Y e. ( ( f |` J ) supp 0 ) ) -> ( # ` ( ( ( f |` J ) supp 0 ) u. { Y } ) ) = ( ( # ` ( ( f |` J ) supp 0 ) ) + 1 ) ) )
315 314 imp 
 |-  ( ( Y e. I /\ ( ( ( f |` J ) supp 0 ) e. Fin /\ -. Y e. ( ( f |` J ) supp 0 ) ) ) -> ( # ` ( ( ( f |` J ) supp 0 ) u. { Y } ) ) = ( ( # ` ( ( f |` J ) supp 0 ) ) + 1 ) )
316 231 290 313 315 syl12anc 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( # ` ( ( ( f |` J ) supp 0 ) u. { Y } ) ) = ( ( # ` ( ( f |` J ) supp 0 ) ) + 1 ) )
317 303 316 eqtrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( # ` ( f supp 0 ) ) = ( ( # ` ( ( f |` J ) supp 0 ) ) + 1 ) )
318 317 eqeq1d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( # ` ( f supp 0 ) ) = K <-> ( ( # ` ( ( f |` J ) supp 0 ) ) + 1 ) = K ) )
319 295 318 bitr4d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) <-> ( # ` ( f supp 0 ) ) = K ) )
320 319 anbi2d 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( ran f C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) ) <-> ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) ) )
321 320 ifbid 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = ( K - 1 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
322 276 321 eqtrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( ( E ` ( K - 1 ) ) ` ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
323 simpr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ran f C_ { 0 , 1 } )
324 157 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> f Fn I )
325 171 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> Y e. I )
326 324 325 fnfvelrnd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( f ` Y ) e. ran f )
327 323 326 sseldd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( f ` Y ) e. { 0 , 1 } )
328 simpllr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> -. ( f ` Y ) = 0 )
329 328 neqned 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( f ` Y ) =/= 0 )
330 78 nn0cnd 
 |-  ( ( ph /\ f e. D ) -> ( f ` Y ) e. CC )
331 330 ad3antrrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( f ` Y ) e. CC )
332 1cnd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> 1 e. CC )
333 simplr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 )
334 156 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( ( _Ind ` I ) ` { Y } ) Fn I )
335 123 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> I e. Fin )
336 324 334 335 325 232 syl22anc 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = ( ( f ` Y ) - ( ( ( _Ind ` I ) ` { Y } ) ` Y ) ) )
337 240 ad4antr 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( ( ( _Ind ` I ) ` { Y } ) ` Y ) = 1 )
338 337 oveq2d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( ( f ` Y ) - ( ( ( _Ind ` I ) ` { Y } ) ` Y ) ) = ( ( f ` Y ) - 1 ) )
339 336 338 eqtrd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = ( ( f ` Y ) - 1 ) )
340 339 eqeq1d 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 <-> ( ( f ` Y ) - 1 ) = 0 ) )
341 333 340 mtbid 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> -. ( ( f ` Y ) - 1 ) = 0 )
342 subeq0 
 |-  ( ( ( f ` Y ) e. CC /\ 1 e. CC ) -> ( ( ( f ` Y ) - 1 ) = 0 <-> ( f ` Y ) = 1 ) )
343 342 notbid 
 |-  ( ( ( f ` Y ) e. CC /\ 1 e. CC ) -> ( -. ( ( f ` Y ) - 1 ) = 0 <-> -. ( f ` Y ) = 1 ) )
344 343 biimpa 
 |-  ( ( ( ( f ` Y ) e. CC /\ 1 e. CC ) /\ -. ( ( f ` Y ) - 1 ) = 0 ) -> -. ( f ` Y ) = 1 )
345 331 332 341 344 syl21anc 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> -. ( f ` Y ) = 1 )
346 345 neqned 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> ( f ` Y ) =/= 1 )
347 329 346 nelprd 
 |-  ( ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) /\ ran f C_ { 0 , 1 } ) -> -. ( f ` Y ) e. { 0 , 1 } )
348 327 347 pm2.65da 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> -. ran f C_ { 0 , 1 } )
349 348 intnanrd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> -. ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) )
350 349 iffalsed 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
351 350 eqcomd 
 |-  ( ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) /\ -. ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 ) -> ( 0g ` R ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
352 322 351 ifeqda 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> if ( ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ` Y ) = 0 , ( ( E ` ( K - 1 ) ) ` ( ( f oF - ( ( _Ind ` I ) ` { Y } ) ) |` J ) ) , ( 0g ` R ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
353 169 173 352 3eqtrd 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
354 167 353 eqtrd 
 |-  ( ( ( ph /\ f e. D ) /\ -. ( f ` Y ) = 0 ) -> ( ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ( +g ` R ) ( 0g ` R ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
355 93 354 ifeqda 
 |-  ( ( ph /\ f e. D ) -> if ( ( f ` Y ) = 0 , ( ( 0g ` R ) ( +g ` R ) if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) , ( ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ( +g ` R ) ( 0g ` R ) ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
356 14 355 eqtrid 
 |-  ( ( ph /\ f e. D ) -> ( if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ( +g ` R ) if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
357 356 mpteq2dva 
 |-  ( ph -> ( f e. D |-> ( if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ( +g ` R ) if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) ) = ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
358 1 7 8 mplringd 
 |-  ( ph -> W e. Ring )
359 1 2 95 7 8 9 mvrcl 
 |-  ( ph -> ( V ` Y ) e. ( Base ` W ) )
360 95 4 358 359 111 ringcld 
 |-  ( ph -> ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) e. ( Base ` W ) )
361 6 fveq1i 
 |-  ( G ` ( E ` K ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) )
362 11 fveq1i 
 |-  ( E ` K ) = ( ( J eSymPoly R ) ` K )
363 13 104 8 281 98 esplympl 
 |-  ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) )
364 362 363 eqeltrid 
 |-  ( ph -> ( E ` K ) e. ( Base ` ( J mPoly R ) ) )
365 100 364 ffvelcdmd 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) e. ( Base ` W ) )
366 361 365 eqeltrid 
 |-  ( ph -> ( G ` ( E ` K ) ) e. ( Base ` W ) )
367 1 95 16 3 360 366 mpladd 
 |-  ( ph -> ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) .+ ( G ` ( E ` K ) ) ) = ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) oF ( +g ` R ) ( G ` ( E ` K ) ) ) )
368 2 fveq1i 
 |-  ( V ` Y ) = ( ( I mVar R ) ` Y )
369 eqid 
 |-  ( ( _Ind ` I ) ` { Y } ) = ( ( _Ind ` I ) ` { Y } )
370 1 368 95 4 17 5 369 7 9 8 111 mplmulmvr 
 |-  ( ph -> ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) = ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ) )
371 6 a1i 
 |-  ( ph -> G = ( ( I extendVars R ) ` Y ) )
372 13 104 8 281 17 20 esplyfval3 
 |-  ( ph -> ( ( J eSymPoly R ) ` K ) = ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
373 362 372 eqtrid 
 |-  ( ph -> ( E ` K ) = ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
374 371 373 fveq12d 
 |-  ( ph -> ( G ` ( E ` K ) ) = ( ( ( I extendVars R ) ` Y ) ` ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
375 372 363 eqeltrrd 
 |-  ( ph -> ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( Base ` ( J mPoly R ) ) )
376 5 17 7 8 9 10 98 375 extvfv 
 |-  ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. D |-> if ( ( f ` Y ) = 0 , ( ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ` ( f |` J ) ) , ( 0g ` R ) ) ) )
377 rneq 
 |-  ( g = ( f |` J ) -> ran g = ran ( f |` J ) )
378 377 sseq1d 
 |-  ( g = ( f |` J ) -> ( ran g C_ { 0 , 1 } <-> ran ( f |` J ) C_ { 0 , 1 } ) )
379 oveq1 
 |-  ( g = ( f |` J ) -> ( g supp 0 ) = ( ( f |` J ) supp 0 ) )
380 379 fveqeq2d 
 |-  ( g = ( f |` J ) -> ( ( # ` ( g supp 0 ) ) = K <-> ( # ` ( ( f |` J ) supp 0 ) ) = K ) )
381 378 380 anbi12d 
 |-  ( g = ( f |` J ) -> ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) <-> ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) ) )
382 381 ifbid 
 |-  ( g = ( f |` J ) -> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
383 eqidd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
384 breq1 
 |-  ( h = ( f |` J ) -> ( h finSupp 0 <-> ( f |` J ) finSupp 0 ) )
385 nn0ex 
 |-  NN0 e. _V
386 385 a1i 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> NN0 e. _V )
387 104 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> J e. Fin )
388 37 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> f : I --> NN0 )
389 103 ad2antrr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> J C_ I )
390 388 389 fssresd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( f |` J ) : J --> NN0 )
391 386 387 390 elmapdd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( f |` J ) e. ( NN0 ^m J ) )
392 288 adantr 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( f |` J ) finSupp 0 )
393 384 391 392 elrabd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( f |` J ) e. { h e. ( NN0 ^m J ) | h finSupp 0 } )
394 393 13 eleqtrrdi 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( f |` J ) e. C )
395 fvexd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( 1r ` R ) e. _V )
396 fvexd 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( 0g ` R ) e. _V )
397 395 396 ifcld 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
398 382 383 394 397 fvmptd4 
 |-  ( ( ( ph /\ f e. D ) /\ ( f ` Y ) = 0 ) -> ( ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ` ( f |` J ) ) = if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) )
399 398 ifeq1da 
 |-  ( ( ph /\ f e. D ) -> if ( ( f ` Y ) = 0 , ( ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ` ( f |` J ) ) , ( 0g ` R ) ) = if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
400 399 mpteq2dva 
 |-  ( ph -> ( f e. D |-> if ( ( f ` Y ) = 0 , ( ( g e. C |-> if ( ( ran g C_ { 0 , 1 } /\ ( # ` ( g supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) ` ( f |` J ) ) , ( 0g ` R ) ) ) = ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) )
401 374 376 400 3eqtrd 
 |-  ( ph -> ( G ` ( E ` K ) ) = ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) )
402 370 401 oveq12d 
 |-  ( ph -> ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) oF ( +g ` R ) ( G ` ( E ` K ) ) ) = ( ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ) oF ( +g ` R ) ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) ) )
403 ovex 
 |-  ( NN0 ^m I ) e. _V
404 5 403 rabex2 
 |-  D e. _V
405 404 a1i 
 |-  ( ph -> D e. _V )
406 nfv 
 |-  F/ f ph
407 fvexd 
 |-  ( ( ph /\ f e. D ) -> ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) e. _V )
408 26 407 ifexd 
 |-  ( ( ph /\ f e. D ) -> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) e. _V )
409 eqid 
 |-  ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ) = ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) )
410 406 408 409 fnmptd 
 |-  ( ph -> ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ) Fn D )
411 27 26 ifcld 
 |-  ( ( ph /\ f e. D ) -> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) e. ( Base ` R ) )
412 eqid 
 |-  ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
413 406 411 412 fnmptd 
 |-  ( ph -> ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) Fn D )
414 ofmpteq 
 |-  ( ( D e. _V /\ ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ) Fn D /\ ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) Fn D ) -> ( ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ) oF ( +g ` R ) ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) ) = ( f e. D |-> ( if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ( +g ` R ) if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) ) )
415 405 410 413 414 syl3anc 
 |-  ( ph -> ( ( f e. D |-> if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ) oF ( +g ` R ) ( f e. D |-> if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) ) = ( f e. D |-> ( if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ( +g ` R ) if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) ) )
416 367 402 415 3eqtrd 
 |-  ( ph -> ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) .+ ( G ` ( E ` K ) ) ) = ( f e. D |-> ( if ( ( f ` Y ) = 0 , ( 0g ` R ) , ( ( G ` ( E ` ( K - 1 ) ) ) ` ( f oF - ( ( _Ind ` I ) ` { Y } ) ) ) ) ( +g ` R ) if ( ( f ` Y ) = 0 , if ( ( ran ( f |` J ) C_ { 0 , 1 } /\ ( # ` ( ( f |` J ) supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) ) )
417 5 7 8 281 17 20 esplyfval3 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = ( f e. D |-> if ( ( ran f C_ { 0 , 1 } /\ ( # ` ( f supp 0 ) ) = K ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
418 357 416 417 3eqtr4rd 
 |-  ( ph -> ( ( I eSymPoly R ) ` K ) = ( ( ( V ` Y ) .x. ( G ` ( E ` ( K - 1 ) ) ) ) .+ ( G ` ( E ` K ) ) ) )