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	biimpi	$$⊢f=\varnothing \to f=\varnothing \times \left\{0\right\}$$
151	150	adantl	$$⊢\left(\phi \wedge f=\varnothing \right)\to f=\varnothing \times \left\{0\right\}$$
152	151	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}$$
153	152 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)$$
154	140 146 153	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)$$
155		elsni	$$⊢h\in \left\{\varnothing \right\}\to h=\varnothing$$
156		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
157		mapdm0	$$⊢{\mathbb{N}}_0\in \mathrm{V}\to {{\mathbb{N}}_0}^{\varnothing }=\left\{\varnothing \right\}$$
158	156 157	ax-mp	$$⊢{{\mathbb{N}}_0}^{\varnothing }=\left\{\varnothing \right\}$$
159	155 158	eleq2s	$$⊢h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\to h=\varnothing$$
160	159	cnveqd	$$⊢h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\to h^{-1}={\varnothing }^{-1}$$
161	160	imaeq1d	$$⊢h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\to h^{-1}\left[\mathbb{N}\right]={\varnothing }^{-1}\left[\mathbb{N}\right]$$
162		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
163	162	imaeq1i	$$⊢{\varnothing }^{-1}\left[\mathbb{N}\right]=\varnothing \left[\mathbb{N}\right]$$
164		0ima	$$⊢\varnothing \left[\mathbb{N}\right]=\varnothing$$
165	163 164	eqtri	$$⊢{\varnothing }^{-1}\left[\mathbb{N}\right]=\varnothing$$
166	161 165	eqtrdi	$$⊢h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\to h^{-1}\left[\mathbb{N}\right]=\varnothing$$
167		0fi	$$⊢\varnothing \in \mathrm{Fin}$$
168	166 167	eqeltrdi	$$⊢h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)\to h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
169	168	rabeqc	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}={{\mathbb{N}}_0}^{\varnothing }$$
170	169 158	eqtr2i	$$⊢\left\{\varnothing \right\}=\left\{h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
171		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\}$$
172	171	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\}$$
173	170 172	eqtr4i	$$⊢\left\{\varnothing \right\}=\left\{h\in \left({{\mathbb{N}}_0}^{\varnothing }\right)|{finSupp}_0\left(h\right)\right\}$$
174		0nn0	$$⊢0\in {\mathbb{N}}_0$$
175	174	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
176	173 142 15 175	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 |-
177		fveqeq2	$$⊢c=\varnothing \to \left(\left|c\right|=0\leftrightarrow \left|\varnothing \right|=0\right)$$
178		0elpw	$$⊢\varnothing \in 𝒫\varnothing$$
179	178	a1i	$$⊢\phi \to \varnothing \in 𝒫\varnothing$$
180	46	a1i	$$⊢\phi \to \left|\varnothing \right|=0$$
181		hasheq0	$$⊢c\in 𝒫\varnothing \to \left(\left|c\right|=0\leftrightarrow c=\varnothing \right)$$
182	181	biimpa	$$⊢\left(c\in 𝒫\varnothing \wedge \left|c\right|=0\right)\to c=\varnothing$$
183	182	adantll	$$⊢\left(\left(\phi \wedge c\in 𝒫\varnothing \right)\wedge \left|c\right|=0\right)\to c=\varnothing$$
184	177 179 180 183	rabeqsnd	$$⊢\phi \to \left\{c\in 𝒫\varnothing |\left|c\right|=0\right\}=\left\{\varnothing \right\}$$
185	184	imaeq2d	$$⊢\phi \to {𝟙}_{\varnothing }\left[\left\{c\in 𝒫\varnothing |\left|c\right|=0\right\}\right]={𝟙}_{\varnothing }\left[\left\{\varnothing \right\}\right]$$
186		pw0	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$
187	186	a1i	$$⊢\phi \to 𝒫\varnothing =\left\{\varnothing \right\}$$
188		indf1o	$$⊢\varnothing \in \mathrm{V}\to {𝟙}_{\varnothing }:𝒫\varnothing \underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^{\varnothing }$$
189		f1of	$$⊢{𝟙}_{\varnothing }:𝒫\varnothing \underset{1-1\; onto}{⟶}{\left\{0,1\right\}}^{\varnothing }\to {𝟙}_{\varnothing }:𝒫\varnothing ⟶{\left\{0,1\right\}}^{\varnothing }$$
190	142 188 189	3syl	$$⊢\phi \to {𝟙}_{\varnothing }:𝒫\varnothing ⟶{\left\{0,1\right\}}^{\varnothing }$$
191	187 190	feq2dd	$$⊢\phi \to {𝟙}_{\varnothing }:\left\{\varnothing \right\}⟶{\left\{0,1\right\}}^{\varnothing }$$
192	191	ffnd	$$⊢\phi \to {𝟙}_{\varnothing }Fn\left\{\varnothing \right\}$$
193	141	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
194	193	a1i	$$⊢\phi \to \varnothing \in \left\{\varnothing \right\}$$
195	192 194	fnimasnd	$$⊢\phi \to {𝟙}_{\varnothing }\left[\left\{\varnothing \right\}\right]=\left\{{𝟙}_{\varnothing }\left(\varnothing \right)\right\}$$
196		ssidd	$$⊢\phi \to \varnothing \subseteq \varnothing$$
197		indf	$$⊢\left(\varnothing \in \mathrm{V}\wedge \varnothing \subseteq \varnothing \right)\to {𝟙}_{\varnothing }\left(\varnothing \right):\varnothing ⟶\left\{0,1\right\}$$
198	142 196 197	syl2anc	$$⊢\phi \to {𝟙}_{\varnothing }\left(\varnothing \right):\varnothing ⟶\left\{0,1\right\}$$
199		f0bi	$$⊢{𝟙}_{\varnothing }\left(\varnothing \right):\varnothing ⟶\left\{0,1\right\}\leftrightarrow {𝟙}_{\varnothing }\left(\varnothing \right)=\varnothing$$
200	198 199	sylib	$$⊢\phi \to {𝟙}_{\varnothing }\left(\varnothing \right)=\varnothing$$
201	200	sneqd	$$⊢\phi \to \left\{{𝟙}_{\varnothing }\left(\varnothing \right)\right\}=\left\{\varnothing \right\}$$
202	185 195 201	3eqtrd	$$⊢\phi \to {𝟙}_{\varnothing }\left[\left\{c\in 𝒫\varnothing |\left|c\right|=0\right\}\right]=\left\{\varnothing \right\}$$
203	202	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)$$
204		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
205		indconst1	$$⊢\left\{\varnothing \right\}\in \mathrm{V}\to {𝟙}_{\left\{\varnothing \right\}}\left(\left\{\varnothing \right\}\right)=\left\{\varnothing \right\}\times \left\{1\right\}$$
206	204 205	ax-mp	$$⊢{𝟙}_{\left\{\varnothing \right\}}\left(\left\{\varnothing \right\}\right)=\left\{\varnothing \right\}\times \left\{1\right\}$$
207	203 206	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\}$$
208	207	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)$$
209	136	zrhrhm	$$⊢R\in \mathrm{Ring}\to \mathrm{\mathbb{Z}RHom}\left(R\right)\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
210		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
211	210 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$$
212	126 209 211	3syl	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right):\mathbb{Z}⟶B$$
213	212	ffnd	$$⊢\phi \to \mathrm{\mathbb{Z}RHom}\left(R\right)Fn\mathbb{Z}$$
214		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
215		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\}$$
216	213 214 215	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\}$$
217	176 208 216	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 |-
218		eqid	$$⊢\varnothing \mathrm{mPoly}R=\varnothing \mathrm{mPoly}R$$
219		eqid	$$⊢0_R=0_R$$
220		eqid	$$⊢\mathrm{algSc}\left(\varnothing \mathrm{mPoly}R\right)=\mathrm{algSc}\left(\varnothing \mathrm{mPoly}R\right)$$
221	218 170 219 2 220 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)$$
222	154 217 221	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 |-
223	222	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 |-
224	223	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 |-
225		eqid	$$⊢\varnothing \mathrm{eval}R=\varnothing \mathrm{eval}R$$
226	193 158	eleqtrri	$$⊢\varnothing \in \left({{\mathbb{N}}_0}^{\varnothing }\right)$$
227	226	a1i	$$⊢\phi \to \varnothing \in \left({{\mathbb{N}}_0}^{\varnothing }\right)$$
228	15	idomcringd	$$⊢\phi \to R\in \mathrm{CRing}$$
229	225 218 2 220 227 228 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\}$$
230	229	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)$$
231	193 42	eleqtrri	$$⊢\varnothing \in \left(B^{\varnothing }\right)$$
232	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}$$
233	231 232	mp1i	$$⊢\phi \to \left(\left(B^{\varnothing }\right)\times \left\{\underset{\dot{}}{1}\right\}\right)\left(\varnothing \right)=\underset{\dot{}}{1}$$
234	224 230 233	3eqtrd	Could not format ( ph -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) = .1. ) : No typesetting found for |- ( ph -> ( ( ( (/) eval R ) ` ( ( (/) eSymPoly R ) ` 0 ) ) ` (/) ) = .1. ) with typecode |-
235	135 234	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 |-
236		iftrue	$$⊢l=0\to if\left(l=0,\underset{\dot{}}{1},0_R\right)=\underset{\dot{}}{1}$$
237		eqid	$$⊢1_W=1_W$$
238	4 237	ringidval	$$⊢1_W=0_M$$
239	238	eqcomi	$$⊢0_M=1_W$$
240	1 239 219 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)$$
241	126 240	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)$$
242	236 241 175 144	fvmptd4	$$⊢\phi \to {\mathrm{coe}}_1\left(0_M\right)\left(0\right)=\underset{\dot{}}{1}$$
243	128 235 242	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 |-
244		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 |-
245	244	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 |-
246	245	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 |-
247	246	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 |-
248		c0ex	$$⊢0\in \mathrm{V}$$
249		oveq2	$$⊢k=0\to 0-k=0-0$$
250		0m0e0	$$⊢0-0=0$$
251	249 250	eqtrdi	$$⊢k=0\to 0-k=0$$
252	251	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)$$
253		oveq1	$$⊢k=0\to k\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)=0\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)$$
254		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 |-
255	254	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 |-
256	253 255	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 |-
257	252 256	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 |-
258	248 257	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 |-
259	247 258	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 |-
260	141 259	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 |-
261	243 260	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 |-
262		nfv	$$⊢Ⅎz\left(\left(\phi \wedge i\subseteq I\right)\wedge m\in \left(I\setminus i\right)\right)$$
263		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 |-
264	262 263	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 |-
265		nfv	$$⊢Ⅎk\left(\left(\phi \wedge i\subseteq I\right)\wedge m\in \left(I\setminus i\right)\right)$$
266		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 |-
267	265 266	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 |-
268		nfv	$$⊢Ⅎkz\in \left(B^{\left(i\cup \left\{m\right\}\right)}\right)$$
269	267 268	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 |-
270		eqid	$$⊢\left(i\cup \left\{m\right\}\right)\mathrm{eval}R=\left(i\cup \left\{m\right\}\right)\mathrm{eval}R$$
271		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 |-
272		eqid	$$⊢\left|i\cup \left\{m\right\}\right|=\left|i\cup \left\{m\right\}\right|$$
273	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 |-
274		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 |-
275	273 274	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 |-
276		snfi	$$⊢\left\{m\right\}\in \mathrm{Fin}$$
277	276	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 |-
278	275 277	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 |-
279	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 |-
280	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 |-
281		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 |-
282	278 280 281	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 |-
283		2fveq3	$$⊢n=o\to A\left(z\left(n\right)\right)=A\left(z\left(o\right)\right)$$
284	283	oveq2d	$$⊢n=o\to X\underset{\dot{}}{-}A\left(z\left(n\right)\right)=X\underset{\dot{}}{-}A\left(z\left(o\right)\right)$$
285	284	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)$$
286	285	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)$$
287		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)$$
288	287	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 |-
289		ssun2	$$⊢\left\{m\right\}\subseteq i\cup \left\{m\right\}$$
290		vsnid	$$⊢m\in \left\{m\right\}$$
291	289 290	sselii	$$⊢m\in \left(i\cup \left\{m\right\}\right)$$
292	291	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 |-
293		eqid	$$⊢\left(i\cup \left\{m\right\}\right)\setminus \left\{m\right\}=\left(i\cup \left\{m\right\}\right)\setminus \left\{m\right\}$$
294		fveq1	$$⊢z=y\to z\left(n\right)=y\left(n\right)$$
295	294	fveq2d	$$⊢z=y\to A\left(z\left(n\right)\right)=A\left(y\left(n\right)\right)$$
296	295	oveq2d	$$⊢z=y\to X\underset{\dot{}}{-}A\left(z\left(n\right)\right)=X\underset{\dot{}}{-}A\left(y\left(n\right)\right)$$
297	296	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)$$
298	297	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)$$
299	298	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)$$
300	299	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)$$
301		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 |-
302	301	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 |-
303	300 302	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 |-
304	303	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 |-
305	304	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 |-
306		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)$$
307	306	eldifbd	$$⊢\left(\left(\phi \wedge i\subseteq I\right)\wedge m\in \left(I\setminus i\right)\right)\to \neg m\in i$$
308		disjsn	$$⊢i\cap \left\{m\right\}=\varnothing \leftrightarrow \neg m\in i$$
309	307 308	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$$
310		undif5	$$⊢i\cap \left\{m\right\}=\varnothing \to \left(i\cup \left\{m\right\}\right)\setminus \left\{m\right\}=i$$
311	309 310	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$$
312	311	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\}$$
313	312	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)}$$
314		oveq2	$$⊢k=l\to \left|i\right|-k=\left|i\right|-l$$
315	314	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)$$
316		oveq1	$$⊢k=l\to k\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)=l\underset{\dot{}}{\times }N\left(\underset{\dot{}}{1}\right)$$
317		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 |-
318	317	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 |-
319	316 318	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 |-
320	315 319	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 |-
321	320	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 |-
322	312	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|$$
323	322	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)$$
324		2fveq3	$$⊢n=o\to A\left(y\left(n\right)\right)=A\left(y\left(o\right)\right)$$
325	324	oveq2d	$$⊢n=o\to X\underset{\dot{}}{-}A\left(y\left(n\right)\right)=X\underset{\dot{}}{-}A\left(y\left(o\right)\right)$$
326	325	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)$$
327	312	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)$$
328	326 327	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)$$
329	328	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)$$
330	329	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)$$
331	322	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$$
332	330 331	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)$$
333	312	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$$
334	312	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 |-
335	334	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 |-
336	333 335	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 |-
337	336	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 |-
338	337	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 |-
339	332 338	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 |-
340	323 339	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 |-
341	321 340	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 |-
342	313 341	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 |-
343	305 342	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 |-
344	343	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 |-
345	344	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 |-
346		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$$
347		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 |-
348		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|$$
349		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 |-
350	278 349	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 |-
351	282 349	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 |-
352		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)$$
353		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
354	1 2 3 4 346 347 7 8 9 10 11 12 348 350 279 351 352 353	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 |-
355	1 2 3 4 270 271 7 8 9 10 11 12 272 278 279 282 286 288 292 293 345 354	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 |-
356	14	ad2antrr	$$⊢\left(\left(\phi \wedge i\subseteq I\right)\wedge m\in \left(I\setminus i\right)\right)\to I\in \mathrm{Fin}$$
357		simplr	$$⊢\left(\left(\phi \wedge i\subseteq I\right)\wedge m\in \left(I\setminus i\right)\right)\to i\subseteq I$$
358	356 357	ssfid	$$⊢\left(\left(\phi \wedge i\subseteq I\right)\wedge m\in \left(I\setminus i\right)\right)\to i\in \mathrm{Fin}$$
359	276	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}$$
360	358 359	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}$$
361	360	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}$$
362		hashcl	$$⊢i\cup \left\{m\right\}\in \mathrm{Fin}\to \left|i\cup \left\{m\right\}\right|\in {\mathbb{N}}_0$$
363	361 362	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$$
364	363	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 ℂ$$
365		elfznn0	$$⊢k\in \left(0\dots \left|i\cup \left\{m\right\}\right|\right)\to k\in {\mathbb{N}}_0$$
366	365	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$$
367	366	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 ℂ$$
368	364 367	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$$
369	368	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)$$
370	368	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 |-
371	370	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 |-
372	371	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 |-
373	369 372	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 |-
374	373	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 |-
375	355 374	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 |-
376	269 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 ) ) ) /\ 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 |-
377	264 376	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 |-
378	377	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 |-
379	378	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 |-
380	71 88 105 125 261 379 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)$$
381	40	a1i	$$⊢\phi \to B\in \mathrm{V}$$
382	381 14 16	elmapdd	$$⊢\phi \to Z\in \left(B^I\right)$$
383	31 38 380 382 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)$$