Theorem vieta

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

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