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

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