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

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 bilani 
 |-  ( ( ph /\ f = (/) ) -> f = ( (/) X. { 0 } ) )
151 150 iftrued 
 |-  ( ( ph /\ f = (/) ) -> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) = .1. )
152 151 142 144 fmptsnd 
 |-  ( ph -> { <. (/) , .1. >. } = ( f e. { (/) } |-> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) ) )
153 140 146 152 3eqtrd 
 |-  ( ph -> ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) = ( f e. { (/) } |-> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) ) )
154 elsni 
 |-  ( h e. { (/) } -> h = (/) )
155 nn0ex 
 |-  NN0 e. _V
156 mapdm0 
 |-  ( NN0 e. _V -> ( NN0 ^m (/) ) = { (/) } )
157 155 156 ax-mp 
 |-  ( NN0 ^m (/) ) = { (/) }
158 154 157 eleq2s 
 |-  ( h e. ( NN0 ^m (/) ) -> h = (/) )
159 158 cnveqd 
 |-  ( h e. ( NN0 ^m (/) ) -> `' h = `' (/) )
160 159 imaeq1d 
 |-  ( h e. ( NN0 ^m (/) ) -> ( `' h " NN ) = ( `' (/) " NN ) )
161 cnv0 
 |-  `' (/) = (/)
162 161 imaeq1i 
 |-  ( `' (/) " NN ) = ( (/) " NN )
163 0ima 
 |-  ( (/) " NN ) = (/)
164 162 163 eqtri 
 |-  ( `' (/) " NN ) = (/)
165 160 164 eqtrdi 
 |-  ( h e. ( NN0 ^m (/) ) -> ( `' h " NN ) = (/) )
166 0fi 
 |-  (/) e. Fin
167 165 166 eqeltrdi 
 |-  ( h e. ( NN0 ^m (/) ) -> ( `' h " NN ) e. Fin )
168 167 rabeqc 
 |-  { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin } = ( NN0 ^m (/) )
169 168 157 eqtr2i 
 |-  { (/) } = { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin }
170 eqid 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } = { h e. ( NN0 ^m (/) ) | h finSupp 0 }
171 170 psrbasfsupp 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } = { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin }
172 169 171 eqtr4i 
 |-  { (/) } = { h e. ( NN0 ^m (/) ) | h finSupp 0 }
173 0nn0 
 |-  0 e. NN0
174 173 a1i 
 |-  ( ph -> 0 e. NN0 )
175 172 142 15 174 esplyfval 
 |-  ( ph -> ( ( (/) eSymPoly R ) ` 0 ) = ( ( ZRHom ` R ) o. ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) ) )
176 fveqeq2 
 |-  ( c = (/) -> ( ( # ` c ) = 0 <-> ( # ` (/) ) = 0 ) )
177 0elpw 
 |-  (/) e. ~P (/)
178 177 a1i 
 |-  ( ph -> (/) e. ~P (/) )
179 46 a1i 
 |-  ( ph -> ( # ` (/) ) = 0 )
180 hasheq0 
 |-  ( c e. ~P (/) -> ( ( # ` c ) = 0 <-> c = (/) ) )
181 180 biimpa 
 |-  ( ( c e. ~P (/) /\ ( # ` c ) = 0 ) -> c = (/) )
182 181 adantll 
 |-  ( ( ( ph /\ c e. ~P (/) ) /\ ( # ` c ) = 0 ) -> c = (/) )
183 176 178 179 182 rabeqsnd 
 |-  ( ph -> { c e. ~P (/) | ( # ` c ) = 0 } = { (/) } )
184 183 imaeq2d 
 |-  ( ph -> ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) = ( ( _Ind ` (/) ) " { (/) } ) )
185 pw0 
 |-  ~P (/) = { (/) }
186 185 a1i 
 |-  ( ph -> ~P (/) = { (/) } )
187 indf1o 
 |-  ( (/) e. _V -> ( _Ind ` (/) ) : ~P (/) -1-1-onto-> ( { 0 , 1 } ^m (/) ) )
188 f1of 
 |-  ( ( _Ind ` (/) ) : ~P (/) -1-1-onto-> ( { 0 , 1 } ^m (/) ) -> ( _Ind ` (/) ) : ~P (/) --> ( { 0 , 1 } ^m (/) ) )
189 142 187 188 3syl 
 |-  ( ph -> ( _Ind ` (/) ) : ~P (/) --> ( { 0 , 1 } ^m (/) ) )
190 186 189 feq2dd 
 |-  ( ph -> ( _Ind ` (/) ) : { (/) } --> ( { 0 , 1 } ^m (/) ) )
191 190 ffnd 
 |-  ( ph -> ( _Ind ` (/) ) Fn { (/) } )
192 141 snid 
 |-  (/) e. { (/) }
193 192 a1i 
 |-  ( ph -> (/) e. { (/) } )
194 191 193 fnimasnd 
 |-  ( ph -> ( ( _Ind ` (/) ) " { (/) } ) = { ( ( _Ind ` (/) ) ` (/) ) } )
195 ssidd 
 |-  ( ph -> (/) C_ (/) )
196 indf 
 |-  ( ( (/) e. _V /\ (/) C_ (/) ) -> ( ( _Ind ` (/) ) ` (/) ) : (/) --> { 0 , 1 } )
197 142 195 196 syl2anc 
 |-  ( ph -> ( ( _Ind ` (/) ) ` (/) ) : (/) --> { 0 , 1 } )
198 f0bi 
 |-  ( ( ( _Ind ` (/) ) ` (/) ) : (/) --> { 0 , 1 } <-> ( ( _Ind ` (/) ) ` (/) ) = (/) )
199 197 198 sylib 
 |-  ( ph -> ( ( _Ind ` (/) ) ` (/) ) = (/) )
200 199 sneqd 
 |-  ( ph -> { ( ( _Ind ` (/) ) ` (/) ) } = { (/) } )
201 184 194 200 3eqtrd 
 |-  ( ph -> ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) = { (/) } )
202 201 fveq2d 
 |-  ( ph -> ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) = ( ( _Ind ` { (/) } ) ` { (/) } ) )
203 p0ex 
 |-  { (/) } e. _V
204 indconst1 
 |-  ( { (/) } e. _V -> ( ( _Ind ` { (/) } ) ` { (/) } ) = ( { (/) } X. { 1 } ) )
205 203 204 ax-mp 
 |-  ( ( _Ind ` { (/) } ) ` { (/) } ) = ( { (/) } X. { 1 } )
206 202 205 eqtrdi 
 |-  ( ph -> ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) = ( { (/) } X. { 1 } ) )
207 206 coeq2d 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( ( _Ind ` { (/) } ) ` ( ( _Ind ` (/) ) " { c e. ~P (/) | ( # ` c ) = 0 } ) ) ) = ( ( ZRHom ` R ) o. ( { (/) } X. { 1 } ) ) )
208 136 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
209 zringbas 
 |-  ZZ = ( Base ` ZZring )
210 209 2 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> B )
211 126 208 210 3syl 
 |-  ( ph -> ( ZRHom ` R ) : ZZ --> B )
212 211 ffnd 
 |-  ( ph -> ( ZRHom ` R ) Fn ZZ )
213 1zzd 
 |-  ( ph -> 1 e. ZZ )
214 fcoconst 
 |-  ( ( ( ZRHom ` R ) Fn ZZ /\ 1 e. ZZ ) -> ( ( ZRHom ` R ) o. ( { (/) } X. { 1 } ) ) = ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) )
215 212 213 214 syl2anc 
 |-  ( ph -> ( ( ZRHom ` R ) o. ( { (/) } X. { 1 } ) ) = ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) )
216 175 207 215 3eqtrd 
 |-  ( ph -> ( ( (/) eSymPoly R ) ` 0 ) = ( { (/) } X. { ( ( ZRHom ` R ) ` 1 ) } ) )
217 eqid 
 |-  ( (/) mPoly R ) = ( (/) mPoly R )
218 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
219 eqid 
 |-  ( algSc ` ( (/) mPoly R ) ) = ( algSc ` ( (/) mPoly R ) )
220 217 169 218 2 219 142 126 127 mplascl 
 |-  ( ph -> ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) = ( f e. { (/) } |-> if ( f = ( (/) X. { 0 } ) , .1. , ( 0g ` R ) ) ) )
221 153 216 220 3eqtr4d 
 |-  ( ph -> ( ( (/) eSymPoly R ) ` 0 ) = ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) )
222 221 fveq2d 
 |-  ( ph -> ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) = ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) )
223 222 fveq1d 
 |-  ( ph -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) = ( ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) ` (/) ) )
224 eqid 
 |-  ( (/) eval R ) = ( (/) eval R )
225 192 157 eleqtrri 
 |-  (/) e. ( NN0 ^m (/) )
226 225 a1i 
 |-  ( ph -> (/) e. ( NN0 ^m (/) ) )
227 15 idomcringd 
 |-  ( ph -> R e. CRing )
228 224 217 2 219 226 227 127 evlsca 
 |-  ( ph -> ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) = ( ( B ^m (/) ) X. { .1. } ) )
229 228 fveq1d 
 |-  ( ph -> ( ( ( (/) eval R ) ` ( ( algSc ` ( (/) mPoly R ) ) ` .1. ) ) ` (/) ) = ( ( ( B ^m (/) ) X. { .1. } ) ` (/) ) )
230 192 42 eleqtrri 
 |-  (/) e. ( B ^m (/) )
231 143 fvconst2 
 |-  ( (/) e. ( B ^m (/) ) -> ( ( ( B ^m (/) ) X. { .1. } ) ` (/) ) = .1. )
232 230 231 mp1i 
 |-  ( ph -> ( ( ( B ^m (/) ) X. { .1. } ) ` (/) ) = .1. )
233 223 229 232 3eqtrd 
 |-  ( ph -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) = .1. )
234 135 233 oveq12d 
 |-  ( ph -> ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) = ( .1. .x. .1. ) )
235 iftrue 
 |-  ( l = 0 -> if ( l = 0 , .1. , ( 0g ` R ) ) = .1. )
236 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
237 4 236 ringidval 
 |-  ( 1r ` W ) = ( 0g ` M )
238 237 eqcomi 
 |-  ( 0g ` M ) = ( 1r ` W )
239 1 238 218 8 coe1id 
 |-  ( R e. Ring -> ( coe1 ` ( 0g ` M ) ) = ( l e. NN0 |-> if ( l = 0 , .1. , ( 0g ` R ) ) ) )
240 126 239 syl 
 |-  ( ph -> ( coe1 ` ( 0g ` M ) ) = ( l e. NN0 |-> if ( l = 0 , .1. , ( 0g ` R ) ) ) )
241 235 240 174 144 fvmptd4 
 |-  ( ph -> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = .1. )
242 128 234 241 3eqtr4rd 
 |-  ( ph -> ( ( coe1 ` ( 0g ` M ) ) ` 0 ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) )
243 fveq2 
 |-  ( z = (/) -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) = ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) )
244 243 oveq2d 
 |-  ( z = (/) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) )
245 244 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 ) ) ` (/) ) ) ) )
246 245 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 ) ) ` (/) ) ) ) )
247 c0ex 
 |-  0 e. _V
248 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
249 0m0e0 
 |-  ( 0 - 0 ) = 0
250 248 249 eqtrdi 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
251 250 fveq2d 
 |-  ( k = 0 -> ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( coe1 ` ( 0g ` M ) ) ` 0 ) )
252 oveq1 
 |-  ( k = 0 -> ( k .^ ( N ` .1. ) ) = ( 0 .^ ( N ` .1. ) ) )
253 2fveq3 
 |-  ( k = 0 -> ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) = ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) )
254 253 fveq1d 
 |-  ( k = 0 -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) = ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) )
255 252 254 oveq12d 
 |-  ( k = 0 -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` (/) ) ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) ) )
256 251 255 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 ) ) ` (/) ) ) ) )
257 247 256 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 ) ) ` (/) ) ) )
258 246 257 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 ) ) ` (/) ) ) ) )
259 141 258 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 ) ) ` (/) ) ) )
260 242 259 sylibr 
 |-  ( ph -> A. z e. { (/) } A. k e. { 0 } ( ( coe1 ` ( 0g ` M ) ) ` ( 0 - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` k ) ) ` z ) ) )
261 nfv 
 |-  F/ z ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) )
262 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 ) )
263 261 262 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 ) ) )
264 nfv 
 |-  F/ k ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) )
265 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 ) )
266 264 265 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 ) ) )
267 nfv 
 |-  F/ k z e. ( B ^m ( i u. { m } ) )
268 266 267 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 } ) ) )
269 eqid 
 |-  ( ( i u. { m } ) eval R ) = ( ( i u. { m } ) eval R )
270 eqid 
 |-  ( ( i u. { m } ) eSymPoly R ) = ( ( i u. { m } ) eSymPoly R )
271 eqid 
 |-  ( # ` ( i u. { m } ) ) = ( # ` ( i u. { m } ) )
272 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 )
273 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 )
274 272 273 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 )
275 snfi 
 |-  { m } e. Fin
276 275 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 )
277 274 276 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 )
278 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 )
279 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 )
280 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 } ) ) )
281 277 279 280 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 )
282 2fveq3 
 |-  ( n = o -> ( A ` ( z ` n ) ) = ( A ` ( z ` o ) ) )
283 282 oveq2d 
 |-  ( n = o -> ( X .- ( A ` ( z ` n ) ) ) = ( X .- ( A ` ( z ` o ) ) ) )
284 283 cbvmptv 
 |-  ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( o e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` o ) ) ) )
285 284 oveq2i 
 |-  ( M gsum ( n e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( o e. ( i u. { m } ) |-> ( X .- ( A ` ( z ` o ) ) ) ) )
286 fznn0sub2 
 |-  ( k e. ( 0 ... ( # ` ( i u. { m } ) ) ) -> ( ( # ` ( i u. { m } ) ) - k ) e. ( 0 ... ( # ` ( i u. { m } ) ) ) )
287 286 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 } ) ) ) )
288 ssun2 
 |-  { m } C_ ( i u. { m } )
289 vsnid 
 |-  m e. { m }
290 288 289 sselii 
 |-  m e. ( i u. { m } )
291 290 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 } ) )
292 eqid 
 |-  ( ( i u. { m } ) \ { m } ) = ( ( i u. { m } ) \ { m } )
293 fveq1 
 |-  ( z = y -> ( z ` n ) = ( y ` n ) )
294 293 fveq2d 
 |-  ( z = y -> ( A ` ( z ` n ) ) = ( A ` ( y ` n ) ) )
295 294 oveq2d 
 |-  ( z = y -> ( X .- ( A ` ( z ` n ) ) ) = ( X .- ( A ` ( y ` n ) ) ) )
296 295 mpteq2dv 
 |-  ( z = y -> ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) )
297 296 oveq2d 
 |-  ( z = y -> ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) )
298 297 fveq2d 
 |-  ( z = y -> ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) ) ) )
299 298 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 ) ) )
300 fveq2 
 |-  ( z = y -> ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` z ) = ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) )
301 300 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 ) ) )
302 299 301 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 ) ) ) )
303 302 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 ) ) ) )
304 303 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 ) ) )
305 simpr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> m e. ( I \ i ) )
306 305 eldifbd 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> -. m e. i )
307 disjsn 
 |-  ( ( i i^i { m } ) = (/) <-> -. m e. i )
308 306 307 sylibr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i i^i { m } ) = (/) )
309 undif5 
 |-  ( ( i i^i { m } ) = (/) -> ( ( i u. { m } ) \ { m } ) = i )
310 308 309 syl 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( i u. { m } ) \ { m } ) = i )
311 310 eqcomd 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> i = ( ( i u. { m } ) \ { m } ) )
312 311 oveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( B ^m i ) = ( B ^m ( ( i u. { m } ) \ { m } ) ) )
313 oveq2 
 |-  ( k = l -> ( ( # ` i ) - k ) = ( ( # ` i ) - l ) )
314 313 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 ) ) )
315 oveq1 
 |-  ( k = l -> ( k .^ ( N ` .1. ) ) = ( l .^ ( N ` .1. ) ) )
316 2fveq3 
 |-  ( k = l -> ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) = ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) )
317 316 fveq1d 
 |-  ( k = l -> ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` k ) ) ` y ) = ( ( ( i eval R ) ` ( ( i eSymPoly R ) ` l ) ) ` y ) )
318 315 317 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 ) ) )
319 314 318 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 ) ) ) )
320 319 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 ) ) )
321 311 fveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( # ` i ) = ( # ` ( ( i u. { m } ) \ { m } ) ) )
322 321 oveq2d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( 0 ... ( # ` i ) ) = ( 0 ... ( # ` ( ( i u. { m } ) \ { m } ) ) ) )
323 2fveq3 
 |-  ( n = o -> ( A ` ( y ` n ) ) = ( A ` ( y ` o ) ) )
324 323 oveq2d 
 |-  ( n = o -> ( X .- ( A ` ( y ` n ) ) ) = ( X .- ( A ` ( y ` o ) ) ) )
325 324 cbvmptv 
 |-  ( n e. i |-> ( X .- ( A ` ( y ` n ) ) ) ) = ( o e. i |-> ( X .- ( A ` ( y ` o ) ) ) )
326 311 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 ) ) ) ) )
327 325 326 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 ) ) ) ) )
328 327 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 ) ) ) ) ) )
329 328 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 ) ) ) ) ) ) )
330 321 oveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( # ` i ) - l ) = ( ( # ` ( ( i u. { m } ) \ { m } ) ) - l ) )
331 329 330 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 ) ) )
332 311 oveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i eval R ) = ( ( ( i u. { m } ) \ { m } ) eval R ) )
333 311 oveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i eSymPoly R ) = ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) )
334 333 fveq1d 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( ( i eSymPoly R ) ` l ) = ( ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) ` l ) )
335 332 334 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 ) ) )
336 335 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 ) )
337 336 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 ) ) )
338 331 337 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 ) ) ) )
339 322 338 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 ) ) ) )
340 320 339 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 ) ) ) )
341 312 340 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 ) ) ) )
342 304 341 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 ) ) ) )
343 342 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 ) ) )
344 343 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 ) ) )
345 eqid 
 |-  ( ( ( i u. { m } ) \ { m } ) eval R ) = ( ( ( i u. { m } ) \ { m } ) eval R )
346 eqid 
 |-  ( ( ( i u. { m } ) \ { m } ) eSymPoly R ) = ( ( ( i u. { m } ) \ { m } ) eSymPoly R )
347 eqid 
 |-  ( # ` ( ( i u. { m } ) \ { m } ) ) = ( # ` ( ( i u. { m } ) \ { m } ) )
348 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 } ) )
349 277 348 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 )
350 281 348 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 )
351 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 ) ) ) ) )
352 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
353 1 2 3 4 345 346 7 8 9 10 11 12 347 349 278 350 351 352 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 } ) ) )
354 1 2 3 4 269 270 7 8 9 10 11 12 271 277 278 281 285 287 291 292 344 353 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 ) ) )
355 14 ad2antrr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> I e. Fin )
356 simplr 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> i C_ I )
357 355 356 ssfid 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> i e. Fin )
358 275 a1i 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> { m } e. Fin )
359 357 358 unfid 
 |-  ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) -> ( i u. { m } ) e. Fin )
360 359 adantr 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( i u. { m } ) e. Fin )
361 hashcl 
 |-  ( ( i u. { m } ) e. Fin -> ( # ` ( i u. { m } ) ) e. NN0 )
362 360 361 syl 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( # ` ( i u. { m } ) ) e. NN0 )
363 362 nn0cnd 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( # ` ( i u. { m } ) ) e. CC )
364 elfznn0 
 |-  ( k e. ( 0 ... ( # ` ( i u. { m } ) ) ) -> k e. NN0 )
365 364 adantl 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> k e. NN0 )
366 365 nn0cnd 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> k e. CC )
367 363 366 nncand 
 |-  ( ( ( ( ph /\ i C_ I ) /\ m e. ( I \ i ) ) /\ k e. ( 0 ... ( # ` ( i u. { m } ) ) ) ) -> ( ( # ` ( i u. { m } ) ) - ( ( # ` ( i u. { m } ) ) - k ) ) = k )
368 367 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. ) ) )
369 367 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 ) )
370 369 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 ) ) )
371 370 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 ) )
372 368 371 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 ) ) )
373 372 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 ) ) )
374 354 373 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 ) ) )
375 268 374 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 ) ) )
376 263 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 ) ) ) -> 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 ) ) )
377 376 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 ) ) ) )
378 377 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 ) ) ) )
379 71 88 105 125 260 378 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 ) ) )
380 40 a1i 
 |-  ( ph -> B e. _V )
381 380 14 16 elmapdd 
 |-  ( ph -> Z e. ( B ^m I ) )
382 31 38 379 381 18 rspc2dv 
 |-  ( ph -> ( C ` ( H - K ) ) = ( ( K .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` K ) ) ` Z ) ) )