| 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 |
|
vietalem.y |
|- ( ph -> Y e. I ) |
| 20 |
|
vietalem.j |
|- J = ( I \ { Y } ) |
| 21 |
|
vietalem.2 |
|- ( ph -> 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 ) ) ) |
| 22 |
|
vietalem.3 |
|- ( ph -> ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) = ( # ` J ) ) |
| 23 |
17
|
a1i |
|- ( ph -> F = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ) |
| 24 |
20
|
uneq1i |
|- ( J u. { Y } ) = ( ( I \ { Y } ) u. { Y } ) |
| 25 |
19
|
snssd |
|- ( ph -> { Y } C_ I ) |
| 26 |
|
undifr |
|- ( { Y } C_ I <-> ( ( I \ { Y } ) u. { Y } ) = I ) |
| 27 |
25 26
|
sylib |
|- ( ph -> ( ( I \ { Y } ) u. { Y } ) = I ) |
| 28 |
24 27
|
eqtr2id |
|- ( ph -> I = ( J u. { Y } ) ) |
| 29 |
28
|
mpteq1d |
|- ( ph -> ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) = ( n e. ( J u. { Y } ) |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) |
| 30 |
29
|
oveq2d |
|- ( ph -> ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) = ( M gsum ( n e. ( J u. { Y } ) |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ) |
| 31 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 32 |
4 31
|
mgpbas |
|- ( Base ` W ) = ( Base ` M ) |
| 33 |
|
eqid |
|- ( .r ` W ) = ( .r ` W ) |
| 34 |
4 33
|
mgpplusg |
|- ( .r ` W ) = ( +g ` M ) |
| 35 |
15
|
idomcringd |
|- ( ph -> R e. CRing ) |
| 36 |
1
|
ply1crng |
|- ( R e. CRing -> W e. CRing ) |
| 37 |
4
|
crngmgp |
|- ( W e. CRing -> M e. CMnd ) |
| 38 |
35 36 37
|
3syl |
|- ( ph -> M e. CMnd ) |
| 39 |
|
diffi |
|- ( I e. Fin -> ( I \ { Y } ) e. Fin ) |
| 40 |
14 39
|
syl |
|- ( ph -> ( I \ { Y } ) e. Fin ) |
| 41 |
20 40
|
eqeltrid |
|- ( ph -> J e. Fin ) |
| 42 |
35 36
|
syl |
|- ( ph -> W e. CRing ) |
| 43 |
42
|
crngringd |
|- ( ph -> W e. Ring ) |
| 44 |
43
|
ringgrpd |
|- ( ph -> W e. Grp ) |
| 45 |
44
|
adantr |
|- ( ( ph /\ n e. J ) -> W e. Grp ) |
| 46 |
15
|
idomringd |
|- ( ph -> R e. Ring ) |
| 47 |
10 1 31
|
vr1cl |
|- ( R e. Ring -> X e. ( Base ` W ) ) |
| 48 |
46 47
|
syl |
|- ( ph -> X e. ( Base ` W ) ) |
| 49 |
48
|
adantr |
|- ( ( ph /\ n e. J ) -> X e. ( Base ` W ) ) |
| 50 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 51 |
|
eqid |
|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
| 52 |
1
|
ply1assa |
|- ( R e. CRing -> W e. AssAlg ) |
| 53 |
35 52
|
syl |
|- ( ph -> W e. AssAlg ) |
| 54 |
53
|
adantr |
|- ( ( ph /\ n e. J ) -> W e. AssAlg ) |
| 55 |
16
|
adantr |
|- ( ( ph /\ n e. J ) -> Z : I --> B ) |
| 56 |
|
difss |
|- ( I \ { Y } ) C_ I |
| 57 |
20 56
|
eqsstri |
|- J C_ I |
| 58 |
57
|
a1i |
|- ( ph -> J C_ I ) |
| 59 |
58
|
sselda |
|- ( ( ph /\ n e. J ) -> n e. I ) |
| 60 |
55 59
|
ffvelcdmd |
|- ( ( ph /\ n e. J ) -> ( Z ` n ) e. B ) |
| 61 |
1
|
ply1sca |
|- ( R e. CRing -> R = ( Scalar ` W ) ) |
| 62 |
35 61
|
syl |
|- ( ph -> R = ( Scalar ` W ) ) |
| 63 |
62
|
fveq2d |
|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` W ) ) ) |
| 64 |
2 63
|
eqtrid |
|- ( ph -> B = ( Base ` ( Scalar ` W ) ) ) |
| 65 |
64
|
adantr |
|- ( ( ph /\ n e. J ) -> B = ( Base ` ( Scalar ` W ) ) ) |
| 66 |
60 65
|
eleqtrd |
|- ( ( ph /\ n e. J ) -> ( Z ` n ) e. ( Base ` ( Scalar ` W ) ) ) |
| 67 |
11 50 51 54 66
|
asclelbas |
|- ( ( ph /\ n e. J ) -> ( A ` ( Z ` n ) ) e. ( Base ` W ) ) |
| 68 |
31 3 45 49 67
|
grpsubcld |
|- ( ( ph /\ n e. J ) -> ( X .- ( A ` ( Z ` n ) ) ) e. ( Base ` W ) ) |
| 69 |
|
neldifsnd |
|- ( ph -> -. Y e. ( I \ { Y } ) ) |
| 70 |
20
|
eleq2i |
|- ( Y e. J <-> Y e. ( I \ { Y } ) ) |
| 71 |
69 70
|
sylnibr |
|- ( ph -> -. Y e. J ) |
| 72 |
64 16
|
feq3dd |
|- ( ph -> Z : I --> ( Base ` ( Scalar ` W ) ) ) |
| 73 |
72 19
|
ffvelcdmd |
|- ( ph -> ( Z ` Y ) e. ( Base ` ( Scalar ` W ) ) ) |
| 74 |
11 50 51 53 73
|
asclelbas |
|- ( ph -> ( A ` ( Z ` Y ) ) e. ( Base ` W ) ) |
| 75 |
31 3 44 48 74
|
grpsubcld |
|- ( ph -> ( X .- ( A ` ( Z ` Y ) ) ) e. ( Base ` W ) ) |
| 76 |
|
2fveq3 |
|- ( n = Y -> ( A ` ( Z ` n ) ) = ( A ` ( Z ` Y ) ) ) |
| 77 |
76
|
oveq2d |
|- ( n = Y -> ( X .- ( A ` ( Z ` n ) ) ) = ( X .- ( A ` ( Z ` Y ) ) ) ) |
| 78 |
32 34 38 41 68 19 71 75 77
|
gsumunsn |
|- ( ph -> ( M gsum ( n e. ( J u. { Y } ) |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) = ( ( M gsum ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) ) |
| 79 |
23 30 78
|
3eqtrd |
|- ( ph -> F = ( ( M gsum ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) ) |
| 80 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
| 81 |
|
eqid |
|- ( .g ` M ) = ( .g ` M ) |
| 82 |
|
eqid |
|- ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) |
| 83 |
|
eqid |
|- ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) = ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) |
| 84 |
|
simpr |
|- ( ( ph /\ n e. J ) -> n e. J ) |
| 85 |
84
|
fvresd |
|- ( ( ph /\ n e. J ) -> ( ( Z |` J ) ` n ) = ( Z ` n ) ) |
| 86 |
85
|
fveq2d |
|- ( ( ph /\ n e. J ) -> ( A ` ( ( Z |` J ) ` n ) ) = ( A ` ( Z ` n ) ) ) |
| 87 |
86
|
oveq2d |
|- ( ( ph /\ n e. J ) -> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) = ( X .- ( A ` ( Z ` n ) ) ) ) |
| 88 |
87
|
mpteq2dva |
|- ( ph -> ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) = ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) |
| 89 |
88
|
oveq2d |
|- ( ph -> ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) = ( M gsum ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ) |
| 90 |
68
|
ralrimiva |
|- ( ph -> A. n e. J ( X .- ( A ` ( Z ` n ) ) ) e. ( Base ` W ) ) |
| 91 |
32 38 41 90
|
gsummptcl |
|- ( ph -> ( M gsum ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) e. ( Base ` W ) ) |
| 92 |
89 91
|
eqeltrd |
|- ( ph -> ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) e. ( Base ` W ) ) |
| 93 |
1 10 31 80 4 81 82 83 46 92
|
ply1coedeg |
|- ( ph -> ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) = ( W gsum ( l e. ( 0 ... ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 94 |
22
|
oveq2d |
|- ( ph -> ( 0 ... ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ) = ( 0 ... ( # ` J ) ) ) |
| 95 |
94
|
mpteq1d |
|- ( ph -> ( l e. ( 0 ... ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) = ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) |
| 96 |
95
|
oveq2d |
|- ( ph -> ( W gsum ( l e. ( 0 ... ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 97 |
93 89 96
|
3eqtr3d |
|- ( ph -> ( M gsum ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) = ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 98 |
43
|
ringcmnd |
|- ( ph -> W e. CMnd ) |
| 99 |
|
hashcl |
|- ( J e. Fin -> ( # ` J ) e. NN0 ) |
| 100 |
41 99
|
syl |
|- ( ph -> ( # ` J ) e. NN0 ) |
| 101 |
1
|
ply1lmod |
|- ( R e. Ring -> W e. LMod ) |
| 102 |
46 101
|
syl |
|- ( ph -> W e. LMod ) |
| 103 |
102
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> W e. LMod ) |
| 104 |
92
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) e. ( Base ` W ) ) |
| 105 |
62
|
fveq2d |
|- ( ph -> ( Poly1 ` R ) = ( Poly1 ` ( Scalar ` W ) ) ) |
| 106 |
1 105
|
eqtrid |
|- ( ph -> W = ( Poly1 ` ( Scalar ` W ) ) ) |
| 107 |
106
|
fveq2d |
|- ( ph -> ( Base ` W ) = ( Base ` ( Poly1 ` ( Scalar ` W ) ) ) ) |
| 108 |
107
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( Base ` W ) = ( Base ` ( Poly1 ` ( Scalar ` W ) ) ) ) |
| 109 |
104 108
|
eleqtrd |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) e. ( Base ` ( Poly1 ` ( Scalar ` W ) ) ) ) |
| 110 |
|
fz0ssnn0 |
|- ( 0 ... ( # ` J ) ) C_ NN0 |
| 111 |
|
simpr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> l e. ( 0 ... ( # ` J ) ) ) |
| 112 |
110 111
|
sselid |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> l e. NN0 ) |
| 113 |
|
eqid |
|- ( Base ` ( Poly1 ` ( Scalar ` W ) ) ) = ( Base ` ( Poly1 ` ( Scalar ` W ) ) ) |
| 114 |
|
eqid |
|- ( Poly1 ` ( Scalar ` W ) ) = ( Poly1 ` ( Scalar ` W ) ) |
| 115 |
82 113 114 51
|
coe1fvalcl |
|- ( ( ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) e. ( Base ` ( Poly1 ` ( Scalar ` W ) ) ) /\ l e. NN0 ) -> ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) e. ( Base ` ( Scalar ` W ) ) ) |
| 116 |
109 112 115
|
syl2anc |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) e. ( Base ` ( Scalar ` W ) ) ) |
| 117 |
38
|
cmnmndd |
|- ( ph -> M e. Mnd ) |
| 118 |
117
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> M e. Mnd ) |
| 119 |
46
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> R e. Ring ) |
| 120 |
119 47
|
syl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> X e. ( Base ` W ) ) |
| 121 |
32 81 118 112 120
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( l ( .g ` M ) X ) e. ( Base ` W ) ) |
| 122 |
31 50 80 51 103 116 121
|
lmodvscld |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 123 |
|
simpr |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> l = ( ( # ` J ) - k ) ) |
| 124 |
123
|
fveq2d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) = ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ) |
| 125 |
|
oveq1 |
|- ( l = ( ( # ` J ) - k ) -> ( l ( .g ` M ) X ) = ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) |
| 126 |
125
|
adantl |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( l ( .g ` M ) X ) = ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) |
| 127 |
124 126
|
oveq12d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) = ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) |
| 128 |
31 98 100 122 127
|
gsummptrev |
|- ( ph -> ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` l ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) = ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) ) |
| 129 |
|
fveq1 |
|- ( z = ( Z |` J ) -> ( z ` n ) = ( ( Z |` J ) ` n ) ) |
| 130 |
129
|
fveq2d |
|- ( z = ( Z |` J ) -> ( A ` ( z ` n ) ) = ( A ` ( ( Z |` J ) ` n ) ) ) |
| 131 |
130
|
oveq2d |
|- ( z = ( Z |` J ) -> ( X .- ( A ` ( z ` n ) ) ) = ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) |
| 132 |
131
|
mpteq2dv |
|- ( z = ( Z |` J ) -> ( n e. J |-> ( X .- ( A ` ( z ` n ) ) ) ) = ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) |
| 133 |
132
|
oveq2d |
|- ( z = ( Z |` J ) -> ( M gsum ( n e. J |-> ( X .- ( A ` ( z ` n ) ) ) ) ) = ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) |
| 134 |
133
|
fveq2d |
|- ( z = ( Z |` J ) -> ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) = ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ) |
| 135 |
134
|
fveq1d |
|- ( z = ( Z |` J ) -> ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( z ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) = ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ) |
| 136 |
|
fveq2 |
|- ( z = ( Z |` J ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` z ) = ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) |
| 137 |
136
|
oveq2d |
|- ( z = ( Z |` J ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` z ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) |
| 138 |
135 137
|
eqeq12d |
|- ( z = ( Z |` 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 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 139 |
138
|
ralbidv |
|- ( z = ( Z |` 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 ... ( # ` J ) ) ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 140 |
2
|
fvexi |
|- B e. _V |
| 141 |
140
|
a1i |
|- ( ph -> B e. _V ) |
| 142 |
16 58
|
fssresd |
|- ( ph -> ( Z |` J ) : J --> B ) |
| 143 |
141 41 142
|
elmapdd |
|- ( ph -> ( Z |` J ) e. ( B ^m J ) ) |
| 144 |
139 21 143
|
rspcdva |
|- ( ph -> A. k e. ( 0 ... ( # ` J ) ) ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) |
| 145 |
144
|
r19.21bi |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) |
| 146 |
145
|
oveq1d |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) = ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) |
| 147 |
146
|
mpteq2dva |
|- ( ph -> ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) = ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) |
| 148 |
147
|
oveq2d |
|- ( ph -> ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) = ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) ) |
| 149 |
|
eqid |
|- ( mulGrp ` R ) = ( mulGrp ` R ) |
| 150 |
149 2
|
mgpbas |
|- B = ( Base ` ( mulGrp ` R ) ) |
| 151 |
149
|
ringmgp |
|- ( R e. Ring -> ( mulGrp ` R ) e. Mnd ) |
| 152 |
119 151
|
syl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( mulGrp ` R ) e. Mnd ) |
| 153 |
|
fznn0sub2 |
|- ( l e. ( 0 ... ( # ` J ) ) -> ( ( # ` J ) - l ) e. ( 0 ... ( # ` J ) ) ) |
| 154 |
153
|
adantl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( # ` J ) - l ) e. ( 0 ... ( # ` J ) ) ) |
| 155 |
110 154
|
sselid |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( # ` J ) - l ) e. NN0 ) |
| 156 |
46
|
ringgrpd |
|- ( ph -> R e. Grp ) |
| 157 |
2 8 46
|
ringidcld |
|- ( ph -> .1. e. B ) |
| 158 |
2 7 156 157
|
grpinvcld |
|- ( ph -> ( N ` .1. ) e. B ) |
| 159 |
158
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( N ` .1. ) e. B ) |
| 160 |
150 12 152 155 159
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) e. B ) |
| 161 |
|
eqid |
|- ( J eval R ) = ( J eval R ) |
| 162 |
|
eqid |
|- ( J mPoly R ) = ( J mPoly R ) |
| 163 |
|
eqid |
|- ( Base ` ( J mPoly R ) ) = ( Base ` ( J mPoly R ) ) |
| 164 |
41
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> J e. Fin ) |
| 165 |
35
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> R e. CRing ) |
| 166 |
|
eqid |
|- { h e. ( NN0 ^m J ) | h finSupp 0 } = { h e. ( NN0 ^m J ) | h finSupp 0 } |
| 167 |
166 164 119 155 163
|
esplympl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) e. ( Base ` ( J mPoly R ) ) ) |
| 168 |
143
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( Z |` J ) e. ( B ^m J ) ) |
| 169 |
161 162 163 2 164 165 167 168
|
evlcl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) e. B ) |
| 170 |
2 9 119 160 169
|
ringcld |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) e. B ) |
| 171 |
1 31 2 80 119 170 121
|
ply1vscl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 172 |
100
|
nn0cnd |
|- ( ph -> ( # ` J ) e. CC ) |
| 173 |
172
|
ad2antrr |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( # ` J ) e. CC ) |
| 174 |
|
simplr |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> k e. ( 0 ... ( # ` J ) ) ) |
| 175 |
110 174
|
sselid |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> k e. NN0 ) |
| 176 |
175
|
nn0cnd |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> k e. CC ) |
| 177 |
173 176
|
subcld |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( # ` J ) - k ) e. CC ) |
| 178 |
123 177
|
eqeltrd |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> l e. CC ) |
| 179 |
173 178
|
subcld |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( # ` J ) - l ) e. CC ) |
| 180 |
173 178
|
nncand |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( # ` J ) - ( ( # ` J ) - l ) ) = l ) |
| 181 |
180 123
|
eqtrd |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( # ` J ) - ( ( # ` J ) - l ) ) = ( ( # ` J ) - k ) ) |
| 182 |
173 179 176 181
|
subcand |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( # ` J ) - l ) = k ) |
| 183 |
182
|
oveq1d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) = ( k .^ ( N ` .1. ) ) ) |
| 184 |
182
|
fveq2d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) = ( ( J eSymPoly R ) ` k ) ) |
| 185 |
184
|
fveq2d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) = ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ) |
| 186 |
185
|
fveq1d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) = ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) |
| 187 |
183 186
|
oveq12d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) |
| 188 |
187 126
|
oveq12d |
|- ( ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) /\ l = ( ( # ` J ) - k ) ) -> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) = ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) |
| 189 |
31 98 100 171 188
|
gsummptrev |
|- ( ph -> ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) = ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) ) |
| 190 |
148 189
|
eqtr4d |
|- ( ph -> ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( coe1 ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) ` ( ( # ` J ) - k ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 191 |
97 128 190
|
3eqtrd |
|- ( ph -> ( M gsum ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) = ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 192 |
191
|
oveq1d |
|- ( ph -> ( ( M gsum ( n e. J |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) = ( ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) ) |
| 193 |
|
eqid |
|- ( +g ` W ) = ( +g ` W ) |
| 194 |
46
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> R e. Ring ) |
| 195 |
194 151
|
syl |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( mulGrp ` R ) e. Mnd ) |
| 196 |
|
elfznn0 |
|- ( i e. ( 0 ... ( # ` J ) ) -> i e. NN0 ) |
| 197 |
196
|
adantl |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> i e. NN0 ) |
| 198 |
158
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( N ` .1. ) e. B ) |
| 199 |
150 12 195 197 198
|
mulgnn0cld |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( i .^ ( N ` .1. ) ) e. B ) |
| 200 |
41
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> J e. Fin ) |
| 201 |
35
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> R e. CRing ) |
| 202 |
166 200 194 197 163
|
esplympl |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( ( J eSymPoly R ) ` i ) e. ( Base ` ( J mPoly R ) ) ) |
| 203 |
143
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( Z |` J ) e. ( B ^m J ) ) |
| 204 |
161 162 163 2 200 201 202 203
|
evlcl |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) e. B ) |
| 205 |
2 9 194 199 204
|
ringcld |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) e. B ) |
| 206 |
117
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> M e. Mnd ) |
| 207 |
|
fznn0sub2 |
|- ( i e. ( 0 ... ( # ` J ) ) -> ( ( # ` J ) - i ) e. ( 0 ... ( # ` J ) ) ) |
| 208 |
207
|
adantl |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( ( # ` J ) - i ) e. ( 0 ... ( # ` J ) ) ) |
| 209 |
110 208
|
sselid |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( ( # ` J ) - i ) e. NN0 ) |
| 210 |
48
|
adantr |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> X e. ( Base ` W ) ) |
| 211 |
32 81 206 209 210
|
mulgnn0cld |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( ( ( # ` J ) - i ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 212 |
1 31 2 80 194 205 211
|
ply1vscl |
|- ( ( ph /\ i e. ( 0 ... ( # ` J ) ) ) -> ( ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - i ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 213 |
|
oveq1 |
|- ( i = 0 -> ( i .^ ( N ` .1. ) ) = ( 0 .^ ( N ` .1. ) ) ) |
| 214 |
|
2fveq3 |
|- ( i = 0 -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) = ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ) |
| 215 |
214
|
fveq1d |
|- ( i = 0 -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) = ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) |
| 216 |
213 215
|
oveq12d |
|- ( i = 0 -> ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ) |
| 217 |
|
oveq2 |
|- ( i = 0 -> ( ( # ` J ) - i ) = ( ( # ` J ) - 0 ) ) |
| 218 |
217
|
oveq1d |
|- ( i = 0 -> ( ( ( # ` J ) - i ) ( .g ` M ) X ) = ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ) |
| 219 |
216 218
|
oveq12d |
|- ( i = 0 -> ( ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - i ) ( .g ` M ) X ) ) = ( ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ) ) |
| 220 |
|
oveq1 |
|- ( i = ( # ` J ) -> ( i .^ ( N ` .1. ) ) = ( ( # ` J ) .^ ( N ` .1. ) ) ) |
| 221 |
|
2fveq3 |
|- ( i = ( # ` J ) -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) = ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ) |
| 222 |
221
|
fveq1d |
|- ( i = ( # ` J ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) = ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) |
| 223 |
220 222
|
oveq12d |
|- ( i = ( # ` J ) -> ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) = ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) |
| 224 |
|
oveq2 |
|- ( i = ( # ` J ) -> ( ( # ` J ) - i ) = ( ( # ` J ) - ( # ` J ) ) ) |
| 225 |
224
|
oveq1d |
|- ( i = ( # ` J ) -> ( ( ( # ` J ) - i ) ( .g ` M ) X ) = ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) |
| 226 |
223 225
|
oveq12d |
|- ( i = ( # ` J ) -> ( ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - i ) ( .g ` M ) X ) ) = ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ) |
| 227 |
|
oveq1 |
|- ( i = k -> ( i .^ ( N ` .1. ) ) = ( k .^ ( N ` .1. ) ) ) |
| 228 |
|
2fveq3 |
|- ( i = k -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) = ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ) |
| 229 |
228
|
fveq1d |
|- ( i = k -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) = ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) |
| 230 |
227 229
|
oveq12d |
|- ( i = k -> ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) |
| 231 |
|
oveq2 |
|- ( i = k -> ( ( # ` J ) - i ) = ( ( # ` J ) - k ) ) |
| 232 |
231
|
oveq1d |
|- ( i = k -> ( ( ( # ` J ) - i ) ( .g ` M ) X ) = ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) |
| 233 |
230 232
|
oveq12d |
|- ( i = k -> ( ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - i ) ( .g ` M ) X ) ) = ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) |
| 234 |
|
oveq1 |
|- ( i = ( k + 1 ) -> ( i .^ ( N ` .1. ) ) = ( ( k + 1 ) .^ ( N ` .1. ) ) ) |
| 235 |
|
2fveq3 |
|- ( i = ( k + 1 ) -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) = ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ) |
| 236 |
235
|
fveq1d |
|- ( i = ( k + 1 ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) = ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) |
| 237 |
234 236
|
oveq12d |
|- ( i = ( k + 1 ) -> ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) = ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ) |
| 238 |
|
oveq2 |
|- ( i = ( k + 1 ) -> ( ( # ` J ) - i ) = ( ( # ` J ) - ( k + 1 ) ) ) |
| 239 |
238
|
oveq1d |
|- ( i = ( k + 1 ) -> ( ( ( # ` J ) - i ) ( .g ` M ) X ) = ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ) |
| 240 |
237 239
|
oveq12d |
|- ( i = ( k + 1 ) -> ( ( ( i .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` i ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - i ) ( .g ` M ) X ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ) ) |
| 241 |
|
eqid |
|- ( invg ` W ) = ( invg ` W ) |
| 242 |
46 151
|
syl |
|- ( ph -> ( mulGrp ` R ) e. Mnd ) |
| 243 |
|
0nn0 |
|- 0 e. NN0 |
| 244 |
243
|
a1i |
|- ( ph -> 0 e. NN0 ) |
| 245 |
150 12 242 244 158
|
mulgnn0cld |
|- ( ph -> ( 0 .^ ( N ` .1. ) ) e. B ) |
| 246 |
8 157
|
eqeltrrid |
|- ( ph -> ( 1r ` R ) e. B ) |
| 247 |
2 9 46 245 246
|
ringcld |
|- ( ph -> ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) e. B ) |
| 248 |
|
hashcl |
|- ( I e. Fin -> ( # ` I ) e. NN0 ) |
| 249 |
14 248
|
syl |
|- ( ph -> ( # ` I ) e. NN0 ) |
| 250 |
13 249
|
eqeltrid |
|- ( ph -> H e. NN0 ) |
| 251 |
32 81 117 250 48
|
mulgnn0cld |
|- ( ph -> ( H ( .g ` M ) X ) e. ( Base ` W ) ) |
| 252 |
1 31 2 80 46 247 251
|
ply1vscl |
|- ( ph -> ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 253 |
150 12 242 250 158
|
mulgnn0cld |
|- ( ph -> ( H .^ ( N ` .1. ) ) e. B ) |
| 254 |
|
eqid |
|- ( I mPoly R ) = ( I mPoly R ) |
| 255 |
|
eqid |
|- ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) ) |
| 256 |
6
|
fveq1i |
|- ( E ` H ) = ( ( I eSymPoly R ) ` H ) |
| 257 |
|
eqid |
|- { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 } |
| 258 |
257 14 46 250 255
|
esplympl |
|- ( ph -> ( ( I eSymPoly R ) ` H ) e. ( Base ` ( I mPoly R ) ) ) |
| 259 |
256 258
|
eqeltrid |
|- ( ph -> ( E ` H ) e. ( Base ` ( I mPoly R ) ) ) |
| 260 |
141 14 16
|
elmapdd |
|- ( ph -> Z e. ( B ^m I ) ) |
| 261 |
5 254 255 2 14 35 259 260
|
evlcl |
|- ( ph -> ( ( Q ` ( E ` H ) ) ` Z ) e. B ) |
| 262 |
2 9 46 253 261
|
ringcld |
|- ( ph -> ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) e. B ) |
| 263 |
32 81 117 244 48
|
mulgnn0cld |
|- ( ph -> ( 0 ( .g ` M ) X ) e. ( Base ` W ) ) |
| 264 |
1 31 2 80 46 262 263
|
ply1vscl |
|- ( ph -> ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 265 |
31 193 3 241 44 252 264
|
grpsubinv |
|- ( ph -> ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) .- ( ( invg ` W ) ` ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) = ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) |
| 266 |
166 41 46 244 163
|
esplympl |
|- ( ph -> ( ( J eSymPoly R ) ` 0 ) e. ( Base ` ( J mPoly R ) ) ) |
| 267 |
161 162 163 2 41 35 266 143
|
evlcl |
|- ( ph -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) e. B ) |
| 268 |
2 9 46 245 267
|
ringcld |
|- ( ph -> ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) e. B ) |
| 269 |
268 64
|
eleqtrd |
|- ( ph -> ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) e. ( Base ` ( Scalar ` W ) ) ) |
| 270 |
172
|
subid1d |
|- ( ph -> ( ( # ` J ) - 0 ) = ( # ` J ) ) |
| 271 |
270 100
|
eqeltrd |
|- ( ph -> ( ( # ` J ) - 0 ) e. NN0 ) |
| 272 |
32 81 117 271 48
|
mulgnn0cld |
|- ( ph -> ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 273 |
31 50 51 80 33 53 269 272 48
|
assaassd |
|- ( ph -> ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ) ( .r ` W ) X ) = ( ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ( .r ` W ) X ) ) ) |
| 274 |
|
eqid |
|- ( 1r ` ( J mPoly R ) ) = ( 1r ` ( J mPoly R ) ) |
| 275 |
41 46 274
|
esplyfval0 |
|- ( ph -> ( ( J eSymPoly R ) ` 0 ) = ( 1r ` ( J mPoly R ) ) ) |
| 276 |
275
|
fveq2d |
|- ( ph -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) = ( ( J eval R ) ` ( 1r ` ( J mPoly R ) ) ) ) |
| 277 |
|
eqid |
|- ( algSc ` ( J mPoly R ) ) = ( algSc ` ( J mPoly R ) ) |
| 278 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
| 279 |
162 277 278 274 41 46
|
mplascl1 |
|- ( ph -> ( ( algSc ` ( J mPoly R ) ) ` ( 1r ` R ) ) = ( 1r ` ( J mPoly R ) ) ) |
| 280 |
279
|
fveq2d |
|- ( ph -> ( ( J eval R ) ` ( ( algSc ` ( J mPoly R ) ) ` ( 1r ` R ) ) ) = ( ( J eval R ) ` ( 1r ` ( J mPoly R ) ) ) ) |
| 281 |
276 280
|
eqtr4d |
|- ( ph -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) = ( ( J eval R ) ` ( ( algSc ` ( J mPoly R ) ) ` ( 1r ` R ) ) ) ) |
| 282 |
281
|
fveq1d |
|- ( ph -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) = ( ( ( J eval R ) ` ( ( algSc ` ( J mPoly R ) ) ` ( 1r ` R ) ) ) ` ( Z |` J ) ) ) |
| 283 |
161 162 2 277 41 35 246 142
|
evlscaval |
|- ( ph -> ( ( ( J eval R ) ` ( ( algSc ` ( J mPoly R ) ) ` ( 1r ` R ) ) ) ` ( Z |` J ) ) = ( 1r ` R ) ) |
| 284 |
282 283
|
eqtrd |
|- ( ph -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) = ( 1r ` R ) ) |
| 285 |
284
|
oveq2d |
|- ( ph -> ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ) |
| 286 |
32 81 34
|
mulgnn0p1 |
|- ( ( M e. Mnd /\ ( # ` J ) e. NN0 /\ X e. ( Base ` W ) ) -> ( ( ( # ` J ) + 1 ) ( .g ` M ) X ) = ( ( ( # ` J ) ( .g ` M ) X ) ( .r ` W ) X ) ) |
| 287 |
117 100 48 286
|
syl3anc |
|- ( ph -> ( ( ( # ` J ) + 1 ) ( .g ` M ) X ) = ( ( ( # ` J ) ( .g ` M ) X ) ( .r ` W ) X ) ) |
| 288 |
|
hashdifsn |
|- ( ( I e. Fin /\ Y e. I ) -> ( # ` ( I \ { Y } ) ) = ( ( # ` I ) - 1 ) ) |
| 289 |
14 19 288
|
syl2anc |
|- ( ph -> ( # ` ( I \ { Y } ) ) = ( ( # ` I ) - 1 ) ) |
| 290 |
20
|
fveq2i |
|- ( # ` J ) = ( # ` ( I \ { Y } ) ) |
| 291 |
13
|
oveq1i |
|- ( H - 1 ) = ( ( # ` I ) - 1 ) |
| 292 |
289 290 291
|
3eqtr4g |
|- ( ph -> ( # ` J ) = ( H - 1 ) ) |
| 293 |
292
|
oveq1d |
|- ( ph -> ( ( # ` J ) + 1 ) = ( ( H - 1 ) + 1 ) ) |
| 294 |
250
|
nn0cnd |
|- ( ph -> H e. CC ) |
| 295 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
| 296 |
294 295
|
npcand |
|- ( ph -> ( ( H - 1 ) + 1 ) = H ) |
| 297 |
293 296
|
eqtr2d |
|- ( ph -> H = ( ( # ` J ) + 1 ) ) |
| 298 |
297
|
oveq1d |
|- ( ph -> ( H ( .g ` M ) X ) = ( ( ( # ` J ) + 1 ) ( .g ` M ) X ) ) |
| 299 |
270
|
oveq1d |
|- ( ph -> ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) = ( ( # ` J ) ( .g ` M ) X ) ) |
| 300 |
299
|
oveq1d |
|- ( ph -> ( ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ( .r ` W ) X ) = ( ( ( # ` J ) ( .g ` M ) X ) ( .r ` W ) X ) ) |
| 301 |
287 298 300
|
3eqtr4rd |
|- ( ph -> ( ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ( .r ` W ) X ) = ( H ( .g ` M ) X ) ) |
| 302 |
285 301
|
oveq12d |
|- ( ph -> ( ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ( .r ` W ) X ) ) = ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) |
| 303 |
273 302
|
eqtr2d |
|- ( ph -> ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) = ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ) ( .r ` W ) X ) ) |
| 304 |
62
|
fveq2d |
|- ( ph -> ( .r ` R ) = ( .r ` ( Scalar ` W ) ) ) |
| 305 |
9 304
|
eqtrid |
|- ( ph -> .x. = ( .r ` ( Scalar ` W ) ) ) |
| 306 |
305
|
oveqd |
|- ( ph -> ( ( Z ` Y ) .x. ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) = ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ) |
| 307 |
306
|
oveq1d |
|- ( ph -> ( ( ( Z ` Y ) .x. ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) = ( ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ) |
| 308 |
16 19
|
ffvelcdmd |
|- ( ph -> ( Z ` Y ) e. B ) |
| 309 |
150 12 242 100 158
|
mulgnn0cld |
|- ( ph -> ( ( # ` J ) .^ ( N ` .1. ) ) e. B ) |
| 310 |
166 41 46 100 163
|
esplympl |
|- ( ph -> ( ( J eSymPoly R ) ` ( # ` J ) ) e. ( Base ` ( J mPoly R ) ) ) |
| 311 |
161 162 163 2 41 35 310 143
|
evlcl |
|- ( ph -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) e. B ) |
| 312 |
2 9 35 308 309 311
|
crng12d |
|- ( ph -> ( ( Z ` Y ) .x. ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) = ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ) |
| 313 |
297
|
oveq1d |
|- ( ph -> ( H .^ ( N ` .1. ) ) = ( ( ( # ` J ) + 1 ) .^ ( N ` .1. ) ) ) |
| 314 |
8 7 12 46 100
|
ringm1expp1 |
|- ( ph -> ( ( ( # ` J ) + 1 ) .^ ( N ` .1. ) ) = ( N ` ( ( # ` J ) .^ ( N ` .1. ) ) ) ) |
| 315 |
313 314
|
eqtrd |
|- ( ph -> ( H .^ ( N ` .1. ) ) = ( N ` ( ( # ` J ) .^ ( N ` .1. ) ) ) ) |
| 316 |
315
|
fveq2d |
|- ( ph -> ( N ` ( H .^ ( N ` .1. ) ) ) = ( N ` ( N ` ( ( # ` J ) .^ ( N ` .1. ) ) ) ) ) |
| 317 |
2 7 156 309
|
grpinvinvd |
|- ( ph -> ( N ` ( N ` ( ( # ` J ) .^ ( N ` .1. ) ) ) ) = ( ( # ` J ) .^ ( N ` .1. ) ) ) |
| 318 |
316 317
|
eqtrd |
|- ( ph -> ( N ` ( H .^ ( N ` .1. ) ) ) = ( ( # ` J ) .^ ( N ` .1. ) ) ) |
| 319 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
| 320 |
|
eqid |
|- ( J eSymPoly R ) = ( J eSymPoly R ) |
| 321 |
|
eqid |
|- ( # ` J ) = ( # ` J ) |
| 322 |
2 319 9 5 161 6 320 13 321 20 14 35 19 16
|
esplyfvn |
|- ( ph -> ( ( Q ` ( E ` H ) ) ` Z ) = ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) |
| 323 |
318 322
|
oveq12d |
|- ( ph -> ( ( N ` ( H .^ ( N ` .1. ) ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) = ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ) |
| 324 |
312 323
|
eqtr4d |
|- ( ph -> ( ( Z ` Y ) .x. ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) = ( ( N ` ( H .^ ( N ` .1. ) ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) |
| 325 |
2 9 7 46 253 261
|
ringmneg1 |
|- ( ph -> ( ( N ` ( H .^ ( N ` .1. ) ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) = ( N ` ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) ) |
| 326 |
62
|
fveq2d |
|- ( ph -> ( invg ` R ) = ( invg ` ( Scalar ` W ) ) ) |
| 327 |
7 326
|
eqtrid |
|- ( ph -> N = ( invg ` ( Scalar ` W ) ) ) |
| 328 |
327
|
fveq1d |
|- ( ph -> ( N ` ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) = ( ( invg ` ( Scalar ` W ) ) ` ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) ) |
| 329 |
324 325 328
|
3eqtrd |
|- ( ph -> ( ( Z ` Y ) .x. ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) = ( ( invg ` ( Scalar ` W ) ) ` ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) ) |
| 330 |
172
|
subidd |
|- ( ph -> ( ( # ` J ) - ( # ` J ) ) = 0 ) |
| 331 |
330
|
oveq1d |
|- ( ph -> ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) = ( 0 ( .g ` M ) X ) ) |
| 332 |
329 331
|
oveq12d |
|- ( ph -> ( ( ( Z ` Y ) .x. ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) = ( ( ( invg ` ( Scalar ` W ) ) ` ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) |
| 333 |
2 9 46 309 311
|
ringcld |
|- ( ph -> ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) e. B ) |
| 334 |
333 64
|
eleqtrd |
|- ( ph -> ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) e. ( Base ` ( Scalar ` W ) ) ) |
| 335 |
330 244
|
eqeltrd |
|- ( ph -> ( ( # ` J ) - ( # ` J ) ) e. NN0 ) |
| 336 |
32 81 117 335 48
|
mulgnn0cld |
|- ( ph -> ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 337 |
|
eqid |
|- ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) ) |
| 338 |
31 50 80 51 337
|
lmodvsass |
|- ( ( W e. LMod /\ ( ( Z ` Y ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) e. ( Base ` W ) ) ) -> ( ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ) ) |
| 339 |
102 73 334 336 338
|
syl13anc |
|- ( ph -> ( ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ) ) |
| 340 |
307 332 339
|
3eqtr3d |
|- ( ph -> ( ( ( invg ` ( Scalar ` W ) ) ` ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ) ) |
| 341 |
|
eqid |
|- ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) ) |
| 342 |
262 64
|
eleqtrd |
|- ( ph -> ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) e. ( Base ` ( Scalar ` W ) ) ) |
| 343 |
31 50 80 241 51 341 102 263 342
|
lmodvsneg |
|- ( ph -> ( ( invg ` W ) ` ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) = ( ( ( invg ` ( Scalar ` W ) ) ` ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) |
| 344 |
1 31 2 80 46 333 336
|
ply1vscl |
|- ( ph -> ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 345 |
11 50 51 31 33 80
|
asclmul2 |
|- ( ( W e. AssAlg /\ ( Z ` Y ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) e. ( Base ` W ) ) -> ( ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ) ) |
| 346 |
53 73 344 345
|
syl3anc |
|- ( ph -> ( ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ) ) |
| 347 |
340 343 346
|
3eqtr4d |
|- ( ph -> ( ( invg ` W ) ` ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) = ( ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) ) |
| 348 |
303 347
|
oveq12d |
|- ( ph -> ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) .- ( ( invg ` W ) ` ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) = ( ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ) ( .r ` W ) X ) .- ( ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) ) ) |
| 349 |
265 348
|
eqtr3d |
|- ( ph -> ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) = ( ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` 0 ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - 0 ) ( .g ` M ) X ) ) ( .r ` W ) X ) .- ( ( ( ( ( # ` J ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( # ` J ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( # ` J ) ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) ) ) |
| 350 |
46
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> R e. Ring ) |
| 351 |
350 151
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( mulGrp ` R ) e. Mnd ) |
| 352 |
|
fzossfz |
|- ( 0 ..^ ( # ` J ) ) C_ ( 0 ... ( # ` J ) ) |
| 353 |
|
simpr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> k e. ( 0 ..^ ( # ` J ) ) ) |
| 354 |
352 353
|
sselid |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> k e. ( 0 ... ( # ` J ) ) ) |
| 355 |
110 354
|
sselid |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> k e. NN0 ) |
| 356 |
|
peano2nn0 |
|- ( k e. NN0 -> ( k + 1 ) e. NN0 ) |
| 357 |
355 356
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( k + 1 ) e. NN0 ) |
| 358 |
158
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( N ` .1. ) e. B ) |
| 359 |
150 12 351 357 358
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( k + 1 ) .^ ( N ` .1. ) ) e. B ) |
| 360 |
41
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> J e. Fin ) |
| 361 |
35
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> R e. CRing ) |
| 362 |
166 360 350 357 163
|
esplympl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( J eSymPoly R ) ` ( k + 1 ) ) e. ( Base ` ( J mPoly R ) ) ) |
| 363 |
143
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( Z |` J ) e. ( B ^m J ) ) |
| 364 |
161 162 163 2 360 361 362 363
|
evlcl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) e. B ) |
| 365 |
16
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> Z : I --> B ) |
| 366 |
19
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> Y e. I ) |
| 367 |
365 366
|
ffvelcdmd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( Z ` Y ) e. B ) |
| 368 |
166 360 350 355 163
|
esplympl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( J eSymPoly R ) ` k ) e. ( Base ` ( J mPoly R ) ) ) |
| 369 |
161 162 163 2 360 361 368 363
|
evlcl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) e. B ) |
| 370 |
2 9 350 367 369
|
ringcld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) e. B ) |
| 371 |
2 319 9 350 359 364 370
|
ringdid |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ( +g ` R ) ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( +g ` R ) ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) ) |
| 372 |
14
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> I e. Fin ) |
| 373 |
6
|
fveq1i |
|- ( E ` ( k + 1 ) ) = ( ( I eSymPoly R ) ` ( k + 1 ) ) |
| 374 |
9 372 361 366 20 320 354 166 373 2 5 161 319 365
|
esplyindfv |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( +g ` R ) ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ) |
| 375 |
46
|
ringabld |
|- ( ph -> R e. Abel ) |
| 376 |
375
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> R e. Abel ) |
| 377 |
2 319 376 370 364
|
ablcomd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( +g ` R ) ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) = ( ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ( +g ` R ) ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 378 |
374 377
|
eqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) = ( ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ( +g ` R ) ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 379 |
378
|
oveq2d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) = ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ( +g ` R ) ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) ) |
| 380 |
|
eqid |
|- ( -g ` R ) = ( -g ` R ) |
| 381 |
156
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> R e. Grp ) |
| 382 |
2 9 350 359 364
|
ringcld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) e. B ) |
| 383 |
2 9 350 359 370
|
ringcld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) e. B ) |
| 384 |
2 319 380 7 381 382 383
|
grpsubinv |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( -g ` R ) ( N ` ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( +g ` R ) ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) ) |
| 385 |
371 379 384
|
3eqtr4d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( -g ` R ) ( N ` ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) ) ) |
| 386 |
62
|
fveq2d |
|- ( ph -> ( -g ` R ) = ( -g ` ( Scalar ` W ) ) ) |
| 387 |
386
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( -g ` R ) = ( -g ` ( Scalar ` W ) ) ) |
| 388 |
|
eqidd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) = ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ) |
| 389 |
242
|
adantr |
|- ( ( ph /\ k e. NN0 ) -> ( mulGrp ` R ) e. Mnd ) |
| 390 |
|
simpr |
|- ( ( ph /\ k e. NN0 ) -> k e. NN0 ) |
| 391 |
158
|
adantr |
|- ( ( ph /\ k e. NN0 ) -> ( N ` .1. ) e. B ) |
| 392 |
150 12 389 390 391
|
mulgnn0cld |
|- ( ( ph /\ k e. NN0 ) -> ( k .^ ( N ` .1. ) ) e. B ) |
| 393 |
355 392
|
syldan |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( k .^ ( N ` .1. ) ) e. B ) |
| 394 |
2 9 350 393 369 367
|
ringassd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) .x. ( Z ` Y ) ) ) ) |
| 395 |
8 7 12 350 355
|
ringm1expp1 |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( k + 1 ) .^ ( N ` .1. ) ) = ( N ` ( k .^ ( N ` .1. ) ) ) ) |
| 396 |
395
|
fveq2d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( N ` ( ( k + 1 ) .^ ( N ` .1. ) ) ) = ( N ` ( N ` ( k .^ ( N ` .1. ) ) ) ) ) |
| 397 |
2 7 381 393
|
grpinvinvd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( N ` ( N ` ( k .^ ( N ` .1. ) ) ) ) = ( k .^ ( N ` .1. ) ) ) |
| 398 |
396 397
|
eqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( N ` ( ( k + 1 ) .^ ( N ` .1. ) ) ) = ( k .^ ( N ` .1. ) ) ) |
| 399 |
2 9 361 367 369
|
crngcomd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) = ( ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) .x. ( Z ` Y ) ) ) |
| 400 |
398 399
|
oveq12d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( N ` ( ( k + 1 ) .^ ( N ` .1. ) ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) = ( ( k .^ ( N ` .1. ) ) .x. ( ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) .x. ( Z ` Y ) ) ) ) |
| 401 |
2 9 7 350 359 370
|
ringmneg1 |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( N ` ( ( k + 1 ) .^ ( N ` .1. ) ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) = ( N ` ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) ) |
| 402 |
394 400 401
|
3eqtr2rd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( N ` ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) = ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ) |
| 403 |
387 388 402
|
oveq123d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( -g ` R ) ( N ` ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Z ` Y ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( -g ` ( Scalar ` W ) ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ) ) |
| 404 |
385 403
|
eqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( -g ` ( Scalar ` W ) ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ) ) |
| 405 |
404
|
oveq1d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) = ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( -g ` ( Scalar ` W ) ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) |
| 406 |
|
eqid |
|- ( -g ` ( Scalar ` W ) ) = ( -g ` ( Scalar ` W ) ) |
| 407 |
350 101
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> W e. LMod ) |
| 408 |
64
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> B = ( Base ` ( Scalar ` W ) ) ) |
| 409 |
382 408
|
eleqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) e. ( Base ` ( Scalar ` W ) ) ) |
| 410 |
2 9 350 393 369
|
ringcld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) e. B ) |
| 411 |
2 9 350 410 367
|
ringcld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) e. B ) |
| 412 |
411 408
|
eleqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) e. ( Base ` ( Scalar ` W ) ) ) |
| 413 |
117
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> M e. Mnd ) |
| 414 |
|
fz0ssnn0 |
|- ( 0 ... H ) C_ NN0 |
| 415 |
|
fzossfz |
|- ( 0 ..^ H ) C_ ( 0 ... H ) |
| 416 |
|
fzssp1 |
|- ( 1 ... ( # ` J ) ) C_ ( 1 ... ( ( # ` J ) + 1 ) ) |
| 417 |
297
|
oveq2d |
|- ( ph -> ( 1 ... H ) = ( 1 ... ( ( # ` J ) + 1 ) ) ) |
| 418 |
416 417
|
sseqtrrid |
|- ( ph -> ( 1 ... ( # ` J ) ) C_ ( 1 ... H ) ) |
| 419 |
418
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( 1 ... ( # ` J ) ) C_ ( 1 ... H ) ) |
| 420 |
360 99
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( # ` J ) e. NN0 ) |
| 421 |
|
fz0add1fz1 |
|- ( ( ( # ` J ) e. NN0 /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( k + 1 ) e. ( 1 ... ( # ` J ) ) ) |
| 422 |
420 353 421
|
syl2anc |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( k + 1 ) e. ( 1 ... ( # ` J ) ) ) |
| 423 |
419 422
|
sseldd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( k + 1 ) e. ( 1 ... H ) ) |
| 424 |
|
ubmelfzo |
|- ( ( k + 1 ) e. ( 1 ... H ) -> ( H - ( k + 1 ) ) e. ( 0 ..^ H ) ) |
| 425 |
423 424
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( H - ( k + 1 ) ) e. ( 0 ..^ H ) ) |
| 426 |
415 425
|
sselid |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( H - ( k + 1 ) ) e. ( 0 ... H ) ) |
| 427 |
414 426
|
sselid |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( H - ( k + 1 ) ) e. NN0 ) |
| 428 |
350 47
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> X e. ( Base ` W ) ) |
| 429 |
32 81 413 427 428
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( H - ( k + 1 ) ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 430 |
31 80 50 51 3 406 407 409 412 429
|
lmodsubdir |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( -g ` ( Scalar ` W ) ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) = ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) .- ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) ) |
| 431 |
297
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> H = ( ( # ` J ) + 1 ) ) |
| 432 |
431
|
oveq1d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( H - ( k + 1 ) ) = ( ( ( # ` J ) + 1 ) - ( k + 1 ) ) ) |
| 433 |
172
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( # ` J ) e. CC ) |
| 434 |
|
1cnd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> 1 e. CC ) |
| 435 |
357
|
nn0cnd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( k + 1 ) e. CC ) |
| 436 |
433 434 435
|
addsubd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( # ` J ) + 1 ) - ( k + 1 ) ) = ( ( ( # ` J ) - ( k + 1 ) ) + 1 ) ) |
| 437 |
432 436
|
eqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( H - ( k + 1 ) ) = ( ( ( # ` J ) - ( k + 1 ) ) + 1 ) ) |
| 438 |
437
|
oveq1d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( H - ( k + 1 ) ) ( .g ` M ) X ) = ( ( ( ( # ` J ) - ( k + 1 ) ) + 1 ) ( .g ` M ) X ) ) |
| 439 |
|
fzofzp1 |
|- ( k e. ( 0 ..^ ( # ` J ) ) -> ( k + 1 ) e. ( 0 ... ( # ` J ) ) ) |
| 440 |
439
|
adantl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( k + 1 ) e. ( 0 ... ( # ` J ) ) ) |
| 441 |
|
fznn0sub2 |
|- ( ( k + 1 ) e. ( 0 ... ( # ` J ) ) -> ( ( # ` J ) - ( k + 1 ) ) e. ( 0 ... ( # ` J ) ) ) |
| 442 |
440 441
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( # ` J ) - ( k + 1 ) ) e. ( 0 ... ( # ` J ) ) ) |
| 443 |
110 442
|
sselid |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( # ` J ) - ( k + 1 ) ) e. NN0 ) |
| 444 |
32 81 34
|
mulgnn0p1 |
|- ( ( M e. Mnd /\ ( ( # ` J ) - ( k + 1 ) ) e. NN0 /\ X e. ( Base ` W ) ) -> ( ( ( ( # ` J ) - ( k + 1 ) ) + 1 ) ( .g ` M ) X ) = ( ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ( .r ` W ) X ) ) |
| 445 |
413 443 428 444
|
syl3anc |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( # ` J ) - ( k + 1 ) ) + 1 ) ( .g ` M ) X ) = ( ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ( .r ` W ) X ) ) |
| 446 |
438 445
|
eqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( H - ( k + 1 ) ) ( .g ` M ) X ) = ( ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ( .r ` W ) X ) ) |
| 447 |
446
|
oveq2d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ( .r ` W ) X ) ) ) |
| 448 |
361 52
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> W e. AssAlg ) |
| 449 |
32 81 413 443 428
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 450 |
31 50 51 80 33 448 409 449 428
|
assaassd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ) ( .r ` W ) X ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ( .r ` W ) X ) ) ) |
| 451 |
447 450
|
eqtr4d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) = ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ) ( .r ` W ) X ) ) |
| 452 |
73
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( Z ` Y ) e. ( Base ` ( Scalar ` W ) ) ) |
| 453 |
410 408
|
eleqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) e. ( Base ` ( Scalar ` W ) ) ) |
| 454 |
|
fznn0sub2 |
|- ( k e. ( 0 ... ( # ` J ) ) -> ( ( # ` J ) - k ) e. ( 0 ... ( # ` J ) ) ) |
| 455 |
354 454
|
syl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( # ` J ) - k ) e. ( 0 ... ( # ` J ) ) ) |
| 456 |
110 455
|
sselid |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( # ` J ) - k ) e. NN0 ) |
| 457 |
32 81 413 456 428
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( # ` J ) - k ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 458 |
31 50 80 51 337
|
lmodvsass |
|- ( ( W e. LMod /\ ( ( Z ` Y ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( ( # ` J ) - k ) ( .g ` M ) X ) e. ( Base ` W ) ) ) -> ( ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) |
| 459 |
407 452 453 457 458
|
syl13anc |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) |
| 460 |
2 9 361 410 367
|
crngcomd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) = ( ( Z ` Y ) .x. ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 461 |
305
|
oveqd |
|- ( ph -> ( ( Z ` Y ) .x. ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) = ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 462 |
461
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( Z ` Y ) .x. ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) = ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 463 |
460 462
|
eqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) = ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ) |
| 464 |
292
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( # ` J ) = ( H - 1 ) ) |
| 465 |
464
|
oveq1d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( # ` J ) - k ) = ( ( H - 1 ) - k ) ) |
| 466 |
294
|
adantr |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> H e. CC ) |
| 467 |
355
|
nn0cnd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> k e. CC ) |
| 468 |
466 467 434
|
sub32d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( H - k ) - 1 ) = ( ( H - 1 ) - k ) ) |
| 469 |
466 467 434
|
subsub4d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( H - k ) - 1 ) = ( H - ( k + 1 ) ) ) |
| 470 |
465 468 469
|
3eqtr2rd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( H - ( k + 1 ) ) = ( ( # ` J ) - k ) ) |
| 471 |
470
|
oveq1d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( H - ( k + 1 ) ) ( .g ` M ) X ) = ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) |
| 472 |
463 471
|
oveq12d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) = ( ( ( Z ` Y ) ( .r ` ( Scalar ` W ) ) ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) |
| 473 |
1 31 2 80 350 410 457
|
ply1vscl |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 474 |
11 50 51 31 33 80
|
asclmul2 |
|- ( ( W e. AssAlg /\ ( Z ` Y ) e. ( Base ` ( Scalar ` W ) ) /\ ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) e. ( Base ` W ) ) -> ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) |
| 475 |
448 452 473 474
|
syl3anc |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) = ( ( Z ` Y ) ( .s ` W ) ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) |
| 476 |
459 472 475
|
3eqtr4d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) = ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) ) |
| 477 |
451 476
|
oveq12d |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) .- ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) .x. ( Z ` Y ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) = ( ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ) ( .r ` W ) X ) .- ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) ) ) |
| 478 |
405 430 477
|
3eqtrd |
|- ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) -> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) = ( ( ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( k + 1 ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - ( k + 1 ) ) ( .g ` M ) X ) ) ( .r ` W ) X ) .- ( ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ( .r ` W ) ( A ` ( Z ` Y ) ) ) ) ) |
| 479 |
31 193 3 33 43 48 74 100 212 219 226 233 240 349 478
|
gsummulsubdishift2s |
|- ( ph -> ( ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) = ( ( W gsum ( k e. ( 0 ..^ ( # ` J ) ) |-> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) ) |
| 480 |
46
|
adantr |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> R e. Ring ) |
| 481 |
480 151
|
syl |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( mulGrp ` R ) e. Mnd ) |
| 482 |
110
|
a1i |
|- ( ph -> ( 0 ... ( # ` J ) ) C_ NN0 ) |
| 483 |
482
|
sselda |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> k e. NN0 ) |
| 484 |
158
|
adantr |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( N ` .1. ) e. B ) |
| 485 |
150 12 481 483 484
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( k .^ ( N ` .1. ) ) e. B ) |
| 486 |
41
|
adantr |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> J e. Fin ) |
| 487 |
35
|
adantr |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> R e. CRing ) |
| 488 |
166 486 480 483 163
|
esplympl |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( J eSymPoly R ) ` k ) e. ( Base ` ( J mPoly R ) ) ) |
| 489 |
143
|
adantr |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( Z |` J ) e. ( B ^m J ) ) |
| 490 |
161 162 163 2 486 487 488 489
|
evlcl |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) e. B ) |
| 491 |
2 9 480 485 490
|
ringcld |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) e. B ) |
| 492 |
117
|
adantr |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> M e. Mnd ) |
| 493 |
454
|
adantl |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( # ` J ) - k ) e. ( 0 ... ( # ` J ) ) ) |
| 494 |
110 493
|
sselid |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( # ` J ) - k ) e. NN0 ) |
| 495 |
48
|
adantr |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> X e. ( Base ` W ) ) |
| 496 |
32 81 492 494 495
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( ( # ` J ) - k ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 497 |
1 31 2 80 480 491 496
|
ply1vscl |
|- ( ( ph /\ k e. ( 0 ... ( # ` J ) ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 498 |
|
oveq1 |
|- ( k = ( ( # ` J ) - l ) -> ( k .^ ( N ` .1. ) ) = ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) ) |
| 499 |
|
2fveq3 |
|- ( k = ( ( # ` J ) - l ) -> ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) = ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ) |
| 500 |
499
|
fveq1d |
|- ( k = ( ( # ` J ) - l ) -> ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) = ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) |
| 501 |
498 500
|
oveq12d |
|- ( k = ( ( # ` J ) - l ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) = ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ) |
| 502 |
501
|
adantl |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) = ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ) |
| 503 |
|
simpr |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> k = ( ( # ` J ) - l ) ) |
| 504 |
503
|
oveq2d |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> ( ( # ` J ) - k ) = ( ( # ` J ) - ( ( # ` J ) - l ) ) ) |
| 505 |
172
|
ad2antrr |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> ( # ` J ) e. CC ) |
| 506 |
112
|
adantr |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> l e. NN0 ) |
| 507 |
506
|
nn0cnd |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> l e. CC ) |
| 508 |
505 507
|
nncand |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> ( ( # ` J ) - ( ( # ` J ) - l ) ) = l ) |
| 509 |
504 508
|
eqtrd |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> ( ( # ` J ) - k ) = l ) |
| 510 |
509
|
oveq1d |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> ( ( ( # ` J ) - k ) ( .g ` M ) X ) = ( l ( .g ` M ) X ) ) |
| 511 |
502 510
|
oveq12d |
|- ( ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) /\ k = ( ( # ` J ) - l ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) = ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) |
| 512 |
31 98 100 497 511
|
gsummptrev |
|- ( ph -> ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 513 |
512
|
oveq1d |
|- ( ph -> ( ( W gsum ( k e. ( 0 ... ( # ` J ) ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` k ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( ( ( # ` J ) - k ) ( .g ` M ) X ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) = ( ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) ) |
| 514 |
46
|
adantr |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> R e. Ring ) |
| 515 |
514 151
|
syl |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( mulGrp ` R ) e. Mnd ) |
| 516 |
|
fz1ssfz0 |
|- ( 1 ... ( # ` J ) ) C_ ( 0 ... ( # ` J ) ) |
| 517 |
516 110
|
sstri |
|- ( 1 ... ( # ` J ) ) C_ NN0 |
| 518 |
517
|
a1i |
|- ( ph -> ( 1 ... ( # ` J ) ) C_ NN0 ) |
| 519 |
518
|
sselda |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> l e. NN0 ) |
| 520 |
158
|
adantr |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( N ` .1. ) e. B ) |
| 521 |
150 12 515 519 520
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( l .^ ( N ` .1. ) ) e. B ) |
| 522 |
14
|
adantr |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> I e. Fin ) |
| 523 |
35
|
adantr |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> R e. CRing ) |
| 524 |
6
|
fveq1i |
|- ( E ` l ) = ( ( I eSymPoly R ) ` l ) |
| 525 |
257 522 514 519 255
|
esplympl |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( ( I eSymPoly R ) ` l ) e. ( Base ` ( I mPoly R ) ) ) |
| 526 |
524 525
|
eqeltrid |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( E ` l ) e. ( Base ` ( I mPoly R ) ) ) |
| 527 |
260
|
adantr |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> Z e. ( B ^m I ) ) |
| 528 |
5 254 255 2 522 523 526 527
|
evlcl |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( ( Q ` ( E ` l ) ) ` Z ) e. B ) |
| 529 |
2 9 514 521 528
|
ringcld |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) e. B ) |
| 530 |
117
|
adantr |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> M e. Mnd ) |
| 531 |
|
fzssp1 |
|- ( 0 ... ( # ` J ) ) C_ ( 0 ... ( ( # ` J ) + 1 ) ) |
| 532 |
297
|
oveq2d |
|- ( ph -> ( 0 ... H ) = ( 0 ... ( ( # ` J ) + 1 ) ) ) |
| 533 |
531 532
|
sseqtrrid |
|- ( ph -> ( 0 ... ( # ` J ) ) C_ ( 0 ... H ) ) |
| 534 |
516 533
|
sstrid |
|- ( ph -> ( 1 ... ( # ` J ) ) C_ ( 0 ... H ) ) |
| 535 |
534
|
sselda |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> l e. ( 0 ... H ) ) |
| 536 |
|
fznn0sub2 |
|- ( l e. ( 0 ... H ) -> ( H - l ) e. ( 0 ... H ) ) |
| 537 |
535 536
|
syl |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( H - l ) e. ( 0 ... H ) ) |
| 538 |
414 537
|
sselid |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( H - l ) e. NN0 ) |
| 539 |
514 47
|
syl |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> X e. ( Base ` W ) ) |
| 540 |
32 81 530 538 539
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( ( H - l ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 541 |
1 31 2 80 514 529 540
|
ply1vscl |
|- ( ( ph /\ l e. ( 1 ... ( # ` J ) ) ) -> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 542 |
|
oveq1 |
|- ( l = ( k + 1 ) -> ( l .^ ( N ` .1. ) ) = ( ( k + 1 ) .^ ( N ` .1. ) ) ) |
| 543 |
|
2fveq3 |
|- ( l = ( k + 1 ) -> ( Q ` ( E ` l ) ) = ( Q ` ( E ` ( k + 1 ) ) ) ) |
| 544 |
543
|
fveq1d |
|- ( l = ( k + 1 ) -> ( ( Q ` ( E ` l ) ) ` Z ) = ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) |
| 545 |
542 544
|
oveq12d |
|- ( l = ( k + 1 ) -> ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) = ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ) |
| 546 |
|
oveq2 |
|- ( l = ( k + 1 ) -> ( H - l ) = ( H - ( k + 1 ) ) ) |
| 547 |
546
|
oveq1d |
|- ( l = ( k + 1 ) -> ( ( H - l ) ( .g ` M ) X ) = ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) |
| 548 |
545 547
|
oveq12d |
|- ( l = ( k + 1 ) -> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) |
| 549 |
548
|
adantl |
|- ( ( ( ph /\ k e. ( 0 ..^ ( # ` J ) ) ) /\ l = ( k + 1 ) ) -> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) = ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) |
| 550 |
31 98 100 541 549
|
gsummptp1 |
|- ( ph -> ( W gsum ( k e. ( 0 ..^ ( # ` J ) ) |-> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) |
| 551 |
550
|
oveq1d |
|- ( ph -> ( ( W gsum ( k e. ( 0 ..^ ( # ` J ) ) |-> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) = ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) ) |
| 552 |
|
oveq1 |
|- ( k = l -> ( k .^ ( N ` .1. ) ) = ( l .^ ( N ` .1. ) ) ) |
| 553 |
|
2fveq3 |
|- ( k = l -> ( Q ` ( E ` k ) ) = ( Q ` ( E ` l ) ) ) |
| 554 |
553
|
fveq1d |
|- ( k = l -> ( ( Q ` ( E ` k ) ) ` Z ) = ( ( Q ` ( E ` l ) ) ` Z ) ) |
| 555 |
552 554
|
oveq12d |
|- ( k = l -> ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) = ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ) |
| 556 |
|
oveq2 |
|- ( k = l -> ( H - k ) = ( H - l ) ) |
| 557 |
556
|
oveq1d |
|- ( k = l -> ( ( H - k ) ( .g ` M ) X ) = ( ( H - l ) ( .g ` M ) X ) ) |
| 558 |
555 557
|
oveq12d |
|- ( k = l -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) = ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) |
| 559 |
558
|
cbvmptv |
|- ( k e. ( 0 ... H ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) ) = ( l e. ( 0 ... H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) |
| 560 |
559
|
a1i |
|- ( ph -> ( k e. ( 0 ... H ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) ) = ( l e. ( 0 ... H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) |
| 561 |
560
|
oveq2d |
|- ( ph -> ( W gsum ( k e. ( 0 ... H ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) |
| 562 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
| 563 |
250 562
|
eleqtrdi |
|- ( ph -> H e. ( ZZ>= ` 0 ) ) |
| 564 |
46
|
adantr |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> R e. Ring ) |
| 565 |
564 151
|
syl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( mulGrp ` R ) e. Mnd ) |
| 566 |
414
|
a1i |
|- ( ph -> ( 0 ... H ) C_ NN0 ) |
| 567 |
566
|
sselda |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> l e. NN0 ) |
| 568 |
158
|
adantr |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( N ` .1. ) e. B ) |
| 569 |
150 12 565 567 568
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( l .^ ( N ` .1. ) ) e. B ) |
| 570 |
14
|
adantr |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> I e. Fin ) |
| 571 |
35
|
adantr |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> R e. CRing ) |
| 572 |
257 570 564 567 255
|
esplympl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( I eSymPoly R ) ` l ) e. ( Base ` ( I mPoly R ) ) ) |
| 573 |
524 572
|
eqeltrid |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( E ` l ) e. ( Base ` ( I mPoly R ) ) ) |
| 574 |
260
|
adantr |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> Z e. ( B ^m I ) ) |
| 575 |
5 254 255 2 570 571 573 574
|
evlcl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( Q ` ( E ` l ) ) ` Z ) e. B ) |
| 576 |
2 9 564 569 575
|
ringcld |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) e. B ) |
| 577 |
117
|
adantr |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> M e. Mnd ) |
| 578 |
|
fznn0sub |
|- ( l e. ( 0 ... H ) -> ( H - l ) e. NN0 ) |
| 579 |
578
|
adantl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( H - l ) e. NN0 ) |
| 580 |
564 47
|
syl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> X e. ( Base ` W ) ) |
| 581 |
32 81 577 579 580
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( H - l ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 582 |
1 31 2 80 564 576 581
|
ply1vscl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 583 |
|
oveq1 |
|- ( l = H -> ( l .^ ( N ` .1. ) ) = ( H .^ ( N ` .1. ) ) ) |
| 584 |
|
2fveq3 |
|- ( l = H -> ( Q ` ( E ` l ) ) = ( Q ` ( E ` H ) ) ) |
| 585 |
584
|
fveq1d |
|- ( l = H -> ( ( Q ` ( E ` l ) ) ` Z ) = ( ( Q ` ( E ` H ) ) ` Z ) ) |
| 586 |
583 585
|
oveq12d |
|- ( l = H -> ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) = ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) |
| 587 |
586
|
adantl |
|- ( ( ph /\ l = H ) -> ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) = ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ) |
| 588 |
|
oveq2 |
|- ( l = H -> ( H - l ) = ( H - H ) ) |
| 589 |
294
|
subidd |
|- ( ph -> ( H - H ) = 0 ) |
| 590 |
588 589
|
sylan9eqr |
|- ( ( ph /\ l = H ) -> ( H - l ) = 0 ) |
| 591 |
590
|
oveq1d |
|- ( ( ph /\ l = H ) -> ( ( H - l ) ( .g ` M ) X ) = ( 0 ( .g ` M ) X ) ) |
| 592 |
587 591
|
oveq12d |
|- ( ( ph /\ l = H ) -> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) = ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) |
| 593 |
31 193 98 563 582 592
|
gsummptfzsplitra |
|- ( ph -> ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) = ( ( W gsum ( l e. ( 0 ..^ H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) |
| 594 |
100
|
nn0zd |
|- ( ph -> ( # ` J ) e. ZZ ) |
| 595 |
|
fzval3 |
|- ( ( # ` J ) e. ZZ -> ( 0 ... ( # ` J ) ) = ( 0 ..^ ( ( # ` J ) + 1 ) ) ) |
| 596 |
594 595
|
syl |
|- ( ph -> ( 0 ... ( # ` J ) ) = ( 0 ..^ ( ( # ` J ) + 1 ) ) ) |
| 597 |
297
|
oveq2d |
|- ( ph -> ( 0 ..^ H ) = ( 0 ..^ ( ( # ` J ) + 1 ) ) ) |
| 598 |
596 597
|
eqtr4d |
|- ( ph -> ( 0 ... ( # ` J ) ) = ( 0 ..^ H ) ) |
| 599 |
598
|
mpteq1d |
|- ( ph -> ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) = ( l e. ( 0 ..^ H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) |
| 600 |
599
|
oveq2d |
|- ( ph -> ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 0 ..^ H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) |
| 601 |
100 562
|
eleqtrdi |
|- ( ph -> ( # ` J ) e. ( ZZ>= ` 0 ) ) |
| 602 |
150 12 152 112 159
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( l .^ ( N ` .1. ) ) e. B ) |
| 603 |
14
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> I e. Fin ) |
| 604 |
257 603 119 112 255
|
esplympl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( I eSymPoly R ) ` l ) e. ( Base ` ( I mPoly R ) ) ) |
| 605 |
524 604
|
eqeltrid |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( E ` l ) e. ( Base ` ( I mPoly R ) ) ) |
| 606 |
260
|
adantr |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> Z e. ( B ^m I ) ) |
| 607 |
5 254 255 2 603 165 605 606
|
evlcl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( Q ` ( E ` l ) ) ` Z ) e. B ) |
| 608 |
2 9 119 602 607
|
ringcld |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) e. B ) |
| 609 |
533
|
sselda |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> l e. ( 0 ... H ) ) |
| 610 |
609 536
|
syl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( H - l ) e. ( 0 ... H ) ) |
| 611 |
414 610
|
sselid |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( H - l ) e. NN0 ) |
| 612 |
32 81 118 611 120
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( H - l ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 613 |
1 31 2 80 119 608 612
|
ply1vscl |
|- ( ( ph /\ l e. ( 0 ... ( # ` J ) ) ) -> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 614 |
|
oveq1 |
|- ( l = 0 -> ( l .^ ( N ` .1. ) ) = ( 0 .^ ( N ` .1. ) ) ) |
| 615 |
614
|
adantl |
|- ( ( ph /\ l = 0 ) -> ( l .^ ( N ` .1. ) ) = ( 0 .^ ( N ` .1. ) ) ) |
| 616 |
|
2fveq3 |
|- ( l = 0 -> ( Q ` ( E ` l ) ) = ( Q ` ( E ` 0 ) ) ) |
| 617 |
616
|
fveq1d |
|- ( l = 0 -> ( ( Q ` ( E ` l ) ) ` Z ) = ( ( Q ` ( E ` 0 ) ) ` Z ) ) |
| 618 |
617
|
adantl |
|- ( ( ph /\ l = 0 ) -> ( ( Q ` ( E ` l ) ) ` Z ) = ( ( Q ` ( E ` 0 ) ) ` Z ) ) |
| 619 |
|
eqid |
|- ( 1r ` ( I mPoly R ) ) = ( 1r ` ( I mPoly R ) ) |
| 620 |
14 46 619
|
esplyfval0 |
|- ( ph -> ( ( I eSymPoly R ) ` 0 ) = ( 1r ` ( I mPoly R ) ) ) |
| 621 |
6
|
fveq1i |
|- ( E ` 0 ) = ( ( I eSymPoly R ) ` 0 ) |
| 622 |
621
|
a1i |
|- ( ph -> ( E ` 0 ) = ( ( I eSymPoly R ) ` 0 ) ) |
| 623 |
|
eqid |
|- ( algSc ` ( I mPoly R ) ) = ( algSc ` ( I mPoly R ) ) |
| 624 |
254 623 278 619 14 46
|
mplascl1 |
|- ( ph -> ( ( algSc ` ( I mPoly R ) ) ` ( 1r ` R ) ) = ( 1r ` ( I mPoly R ) ) ) |
| 625 |
620 622 624
|
3eqtr4d |
|- ( ph -> ( E ` 0 ) = ( ( algSc ` ( I mPoly R ) ) ` ( 1r ` R ) ) ) |
| 626 |
625
|
fveq2d |
|- ( ph -> ( Q ` ( E ` 0 ) ) = ( Q ` ( ( algSc ` ( I mPoly R ) ) ` ( 1r ` R ) ) ) ) |
| 627 |
626
|
fveq1d |
|- ( ph -> ( ( Q ` ( E ` 0 ) ) ` Z ) = ( ( Q ` ( ( algSc ` ( I mPoly R ) ) ` ( 1r ` R ) ) ) ` Z ) ) |
| 628 |
627
|
adantr |
|- ( ( ph /\ l = 0 ) -> ( ( Q ` ( E ` 0 ) ) ` Z ) = ( ( Q ` ( ( algSc ` ( I mPoly R ) ) ` ( 1r ` R ) ) ) ` Z ) ) |
| 629 |
5 254 2 623 14 35 246 16
|
evlscaval |
|- ( ph -> ( ( Q ` ( ( algSc ` ( I mPoly R ) ) ` ( 1r ` R ) ) ) ` Z ) = ( 1r ` R ) ) |
| 630 |
629
|
adantr |
|- ( ( ph /\ l = 0 ) -> ( ( Q ` ( ( algSc ` ( I mPoly R ) ) ` ( 1r ` R ) ) ) ` Z ) = ( 1r ` R ) ) |
| 631 |
618 628 630
|
3eqtrd |
|- ( ( ph /\ l = 0 ) -> ( ( Q ` ( E ` l ) ) ` Z ) = ( 1r ` R ) ) |
| 632 |
615 631
|
oveq12d |
|- ( ( ph /\ l = 0 ) -> ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) = ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ) |
| 633 |
|
oveq2 |
|- ( l = 0 -> ( H - l ) = ( H - 0 ) ) |
| 634 |
633
|
adantl |
|- ( ( ph /\ l = 0 ) -> ( H - l ) = ( H - 0 ) ) |
| 635 |
294
|
adantr |
|- ( ( ph /\ l = 0 ) -> H e. CC ) |
| 636 |
635
|
subid1d |
|- ( ( ph /\ l = 0 ) -> ( H - 0 ) = H ) |
| 637 |
634 636
|
eqtrd |
|- ( ( ph /\ l = 0 ) -> ( H - l ) = H ) |
| 638 |
637
|
oveq1d |
|- ( ( ph /\ l = 0 ) -> ( ( H - l ) ( .g ` M ) X ) = ( H ( .g ` M ) X ) ) |
| 639 |
632 638
|
oveq12d |
|- ( ( ph /\ l = 0 ) -> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) = ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) |
| 640 |
31 193 98 601 613 639
|
gsummptfzsplitla |
|- ( ph -> ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) = ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( W gsum ( l e. ( ( 0 + 1 ) ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) ) |
| 641 |
|
0p1e1 |
|- ( 0 + 1 ) = 1 |
| 642 |
641
|
oveq1i |
|- ( ( 0 + 1 ) ... ( # ` J ) ) = ( 1 ... ( # ` J ) ) |
| 643 |
642
|
mpteq1i |
|- ( l e. ( ( 0 + 1 ) ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) = ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) |
| 644 |
643
|
oveq2i |
|- ( W gsum ( l e. ( ( 0 + 1 ) ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) |
| 645 |
644
|
oveq2i |
|- ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( W gsum ( l e. ( ( 0 + 1 ) ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) = ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) |
| 646 |
645
|
a1i |
|- ( ph -> ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( W gsum ( l e. ( ( 0 + 1 ) ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) = ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) ) |
| 647 |
43
|
ringabld |
|- ( ph -> W e. Abel ) |
| 648 |
|
fzfid |
|- ( ph -> ( 1 ... ( # ` J ) ) e. Fin ) |
| 649 |
541
|
ralrimiva |
|- ( ph -> A. l e. ( 1 ... ( # ` J ) ) ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 650 |
31 98 648 649
|
gsummptcl |
|- ( ph -> ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) e. ( Base ` W ) ) |
| 651 |
31 193 647 252 650
|
ablcomd |
|- ( ph -> ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) = ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) ) |
| 652 |
640 646 651
|
3eqtrd |
|- ( ph -> ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) = ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) ) |
| 653 |
600 652
|
eqtr3d |
|- ( ph -> ( W gsum ( l e. ( 0 ..^ H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) = ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) ) |
| 654 |
653
|
oveq1d |
|- ( ph -> ( ( W gsum ( l e. ( 0 ..^ H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) = ( ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) |
| 655 |
593 654
|
eqtr2d |
|- ( ph -> ( ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) = ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ) |
| 656 |
31 193 44 650 252 264
|
grpassd |
|- ( ph -> ( ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) = ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) ) |
| 657 |
561 655 656
|
3eqtr2rd |
|- ( ph -> ( ( W gsum ( l e. ( 1 ... ( # ` J ) ) |-> ( ( ( l .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` l ) ) ` Z ) ) ( .s ` W ) ( ( H - l ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) = ( W gsum ( k e. ( 0 ... H ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) ) ) ) |
| 658 |
46
|
adantr |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> R e. Ring ) |
| 659 |
658 151
|
syl |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( mulGrp ` R ) e. Mnd ) |
| 660 |
566
|
sselda |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> k e. NN0 ) |
| 661 |
158
|
adantr |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( N ` .1. ) e. B ) |
| 662 |
150 12 659 660 661
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( k .^ ( N ` .1. ) ) e. B ) |
| 663 |
14
|
adantr |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> I e. Fin ) |
| 664 |
35
|
adantr |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> R e. CRing ) |
| 665 |
6
|
fveq1i |
|- ( E ` k ) = ( ( I eSymPoly R ) ` k ) |
| 666 |
257 663 658 660 255
|
esplympl |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( ( I eSymPoly R ) ` k ) e. ( Base ` ( I mPoly R ) ) ) |
| 667 |
665 666
|
eqeltrid |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( E ` k ) e. ( Base ` ( I mPoly R ) ) ) |
| 668 |
260
|
adantr |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> Z e. ( B ^m I ) ) |
| 669 |
5 254 255 2 663 664 667 668
|
evlcl |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( ( Q ` ( E ` k ) ) ` Z ) e. B ) |
| 670 |
2 9 658 662 669
|
ringcld |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) e. B ) |
| 671 |
117
|
adantr |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> M e. Mnd ) |
| 672 |
|
fznn0sub2 |
|- ( k e. ( 0 ... H ) -> ( H - k ) e. ( 0 ... H ) ) |
| 673 |
672
|
adantl |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( H - k ) e. ( 0 ... H ) ) |
| 674 |
414 673
|
sselid |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( H - k ) e. NN0 ) |
| 675 |
48
|
adantr |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> X e. ( Base ` W ) ) |
| 676 |
32 81 671 674 675
|
mulgnn0cld |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( ( H - k ) ( .g ` M ) X ) e. ( Base ` W ) ) |
| 677 |
1 31 2 80 658 670 676
|
ply1vscl |
|- ( ( ph /\ k e. ( 0 ... H ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) e. ( Base ` W ) ) |
| 678 |
|
oveq1 |
|- ( k = ( H - l ) -> ( k .^ ( N ` .1. ) ) = ( ( H - l ) .^ ( N ` .1. ) ) ) |
| 679 |
|
2fveq3 |
|- ( k = ( H - l ) -> ( Q ` ( E ` k ) ) = ( Q ` ( E ` ( H - l ) ) ) ) |
| 680 |
679
|
fveq1d |
|- ( k = ( H - l ) -> ( ( Q ` ( E ` k ) ) ` Z ) = ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) |
| 681 |
678 680
|
oveq12d |
|- ( k = ( H - l ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) = ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ) |
| 682 |
681
|
adantl |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) = ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ) |
| 683 |
|
simpr |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> k = ( H - l ) ) |
| 684 |
683
|
oveq2d |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> ( H - k ) = ( H - ( H - l ) ) ) |
| 685 |
294
|
ad2antrr |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> H e. CC ) |
| 686 |
567
|
adantr |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> l e. NN0 ) |
| 687 |
686
|
nn0cnd |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> l e. CC ) |
| 688 |
685 687
|
nncand |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> ( H - ( H - l ) ) = l ) |
| 689 |
684 688
|
eqtrd |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> ( H - k ) = l ) |
| 690 |
689
|
oveq1d |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> ( ( H - k ) ( .g ` M ) X ) = ( l ( .g ` M ) X ) ) |
| 691 |
682 690
|
oveq12d |
|- ( ( ( ph /\ l e. ( 0 ... H ) ) /\ k = ( H - l ) ) -> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) = ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) |
| 692 |
31 98 250 677 691
|
gsummptrev |
|- ( ph -> ( W gsum ( k e. ( 0 ... H ) |-> ( ( ( k .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` k ) ) ` Z ) ) ( .s ` W ) ( ( H - k ) ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 693 |
551 657 692
|
3eqtrd |
|- ( ph -> ( ( W gsum ( k e. ( 0 ..^ ( # ` J ) ) |-> ( ( ( ( k + 1 ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( k + 1 ) ) ) ` Z ) ) ( .s ` W ) ( ( H - ( k + 1 ) ) ( .g ` M ) X ) ) ) ) ( +g ` W ) ( ( ( ( 0 .^ ( N ` .1. ) ) .x. ( 1r ` R ) ) ( .s ` W ) ( H ( .g ` M ) X ) ) ( +g ` W ) ( ( ( H .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` H ) ) ` Z ) ) ( .s ` W ) ( 0 ( .g ` M ) X ) ) ) ) = ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 694 |
479 513 693
|
3eqtr3d |
|- ( ph -> ( ( W gsum ( l e. ( 0 ... ( # ` J ) ) |-> ( ( ( ( ( # ` J ) - l ) .^ ( N ` .1. ) ) .x. ( ( ( J eval R ) ` ( ( J eSymPoly R ) ` ( ( # ` J ) - l ) ) ) ` ( Z |` J ) ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ( .r ` W ) ( X .- ( A ` ( Z ` Y ) ) ) ) = ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 695 |
79 192 694
|
3eqtrd |
|- ( ph -> F = ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) |
| 696 |
695
|
fveq2d |
|- ( ph -> ( coe1 ` F ) = ( coe1 ` ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) ) |
| 697 |
696
|
fveq1d |
|- ( ph -> ( ( coe1 ` F ) ` K ) = ( ( coe1 ` ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) ` K ) ) |
| 698 |
4
|
fveq2i |
|- ( .g ` M ) = ( .g ` ( mulGrp ` W ) ) |
| 699 |
150 12 565 579 568
|
mulgnn0cld |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( H - l ) .^ ( N ` .1. ) ) e. B ) |
| 700 |
6
|
fveq1i |
|- ( E ` ( H - l ) ) = ( ( I eSymPoly R ) ` ( H - l ) ) |
| 701 |
257 570 564 579 255
|
esplympl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( I eSymPoly R ) ` ( H - l ) ) e. ( Base ` ( I mPoly R ) ) ) |
| 702 |
700 701
|
eqeltrid |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( E ` ( H - l ) ) e. ( Base ` ( I mPoly R ) ) ) |
| 703 |
5 254 255 2 570 571 702 574
|
evlcl |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) e. B ) |
| 704 |
2 9 564 699 703
|
ringcld |
|- ( ( ph /\ l e. ( 0 ... H ) ) -> ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) e. B ) |
| 705 |
704
|
ralrimiva |
|- ( ph -> A. l e. ( 0 ... H ) ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) e. B ) |
| 706 |
|
oveq2 |
|- ( l = K -> ( H - l ) = ( H - K ) ) |
| 707 |
706
|
oveq1d |
|- ( l = K -> ( ( H - l ) .^ ( N ` .1. ) ) = ( ( H - K ) .^ ( N ` .1. ) ) ) |
| 708 |
706
|
fveq2d |
|- ( l = K -> ( E ` ( H - l ) ) = ( E ` ( H - K ) ) ) |
| 709 |
708
|
fveq2d |
|- ( l = K -> ( Q ` ( E ` ( H - l ) ) ) = ( Q ` ( E ` ( H - K ) ) ) ) |
| 710 |
709
|
fveq1d |
|- ( l = K -> ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) = ( ( Q ` ( E ` ( H - K ) ) ) ` Z ) ) |
| 711 |
707 710
|
oveq12d |
|- ( l = K -> ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) = ( ( ( H - K ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - K ) ) ) ` Z ) ) ) |
| 712 |
1 31 10 698 46 2 80 250 705 18 711
|
gsummoncoe1fz |
|- ( ph -> ( ( coe1 ` ( W gsum ( l e. ( 0 ... H ) |-> ( ( ( ( H - l ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - l ) ) ) ` Z ) ) ( .s ` W ) ( l ( .g ` M ) X ) ) ) ) ) ` K ) = ( ( ( H - K ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - K ) ) ) ` Z ) ) ) |
| 713 |
697 712
|
eqtrd |
|- ( ph -> ( ( coe1 ` F ) ` K ) = ( ( ( H - K ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - K ) ) ) ` Z ) ) ) |