Theorem vietalem

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

	Ref	Expression
Hypotheses	vieta.w	$$⊢W={\mathrm{Poly}}_1\left(R\right)$$
	vieta.b	$$⊢B={\mathrm{Base}}_R$$
	vieta.3	$$⊢\underset{\dot{}}{-}={-}_W$$
	vieta.m	$$⊢M={\mathrm{mulGrp}}_W$$
	vieta.q	$$⊢Q=I\mathrm{eval}R$$
	vieta.e	No typesetting found for |- E = ( I eSymPoly R ) with typecode |-
	vieta.n	$$⊢N={inv}_g\left(R\right)$$
	vieta.1	$$⊢\underset{\dot{}}{1}=1_R$$
	vieta.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	vieta.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	vieta.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	vieta.p	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	vieta.h	$$⊢H=\left|I\right|$$
	vieta.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	vieta.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
	vieta.z	$$⊢\phi \to Z:I⟶B$$
	vieta.f	$$⊢F=\underset{n\in I}{{\sum }_M}\left(X\underset{\dot{}}{-}A\left(Z\left(n\right)\right)\right)$$
	vieta.k	$$⊢\phi \to K\in \left(0\dots H\right)$$
	vietalem.y	$$⊢\phi \to Y\in I$$
	vietalem.j	$$⊢J=I\setminus \left\{Y\right\}$$
	vietalem.2	No typesetting found for |- ( 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 ) ) ) with typecode |-
	vietalem.3	$$⊢\phi \to {\mathrm{deg}}_1\left(R\right)\left(\underset{n\in J}{{\sum }_M}\left(X\underset{\dot{}}{-}A\left(\left({Z\upharpoonright }_J\right)\left(n\right)\right)\right)\right)=\left|J\right|$$
Assertion	vietalem	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(K\right)=\left(\left(H-K\right)\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)\right)\underset{\dot{}}{·}Q\left(E\left(H-K\right)\right)\left(Z\right)$$

Proof

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