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