Theorem vietalem

Description: Lemma for vieta : induction step. (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	vieta.w	|- W = ( Poly1 ` R )
	vieta.b	|- B = ( Base ` R )
	vieta.3	|- .- = ( -g ` W )
	vieta.m	|- M = ( mulGrp ` W )
	vieta.q	|- Q = ( I eval R )
	vieta.e	|- E = ( I eSymPoly R )
	vieta.n	|- N = ( invg ` R )
	vieta.1	|- .1. = ( 1r ` R )
	vieta.t	|- .x. = ( .r ` R )
	vieta.x	|- X = ( var1 ` R )
	vieta.a	|- A = ( algSc ` W )
	vieta.p	|- .^ = ( .g ` ( mulGrp ` R ) )
	vieta.h	|- H = ( # ` I )
	vieta.i	|- ( ph -> I e. Fin )
	vieta.r	|- ( ph -> R e. IDomn )
	vieta.z	|- ( ph -> Z : I --> B )
	vieta.f	|- F = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) )
	vieta.k	|- ( ph -> K e. ( 0 ... H ) )
	vietalem.y	|- ( ph -> Y e. I )
	vietalem.j	|- J = ( I \ { Y } )
	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 ) ) )
	vietalem.3	|- ( ph -> ( ( deg1 ` R ) ` ( M gsum ( n e. J |-> ( X .- ( A ` ( ( Z |` J ) ` n ) ) ) ) ) ) = ( # ` J ) )
Assertion	vietalem	|- ( ph -> ( ( coe1 ` F ) ` K ) = ( ( ( H - K ) .^ ( N ` .1. ) ) .x. ( ( Q ` ( E ` ( H - K ) ) ) ` Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		vieta.w	|- W = ( Poly1 ` R )
2		vieta.b	|- B = ( Base ` R )
3		vieta.3	|- .- = ( -g ` W )
4		vieta.m	|- M = ( mulGrp ` W )
5		vieta.q	|- Q = ( I eval R )
6		vieta.e	|- E = ( I eSymPoly R )
7		vieta.n	|- N = ( invg ` R )
8		vieta.1	|- .1. = ( 1r ` R )
9		vieta.t	|- .x. = ( .r ` R )
10		vieta.x	|- X = ( var1 ` R )
11		vieta.a	|- A = ( algSc ` W )
12		vieta.p	|- .^ = ( .g ` ( mulGrp ` R ) )
13		vieta.h	|- H = ( # ` I )
14		vieta.i	|- ( ph -> I e. Fin )
15		vieta.r	|- ( ph -> R e. IDomn )
16		vieta.z	|- ( ph -> Z : I --> B )
17		vieta.f	|- F = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) )
18		vieta.k	|- ( ph -> K e. ( 0 ... H ) )
19		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 ) ) )