Metamath Proof Explorer

Theorem vieta

Description: Vieta's Formulas: Coefficients of a monic polynomial F expressed as a product of linear polynomials of the form X - Z can be expressed in terms of elementary symmetric polynomials. The formulas appear in Chapter 6 of Lang, p. 190. Theorem vieta1 is a special case for the complex numbers, for the case K = 1 . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses vieta.w 
|- W = ( Poly1 ` R )
vieta.b 
|- B = ( Base ` R )
vieta.3 
|- .- = ( -g ` W )
vieta.m 
|- M = ( mulGrp ` W )
vieta.q 
|- Q = ( I eval R )
vieta.e 
|- E = ( I eSymPoly R )
vieta.n 
|- N = ( invg ` R )
vieta.1 
|- .1. = ( 1r ` R )
vieta.t 
|- .x. = ( .r ` R )
vieta.x 
|- X = ( var1 ` R )
vieta.a 
|- A = ( algSc ` W )
vieta.p 
|- .^ = ( .g ` ( mulGrp ` R ) )
vieta.h 
|- H = ( # ` I )
vieta.i 
|- ( ph -> I e. Fin )
vieta.r 
|- ( ph -> R e. IDomn )
vieta.z 
|- ( ph -> Z : I --> B )
vieta.f 
|- F = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) )
vieta.k 
|- ( ph -> K e. ( 0 ... H ) )
vieta.c 
|- C = ( coe1 ` F )
Assertion vieta 
|- ( ph -> ( C ` ( H - K ) ) = ( ( K .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` K ) ) ` Z ) ) )

Proof

Step Hyp Ref Expression
1 vieta.w 
 |-  W = ( Poly1 ` R )
2 vieta.b 
 |-  B = ( Base ` R )
3 vieta.3 
 |-  .- = ( -g ` W )
4 vieta.m 
 |-  M = ( mulGrp ` W )
5 vieta.q 
 |-  Q = ( I eval R )
6 vieta.e 
 |-  E = ( I eSymPoly R )
7 vieta.n 
 |-  N = ( invg ` R )
8 vieta.1 
 |-  .1. = ( 1r ` R )
9 vieta.t 
 |-  .x. = ( .r ` R )
10 vieta.x 
 |-  X = ( var1 ` R )
11 vieta.a 
 |-  A = ( algSc ` W )
12 vieta.p 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
13 vieta.h 
 |-  H = ( # ` I )
14 vieta.i 
 |-  ( ph -> I e. Fin )
15 vieta.r 
 |-  ( ph -> R e. IDomn )
16 vieta.z 
 |-  ( ph -> Z : I --> B )
17 vieta.f 
 |-  F = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) )
18 vieta.k 
 |-  ( ph -> K e. ( 0 ... H ) )
19 vieta.c 
 |-  C = ( coe1 ` F )
20 fveq1 
 |-  ( z = Z -> ( z ` n ) = ( Z ` n ) )
21 20 fveq2d 
 |-  ( z = Z -> ( A ` ( z ` n ) ) = ( A ` ( Z ` n ) ) )
22 21 oveq2d 
 |-  ( z = Z -> ( X .- ( A ` ( z ` n ) ) ) = ( X .- ( A ` ( Z ` n ) ) ) )
23 22 mpteq2dv 
 |-  ( z = Z -> ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) )
24 23 oveq2d 
 |-  ( z = Z -> ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) )
25 24 17 eqtr4di 
 |-  ( z = Z -> ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = F )
26 25 fveq2d 
 |-  ( z = Z -> ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` F ) )
27 26 19 eqtr4di 
 |-  ( z = Z -> ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = C )
28 27 fveq1d 
 |-  ( z = Z -> ( ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( H - k ) ) = ( C ` ( H - k ) ) )
29 fveq2 
 |-  ( z = Z -> ( ( Q ` ( E ` k ) ) ` z ) = ( ( Q ` ( E ` k ) ) ` Z ) )
30 29 oveq2d 
 |-  ( z = Z -> ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) )
31 28 30 eqeq12d 
 |-  ( z = Z -> ( ( ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( H - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` z ) ) <-> ( C ` ( H - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ) )
32 oveq2 
 |-  ( k = K -> ( H - k ) = ( H - K ) )
33 32 fveq2d 
 |-  ( k = K -> ( C ` ( H - k ) ) = ( C ` ( H - K ) ) )
34 oveq1 
 |-  ( k = K -> ( k .^ ( N ` .1. ) ) = ( K .^ ( N ` .1. ) ) )
35 2fveq3 
 |-  ( k = K -> ( Q ` ( E ` k ) ) = ( Q ` ( E ` K ) ) )
36 35 fveq1d 
 |-  ( k = K -> ( ( Q ` ( E ` k ) ) ` Z ) = ( ( Q ` ( E ` K ) ) ` Z ) )
37 34 36 oveq12d 
 |-  ( k = K -> ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) = ( ( K .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` K ) ) ` Z ) ) )
38 33 37 eqeq12d 
 |-  ( k = K -> ( ( C ` ( H - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) <-> ( C ` ( H - K ) ) = ( ( K .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` K ) ) ` Z ) ) ) )
39 oveq2 
 |-  ( j = (/) -> ( B ^m j ) = ( B ^m (/) ) )
40 2 fvexi 
 |-  B e. _V
41 mapdm0 
 |-  ( B e. _V -> ( B ^m (/) ) = { (/) } )
42 40 41 ax-mp 
 |-  ( B ^m (/) ) = { (/) }
43 39 42 eqtrdi 
 |-  ( j = (/) -> ( B ^m j ) = { (/) } )
44 fveq2 
 |-  ( j = (/) -> ( # ` j ) = ( # ` (/) ) )
45 44 oveq2d 
 |-  ( j = (/) -> ( 0 ... ( # ` j ) ) = ( 0 ... ( # ` (/) ) ) )
46 hash0 
 |-  ( # ` (/) ) = 0
47 46 oveq2i 
 |-  ( 0 ... ( # ` (/) ) ) = ( 0 ... 0 )
48 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
49 47 48 eqtri 
 |-  ( 0 ... ( # ` (/) ) ) = { 0 }
50 45 49 eqtrdi 
 |-  ( j = (/) -> ( 0 ... ( # ` j ) ) = { 0 } )
51 mpteq1 
 |-  ( j = (/) -> ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. (/) |-> ( X .- ( A ` ( z ` n ) ) ) ) )
52 mpt0 
 |-  ( n e. (/) |-> ( X .- ( A ` ( z ` n ) ) ) ) = (/)
53 51 52 eqtrdi 
 |-  ( j = (/) -> ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) = (/) )
54 53 oveq2d 
 |-  ( j = (/) -> ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum (/) ) )
55 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
56 55 gsum0 
 |-  ( M gsum (/) ) = ( 0g ` M )
57 54 56 eqtrdi 
 |-  ( j = (/) -> ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( 0g ` M ) )
58 57 fveq2d 
 |-  ( j = (/) -> ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` ( 0g ` M ) ) )
59 44 oveq1d 
 |-  ( j = (/) -> ( ( # ` j ) - k ) = ( ( # ` (/) ) - k ) )
60 46 oveq1i 
 |-  ( ( # ` (/) ) - k ) = ( 0 - k )
61 59 60 eqtrdi 
 |-  ( j = (/) -> ( ( # ` j ) - k ) = ( 0 - k ) )
62 58 61 fveq12d 
 |-  ( j = (/) -> ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) )
63 oveq1 
 |-  ( j = (/) -> ( j eval R ) = ( (/) eval R ) )
64 oveq1 
 |-  ( j = (/) -> ( j eSymPoly R ) = ( (/) eSymPoly R ) )
65 64 fveq1d 
 |-  ( j = (/) -> ( ( j eSymPoly R ) ` k ) = ( ( (/) eSymPoly R ) ` k ) )
66 63 65 fveq12d 
 |-  ( j = (/) -> ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) = ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) )
67 66 fveq1d 
 |-  ( j = (/) -> ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) = ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) )
68 67 oveq2d 
 |-  ( j = (/) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) )
69 62 68 eqeq12d 
 |-  ( j = (/) -> ( ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) ) )
70 50 69 raleqbidv 
 |-  ( j = (/) -> ( A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) ) )
71 43 70 raleqbidv 
 |-  ( j = (/) -> ( A. z e. ( B ^m j ) A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. z e. { (/) } A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) ) )
72 oveq2 
 |-  ( j = i -> ( B ^m j ) = ( B ^m i ) )
73 fveq2 
 |-  ( j = i -> ( # ` j ) = ( # ` i ) )
74 73 oveq2d 
 |-  ( j = i -> ( 0 ... ( # ` j ) ) = ( 0 ... ( # ` i ) ) )
75 mpteq1 
 |-  ( j = i -> ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) )
76 75 oveq2d 
 |-  ( j = i -> ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) )
77 76 fveq2d 
 |-  ( j = i -> ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) )
78 73 oveq1d 
 |-  ( j = i -> ( ( # ` j ) - k ) = ( ( # ` i ) - k ) )
79 77 78 fveq12d 
 |-  ( j = i -> ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) )
80 oveq1 
 |-  ( j = i -> ( j eval R ) = ( i eval R ) )
81 oveq1 
 |-  ( j = i -> ( j eSymPoly R ) = ( i eSymPoly R ) )
82 81 fveq1d 
 |-  ( j = i -> ( ( j eSymPoly R ) ` k ) = ( ( i eSymPoly R ) ` k ) )
83 80 82 fveq12d 
 |-  ( j = i -> ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) = ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) )
84 83 fveq1d 
 |-  ( j = i -> ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) = ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) )
85 84 oveq2d 
 |-  ( j = i -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) )
86 79 85 eqeq12d 
 |-  ( j = i -> ( ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) )
87 74 86 raleqbidv 
 |-  ( j = i -> ( A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) )
88 72 87 raleqbidv 
 |-  ( j = i -> ( A. z e. ( B ^m j ) A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) )
89 oveq2 
 |-  ( j = ( i u. { m } ) -> ( B ^m j ) = ( B ^m ( i u. { m } ) ) )
90 fveq2 
 |-  ( j = ( i u. { m } ) -> ( # ` j ) = ( # ` ( i u. { m } ) ) )
91 90 oveq2d 
 |-  ( j = ( i u. { m } ) -> ( 0 ... ( # ` j ) ) = ( 0 ... ( # ` ( i u. { m } ) ) ) )
92 mpteq1 
 |-  ( j = ( i u. { m } ) -> ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) )
93 92 oveq2d 
 |-  ( j = ( i u. { m } ) -> ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) )
94 93 fveq2d 
 |-  ( j = ( i u. { m } ) -> ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) )
95 90 oveq1d 
 |-  ( j = ( i u. { m } ) -> ( ( # ` j ) - k ) = ( ( # ` ( i u. { m } ) ) - k ) )
96 94 95 fveq12d 
 |-  ( j = ( i u. { m } ) -> ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) )
97 oveq1 
 |-  ( j = ( i u. { m } ) -> ( j eval R ) = ( ( i u. { m } ) eval R ) )
98 oveq1 
 |-  ( j = ( i u. { m } ) -> ( j eSymPoly R ) = ( ( i u. { m } ) eSymPoly R ) )
99 98 fveq1d 
 |-  ( j = ( i u. { m } ) -> ( ( j eSymPoly R ) ` k ) = ( ( ( i u. { m } ) eSymPoly R ) ` k ) )
100 97 99 fveq12d 
 |-  ( j = ( i u. { m } ) -> ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) = ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) )
101 100 fveq1d 
 |-  ( j = ( i u. { m } ) -> ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) = ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) )
102 101 oveq2d 
 |-  ( j = ( i u. { m } ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) )
103 96 102 eqeq12d 
 |-  ( j = ( i u. { m } ) -> ( ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) ) )
104 91 103 raleqbidv 
 |-  ( j = ( i u. { m } ) -> ( A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) ) )
105 89 104 raleqbidv 
 |-  ( j = ( i u. { m } ) -> ( A. z e. ( B ^m j ) A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. z e. ( B ^m ( i u. { m } ) ) A. k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) ) )
106 oveq2 
 |-  ( j = I -> ( B ^m j ) = ( B ^m I ) )
107 fveq2 
 |-  ( j = I -> ( # ` j ) = ( # ` I ) )
108 107 13 eqtr4di 
 |-  ( j = I -> ( # ` j ) = H )
109 108 oveq2d 
 |-  ( j = I -> ( 0 ... ( # ` j ) ) = ( 0 ... H ) )
110 mpteq1 
 |-  ( j = I -> ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) )
111 110 oveq2d 
 |-  ( j = I -> ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) )
112 111 fveq2d 
 |-  ( j = I -> ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) )
113 108 oveq1d 
 |-  ( j = I -> ( ( # ` j ) - k ) = ( H - k ) )
114 112 113 fveq12d 
 |-  ( j = I -> ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( H - k ) ) )
115 oveq1 
 |-  ( j = I -> ( j eval R ) = ( I eval R ) )
116 115 5 eqtr4di 
 |-  ( j = I -> ( j eval R ) = Q )
117 oveq1 
 |-  ( j = I -> ( j eSymPoly R ) = ( I eSymPoly R ) )
118 117 6 eqtr4di 
 |-  ( j = I -> ( j eSymPoly R ) = E )
119 118 fveq1d 
 |-  ( j = I -> ( ( j eSymPoly R ) ` k ) = ( E ` k ) )
120 116 119 fveq12d 
 |-  ( j = I -> ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) = ( Q ` ( E ` k ) ) )
121 120 fveq1d 
 |-  ( j = I -> ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) = ( ( Q ` ( E ` k ) ) ` z ) )
122 121 oveq2d 
 |-  ( j = I -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` z ) ) )
123 114 122 eqeq12d 
 |-  ( j = I -> ( ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( H - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` z ) ) ) )
124 109 123 raleqbidv 
 |-  ( j = I -> ( A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. k e. ( 0 ... H ) ( ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( H - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` z ) ) ) )
125 106 124 raleqbidv 
 |-  ( j = I -> ( A. z e. ( B ^m j ) A. k e. ( 0 ... ( # ` j ) ) ( ( coe1 ` ( M gsum ( n e. j |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` j ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( j eval R ) ` ( ( j eSymPoly R ) ` k ) ) ` z ) ) <-> A. z e. ( B ^m I ) A. k e. ( 0 ... H ) ( ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( H - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` z ) ) ) )
126 15 idomringd 
 |-  ( ph -> R e. Ring )
127 2 8 126 ringidcld 
 |-  ( ph -> .1. e. B )
128 2 9 8 126 127 ringlidmd 
 |-  ( ph -> ( .1. .x. .1. ) = .1. )
129 126 ringgrpd 
 |-  ( ph -> R e. Grp )
130 2 7 129 127 grpinvcld 
 |-  ( ph -> ( N ` .1. ) e. B )
131 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
132 131 2 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
133 131 8 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
134 132 133 12 mulg0 
 |-  ( ( N ` .1. ) e. B -> ( 0 .^ ( N ` .1. ) ) = .1. )
135 130 134 syl 
 |-  ( ph -> ( 0 .^ ( N ` .1. ) ) = .1. )
136 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
137 136 8 zrh1 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 1 ) = .1. )
138 126 137 syl 
 |-  ( ph -> ( ( ZRHom ` R ) ` 1 ) = .1. )
139 138 sneqd 
 |-  ( ph -> { ( ( ZRHom ` R ) ` 1 ) } = { .1. } )
140 139 xpeq2d 
 |-  ( ph -> ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) = ( { (/) } X. { .1. } ) )
141 0ex 
 |-  (/) e. _V
142 141 a1i 
 |-  ( ph -> (/) e. _V )
143 8 fvexi 
 |-  .1. e. _V
144 143 a1i 
 |-  ( ph -> .1. e. _V )
145 xpsng 
 |-  ( ( (/) e. _V /\ .1. e. _V ) -> ( { (/) } X. { .1. } ) = { <. (/) , .1. >. } )
146 142 144 145 syl2anc 
 |-  ( ph -> ( { (/) } X. { .1. } ) = { <. (/) , .1. >. } )
147 0xp 
 |-  ( (/) X. { 0 } ) = (/)
148 147 eqcomi 
 |-  (/) = ( (/) X. { 0 } )
149 148 eqeq2i 
 |-  ( f = (/) <-> f = ( (/) X. { 0 } ) )
150 149 biimpi 
 |-  ( f = (/) -> f = ( (/) X. { 0 } ) )
151 150 adantl 
 |-  ( ( ph /\ f = (/) ) -> f = ( (/) X. { 0 } ) )
152 151 iftrued 
 |-  ( ( ph /\ f = (/) ) -> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) = .1. )
153 152 142 144 fmptsnd 
 |-  ( ph -> { <. (/) , .1. >. } = ( f e. { (/) } |-> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) ) )
154 140 146 153 3eqtrd 
 |-  ( ph -> ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) = ( f e. { (/) } |-> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) ) )
155 elsni 
 |-  ( h e. { (/) } -> h = (/) )
156 nn0ex 
 |-  NN0 e. _V
157 mapdm0 
 |-  ( NN0 e. _V -> ( NN0 ^m (/) ) = { (/) } )
158 156 157 ax-mp 
 |-  ( NN0 ^m (/) ) = { (/) }
159 155 158 eleq2s 
 |-  ( h e. ( NN0 ^m (/) ) -> h = (/) )
160 159 cnveqd 
 |-  ( h e. ( NN0 ^m (/) ) -> `' h = `' (/) )
161 160 imaeq1d 
 |-  ( h e. ( NN0 ^m (/) ) -> ( `' h " NN ) = ( `' (/) " NN ) )
162 cnv0 
 |-  `' (/) = (/)
163 162 imaeq1i 
 |-  ( `' (/) " NN ) = ( (/) " NN )
164 0ima 
 |-  ( (/) " NN ) = (/)
165 163 164 eqtri 
 |-  ( `' (/) " NN ) = (/)
166 161 165 eqtrdi 
 |-  ( h e. ( NN0 ^m (/) ) -> ( `' h " NN ) = (/) )
167 0fi 
 |-  (/) e. Fin
168 166 167 eqeltrdi 
 |-  ( h e. ( NN0 ^m (/) ) -> ( `' h " NN ) e. Fin )
169 168 rabeqc 
 |-  { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin } = ( NN0 ^m (/) )
170 169 158 eqtr2i 
 |-  { (/) } = { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin }
171 eqid 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } = { h e. ( NN0 ^m (/) ) | h finSupp 0 }
172 171 psrbasfsupp 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } = { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin }
173 170 172 eqtr4i 
 |-  { (/) } = { h e. ( NN0 ^m (/) ) | h finSupp 0 }
174 0nn0 
 |-  0 e. NN0
175 174 a1i 
 |-  ( ph -> 0 e. NN0 )
176 173 142 15 175 esplyfval 
 |-  ( ph -> ( ( (/) eSymPoly R ) ` 0 ) = ( ( ZRHom ` R ) o. ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) ) )
177 fveqeq2 
 |-  ( c = (/) -> ( ( # ` c ) = 0 <-> ( # ` (/) ) = 0 ) )
178 0elpw 
 |-  (/) e. ~P (/)
179 178 a1i 
 |-  ( ph -> (/) e. ~P (/) )
180 46 a1i 
 |-  ( ph -> ( # ` (/) ) = 0 )
181 hasheq0 
 |-  ( c e. ~P (/) -> ( ( # ` c ) = 0 <-> c = (/) ) )
182 181 biimpa 
 |-  ( ( c e. ~P (/) /\ ( # ` c ) = 0 ) -> c = (/) )
183 182 adantll 
 |-  ( ( ( ph /\ c e. ~P (/) ) /\ ( # ` c ) = 0 ) -> c = (/) )
184 177 179 180 183 rabeqsnd 
 |-  ( ph -> { c e. ~P (/) | ( # ` c ) = 0 } = { (/) } )
185 184 imaeq2d 
 |-  ( ph -> ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) = ( ( _Ind ` (/) ) " { (/) } ) )
186 pw0 
 |-  ~P (/) = { (/) }
187 186 a1i 
 |-  ( ph -> ~P (/) = { (/) } )
188 indf1o 
 |-  ( (/) e. _V -> ( _Ind ` (/) ) : ~P (/) -1-1-onto-> ( { 0 , 1 } ^m (/) ) )
189 f1of 
 |-  ( ( _Ind ` (/) ) : ~P (/) -1-1-onto-> ( { 0 , 1 } ^m (/) ) -> ( _Ind ` (/) ) : ~P (/) --> ( { 0 , 1 } ^m (/) ) )
190 142 188 189 3syl 
 |-  ( ph -> ( _Ind ` (/) ) : ~P (/) --> ( { 0 , 1 } ^m (/) ) )
191 187 190 feq2dd 
 |-  ( ph -> ( _Ind ` (/) ) : { (/) } --> ( { 0 , 1 } ^m (/) ) )
192 191 ffnd 
 |-  ( ph -> ( _Ind ` (/) ) Fn { (/) } )
193 141 snid 
 |-  (/) e. { (/) }
194 193 a1i 
 |-  ( ph -> (/) e. { (/) } )
195 192 194 fnimasnd 
 |-  ( ph -> ( ( _Ind ` (/) ) " { (/) } ) = { ( ( _Ind ` (/) ) ` (/) ) } )
196 ssidd 
 |-  ( ph -> (/) C_ (/) )
197 indf 
 |-  ( ( (/) e. _V /\ (/) C_ (/) ) -> ( ( _Ind ` (/) ) ` (/) ) : (/) --> { 0 , 1 } )
198 142 196 197 syl2anc 
 |-  ( ph -> ( ( _Ind ` (/) ) ` (/) ) : (/) --> { 0 , 1 } )
199 f0bi 
 |-  ( ( ( _Ind ` (/) ) ` (/) ) : (/) --> { 0 , 1 } <-> ( ( _Ind ` (/) ) ` (/) ) = (/) )
200 198 199 sylib 
 |-  ( ph -> ( ( _Ind ` (/) ) ` (/) ) = (/) )
201 200 sneqd 
 |-  ( ph -> { ( ( _Ind ` (/) ) ` (/) ) } = { (/) } )
202 185 195 201 3eqtrd 
 |-  ( ph -> ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) = { (/) } )
203 202 fveq2d 
 |-  ( ph -> ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) = ( ( _Ind ` { (/) } ) ` { (/) } ) )
204 p0ex 
 |-  { (/) } e. _V
205 indconst1 
 |-  ( { (/) } e. _V -> ( ( _Ind ` { (/) } ) ` { (/) } ) = ( { (/) } X. { 1 } ) )
206 204 205 ax-mp 
 |-  ( ( _Ind ` { (/) } ) ` { (/) } ) = ( { (/) } X. { 1 } )
207 203 206 eqtrdi 
 |-  ( ph -> ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) = ( { (/) } X. { 1 } ) )
208 207 coeq2d 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) ) = ( ( ZRHom ` R ) o. ( { (/) } X. { 1 } ) ) )
209 136 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
210 zringbas 
 |-  ZZ = ( Base ` ZZring )
211 210 2 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> B )
212 126 209 211 3syl 
 |-  ( ph -> ( ZRHom ` R ) : ZZ --> B )
213 212 ffnd 
 |-  ( ph -> ( ZRHom ` R ) Fn ZZ )
214 1zzd 
 |-  ( ph -> 1 e. ZZ )
215 fcoconst 
 |-  ( ( ( ZRHom ` R ) Fn ZZ /\ 1 e. ZZ ) -> ( ( ZRHom ` R ) o. ( { (/) } X. { 1 } ) ) = ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) )
216 213 214 215 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( { (/) } X. { 1 } ) ) = ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) )
217 176 208 216 3eqtrd 
 |-  ( ph -> ( ( (/) eSymPoly R ) ` 0 ) = ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) )
218 eqid 
 |-  ( (/) mPoly R ) = ( (/) mPoly R )
219 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
220 eqid 
 |-  ( algSc ` ( (/) mPoly R ) ) = ( algSc ` ( (/) mPoly R ) )
221 218 170 219 2 220 142 126 127 mplascl 
 |-  ( ph -> ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) = ( f e. { (/) } |-> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) ) )
222 154 217 221 3eqtr4d 
 |-  ( ph -> ( ( (/) eSymPoly R ) ` 0 ) = ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) )
223 222 fveq2d 
 |-  ( ph -> ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) = ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) )
224 223 fveq1d 
 |-  ( ph -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) = ( ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) ` (/) ) )
225 eqid 
 |-  ( (/) eval R ) = ( (/) eval R )
226 193 158 eleqtrri 
 |-  (/) e. ( NN0 ^m (/) )
227 226 a1i 
 |-  ( ph -> (/) e. ( NN0 ^m (/) ) )
228 15 idomcringd 
 |-  ( ph -> R e. CRing )
229 225 218 2 220 227 228 127 evlsca 
 |-  ( ph -> ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) = ( ( B ^m (/) ) X. { .1. } ) )
230 229 fveq1d 
 |-  ( ph -> ( ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) ` (/) ) = ( ( ( B ^m (/) ) X. { .1. } ) ` (/) ) )
231 193 42 eleqtrri 
 |-  (/) e. ( B ^m (/) )
232 143 fvconst2 
 |-  ( (/) e. ( B ^m (/) ) -> ( ( ( B ^m (/) ) X. { .1. } ) ` (/) ) = .1. )
233 231 232 mp1i 
 |-  ( ph -> ( ( ( B ^m (/) ) X. { .1. } ) ` (/) ) = .1. )
234 224 230 233 3eqtrd 
 |-  ( ph -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) = .1. )
235 135 234 oveq12d 
 |-  ( ph -> ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) = ( .1. .x. .1. ) )
236 iftrue 
 |-  ( l = 0 -> if ( l = 0 , .1. , ( 0g ` R ) ) = .1. )
237 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
238 4 237 ringidval 
 |-  ( 1r ` W ) = ( 0g ` M )
239 238 eqcomi 
 |-  ( 0g ` M ) = ( 1r ` W )
240 1 239 219 8 coe1id 
 |-  ( R e. Ring -> ( coe1 ` ( 0g ` M ) ) = ( l e. NN0 |-> if ( l = 0 , .1. , ( 0g ` R ) ) ) )
241 126 240 syl 
 |-  ( ph -> ( coe1 ` ( 0g ` M ) ) = ( l e. NN0 |-> if ( l = 0 , .1. , ( 0g ` R ) ) ) )
242 236 241 175 144 fvmptd4 
 |-  ( ph -> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = .1. )
243 128 235 242 3eqtr4rd 
 |-  ( ph -> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) )
244 fveq2 
 |-  ( z = (/) -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) = ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) )
245 244 oveq2d 
 |-  ( z = (/) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) )
246 245 eqeq2d 
 |-  ( z = (/) -> ( ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) ) )
247 246 ralbidv 
 |-  ( z = (/) -> ( A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) <-> A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) ) )
248 c0ex 
 |-  0 e. _V
249 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
250 0m0e0 
 |-  ( 0 - 0 ) = 0
251 249 250 eqtrdi 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
252 251 fveq2d 
 |-  ( k = 0 -> ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( coe1 ` ( 0g ` M ) ) ` 0 ) )
253 oveq1 
 |-  ( k = 0 -> ( k .^ ( N ` .1. ) ) = ( 0 .^ ( N ` .1. ) ) )
254 2fveq3 
 |-  ( k = 0 -> ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) = ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) )
255 254 fveq1d 
 |-  ( k = 0 -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) = ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) )
256 253 255 oveq12d 
 |-  ( k = 0 -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) )
257 252 256 eqeq12d 
 |-  ( k = 0 -> ( ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) <-> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) ) )
258 248 257 ralsn 
 |-  ( A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) <-> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) )
259 247 258 bitrdi 
 |-  ( z = (/) -> ( A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) ) )
260 141 259 ralsn 
 |-  ( A. z e. { (/) } A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) )
261 243 260 sylibr 
 |-  ( ph -> A. z e. { (/) } A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) )
262 nfv 
 |-  F/ z ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) )
263 nfra1 
 |-  F/ z A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) )
264 262 263 nfan 
 |-  F/ z ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) )
265 nfv 
 |-  F/ k ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) )
266 nfra2w 
 |-  F/ k A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) )
267 265 266 nfan 
 |-  F/ k ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) )
268 nfv 
 |-  F/ k z e. ( B ^m ( i u. { m } ) )
269 267 268 nfan 
 |-  F/ k ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) )
270 eqid 
 |-  ( ( i u. { m } ) eval R ) = ( ( i u. { m } ) eval R )
271 eqid 
 |-  ( ( i u. { m } ) eSymPoly R ) = ( ( i u. { m } ) eSymPoly R )
272 eqid 
 |-  ( # ` ( i u. { m } ) ) = ( # ` ( i u. { m } ) )
273 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> I e. Fin )
274 simp-5r 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> i C_ I )
275 273 274 ssfid 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> i e. Fin )
276 snfi 
 |-  { m } e. Fin
277 276 a1i 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> { m } e. Fin )
278 275 277 unfid 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( i u. { m } ) e. Fin )
279 15 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> R e. IDomn )
280 40 a1i 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> B e. _V )
281 simplr 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> z e. ( B ^m ( i u. { m } ) ) )
282 278 280 281 elmaprd 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> z : ( i u. { m } ) --> B )
283 2fveq3 
 |-  ( n = o -> ( A ` ( z ` n ) ) = ( A ` ( z ` o ) ) )
284 283 oveq2d 
 |-  ( n = o -> ( X .- ( A ` ( z ` n ) ) ) = ( X .- ( A ` ( z ` o ) ) ) )
285 284 cbvmptv 
 |-  ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( o e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` o ) ) ) )
286 285 oveq2i 
 |-  ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( o e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` o ) ) ) ) )
287 fznn0sub2 
 |-  ( k e. ( 0 ... ( # ` ( i u. { m } ) ) ) -> ( ( # ` ( i u. { m } ) ) - k ) e. ( 0 ... ( # ` ( i u. { m } ) ) ) )
288 287 adantl 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( # ` ( i u. { m } ) ) - k ) e. ( 0 ... ( # ` ( i u. { m } ) ) ) )
289 ssun2 
 |-  { m } C_ ( i u. { m } )
290 vsnid 
 |-  m e. { m }
291 289 290 sselii 
 |-  m e. ( i u. { m } )
292 291 a1i 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> m e. ( i u. { m } ) )
293 eqid 
 |-  ( ( i u. { m } ) \ { m } ) = ( ( i u. { m } ) \ { m } )
294 fveq1 
 |-  ( z = y -> ( z ` n ) = ( y ` n ) )
295 294 fveq2d 
 |-  ( z = y -> ( A ` ( z ` n ) ) = ( A ` ( y ` n ) ) )
296 295 oveq2d 
 |-  ( z = y -> ( X .- ( A ` ( z ` n ) ) ) = ( X .- ( A ` ( y ` n ) ) ) )
297 296 mpteq2dv 
 |-  ( z = y -> ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) )
298 297 oveq2d 
 |-  ( z = y -> ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) )
299 298 fveq2d 
 |-  ( z = y -> ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) )
300 299 fveq1d 
 |-  ( z = y -> ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) )
301 fveq2 
 |-  ( z = y -> ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) = ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) )
302 301 oveq2d 
 |-  ( z = y -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) )
303 300 302 eqeq12d 
 |-  ( z = y -> ( ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) <-> ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) ) )
304 303 ralbidv 
 |-  ( z = y -> ( A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) <-> A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) ) )
305 304 cbvralvw 
 |-  ( A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) <-> A. y e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) )
306 simpr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> m e. ( I \ i ) )
307 306 eldifbd 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> -. m e. i )
308 disjsn 
 |-  ( ( i i^i { m } ) = (/) <-> -. m e. i )
309 307 308 sylibr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i i^i { m } ) = (/) )
310 undif5 
 |-  ( ( i i^i { m } ) = (/) -> ( ( i u. { m } ) \ { m } ) = i )
311 309 310 syl 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( i u. { m } ) \ { m } ) = i )
312 311 eqcomd 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> i = ( ( i u. { m } ) \ { m } ) )
313 312 oveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( B ^m i ) = ( B ^m ( ( i u. { m } ) \ { m } ) ) )
314 oveq2 
 |-  ( k = l -> ( ( # ` i ) - k ) = ( ( # ` i ) - l ) )
315 314 fveq2d 
 |-  ( k = l -> ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - l ) ) )
316 oveq1 
 |-  ( k = l -> ( k .^ ( N ` .1. ) ) = ( l .^ ( N ` .1. ) ) )
317 2fveq3 
 |-  ( k = l -> ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) = ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) )
318 317 fveq1d 
 |-  ( k = l -> ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) = ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) )
319 316 318 oveq12d 
 |-  ( k = l -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) ) )
320 315 319 eqeq12d 
 |-  ( k = l -> ( ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) <-> ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) ) ) )
321 320 cbvralvw 
 |-  ( A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) <-> A. l e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) ) )
322 312 fveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( # ` i ) = ( # ` ( ( i u. { m } ) \ { m } ) ) )
323 322 oveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( 0 ... ( # ` i ) ) = ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) )
324 2fveq3 
 |-  ( n = o -> ( A ` ( y ` n ) ) = ( A ` ( y ` o ) ) )
325 324 oveq2d 
 |-  ( n = o -> ( X .- ( A ` ( y ` n ) ) ) = ( X .- ( A ` ( y ` o ) ) ) )
326 325 cbvmptv 
 |-  ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) = ( o e. i |-> ( X .- ( A ` ( y ` o ) ) ) )
327 312 mpteq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( o e. i |-> ( X .- ( A ` ( y ` o ) ) ) ) = ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) )
328 326 327 eqtrid 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) = ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) )
329 328 oveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) = ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) )
330 329 fveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) )
331 322 oveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( # ` i ) - l ) = ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) )
332 330 331 fveq12d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - l ) ) = ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) )
333 312 oveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i eval R ) = ( ( ( i u. { m } ) \ { m } ) eval R ) )
334 312 oveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i eSymPoly R ) = ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) )
335 334 fveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( i eSymPoly R ) ` l ) = ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) )
336 333 335 fveq12d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) = ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) )
337 336 fveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) = ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) )
338 337 oveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( l .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) )
339 332 338 eqeq12d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) ) <-> ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) ) )
340 323 339 raleqbidv 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( A. l e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) ) <-> A. l e. ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) ) )
341 321 340 bitrid 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) <-> A. l e. ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) ) )
342 313 341 raleqbidv 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( A. y e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) ) <-> A. y e. ( B ^m ( ( i u. { m } ) \ { m } ) ) A. l e. ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) ) )
343 305 342 bitrid 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) <-> A. y e. ( B ^m ( ( i u. { m } ) \ { m } ) ) A. l e. ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) ) )
344 343 biimpa 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) -> A. y e. ( B ^m ( ( i u. { m } ) \ { m } ) ) A. l e. ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) )
345 344 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> A. y e. ( B ^m ( ( i u. { m } ) \ { m } ) ) A. l e. ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) ( ( coe1 ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( y ` o ) ) ) ) ) ) ` ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( ( ( ( i u. { m } ) \ { m } ) eval R ) ` ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) ) ` y ) ) )
346 eqid 
 |-  ( ( ( i u. { m } ) \ { m } ) eval R ) = ( ( ( i u. { m } ) \ { m } ) eval R )
347 eqid 
 |-  ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) = ( ( ( i u. { m } ) \ { m } ) eSymPoly R )
348 eqid 
 |-  ( # ` ( ( i u. { m } ) \ { m } ) ) = ( # ` ( ( i u. { m } ) \ { m } ) )
349 difssd 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( i u. { m } ) \ { m } ) C_ ( i u. { m } ) )
350 278 349 ssfid 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( i u. { m } ) \ { m } ) e. Fin )
351 282 349 fssresd 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( z |` ( ( i u. { m } ) \ { m } ) ) : ( ( i u. { m } ) \ { m } ) --> B )
352 eqid 
 |-  ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( ( z |` ( ( i u. { m } ) \ { m } ) ) ` o ) ) ) ) ) = ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( ( z |` ( ( i u. { m } ) \ { m } ) ) ` o ) ) ) ) )
353 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
354 1 2 3 4 346 347 7 8 9 10 11 12 348 350 279 351 352 353 vietadeg1 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( deg1 ` R ) ` ( M gsum ( o e. ( ( i u. { m } ) \ { m } ) |-> ( X .- ( A ` ( ( z |` ( ( i u. { m } ) \ { m } ) ) ` o ) ) ) ) ) ) = ( # ` ( ( i u. { m } ) \ { m } ) ) )
355 1 2 3 4 270 271 7 8 9 10 11 12 272 278 279 282 286 288 292 293 345 354 vietalem 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) ) ) ` z ) ) )
356 14 ad2antrr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> I e. Fin )
357 simplr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> i C_ I )
358 356 357 ssfid 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> i e. Fin )
359 276 a1i 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> { m } e. Fin )
360 358 359 unfid 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i u. { m } ) e. Fin )
361 360 adantr 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( i u. { m } ) e. Fin )
362 hashcl 
 |-  ( ( i u. { m } ) e. Fin -> ( # ` ( i u. { m } ) ) e. NN0 )
363 361 362 syl 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( # ` ( i u. { m } ) ) e. NN0 )
364 363 nn0cnd 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( # ` ( i u. { m } ) ) e. CC )
365 elfznn0 
 |-  ( k e. ( 0 ... ( # ` ( i u. { m } ) ) ) -> k e. NN0 )
366 365 adantl 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> k e. NN0 )
367 366 nn0cnd 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> k e. CC )
368 364 367 nncand 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) = k )
369 368 oveq1d 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) .^ ( N ` .1. ) ) = ( k .^ ( N ` .1. ) ) )
370 368 fveq2d 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( ( i u. { m } ) eSymPoly R ) ` ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) ) = ( ( ( i u. { m } ) eSymPoly R ) ` k ) )
371 370 fveq2d 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) ) ) = ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) )
372 371 fveq1d 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) ) ) ` z ) = ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) )
373 369 372 oveq12d 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) )
374 373 ad4ant14 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) )
375 355 374 eqtrd 
 |-  ( ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) )
376 269 375 ralrimia 
 |-  ( ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) /\ z e. ( B ^m ( i u. { m } ) ) ) -> A. k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) )
377 264 376 ralrimia 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) ) -> A. z e. ( B ^m ( i u. { m } ) ) A. k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) )
378 377 ex 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) -> A. z e. ( B ^m ( i u. { m } ) ) A. k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) ) )
379 378 anasss 
 |-  ( ( ph /\ ( i C_ I /\ m e. ( I \ i ) ) ) -> ( A. z e. ( B ^m i ) A. k e. ( 0 ... ( # ` i ) ) ( ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` i ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) ) -> A. z e. ( B ^m ( i u. { m } ) ) A. k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ( ( coe1 ` ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` ( i u. { m } ) ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( i u. { m } ) eval R ) ` ( ( ( i u. { m } ) eSymPoly R ) ` k ) ) ` z ) ) ) )
380 71 88 105 125 261 379 14 findcard2d 
 |-  ( ph -> A. z e. ( B ^m I ) A. k e. ( 0 ... H ) ( ( coe1 ` ( M gsum ( n e. I |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( H - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` z ) ) )
381 40 a1i 
 |-  ( ph -> B e. _V )
382 381 14 16 elmapdd 
 |-  ( ph -> Z e. ( B ^m I ) )
383 31 38 380 382 18 rspc2dv 
 |-  ( ph -> ( C ` ( H - K ) ) = ( ( K .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` K ) ) ` Z ) ) )