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 = {Poly}_{1} (R)$
	vieta.b	$⊢ B = {Base}_{R}$
	vieta.3	$⊢ \underset{˙}{-} = -_{W}$
	vieta.m	$⊢ M = {mulGrp}_{W}$
	vieta.q	$⊢ Q = I eval R$
	vieta.e	No typesetting found for \|- E = ( I eSymPoly R ) with typecode \|-
	vieta.n	$⊢ N = {inv}_{g} (R)$
	vieta.1	$⊢ \underset{˙}{1} = 1_{R}$
	vieta.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	vieta.x	$⊢ X = {var}_{1} (R)$
	vieta.a	$⊢ A = algSc (W)$
	vieta.p	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
	vieta.h	$⊢ H = \|I\|$
	vieta.i	$⊢ φ \to I \in Fin$
	vieta.r	$⊢ φ \to R \in IDomn$
	vieta.z	$⊢ φ \to Z : I ⟶ B$
	vieta.f	$⊢ F = \underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (Z (n)))$
	vieta.k	$⊢ φ \to K \in (0 \dots H)$
	vieta.c	$⊢ C = {coe}_{1} (F)$
Assertion	vieta	$⊢ φ \to C (H - K) = (K \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (K)) (Z)$

Proof

Step	Hyp	Ref	Expression
1		vieta.w	$⊢ W = {Poly}_{1} (R)$
2		vieta.b	$⊢ B = {Base}_{R}$
3		vieta.3	$⊢ \underset{˙}{-} = -_{W}$
4		vieta.m	$⊢ M = {mulGrp}_{W}$
5		vieta.q	$⊢ Q = I 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} (R)$
8		vieta.1	$⊢ \underset{˙}{1} = 1_{R}$
9		vieta.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
10		vieta.x	$⊢ X = {var}_{1} (R)$
11		vieta.a	$⊢ A = algSc (W)$
12		vieta.p	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
13		vieta.h	$⊢ H = \|I\|$
14		vieta.i	$⊢ φ \to I \in Fin$
15		vieta.r	$⊢ φ \to R \in IDomn$
16		vieta.z	$⊢ φ \to Z : I ⟶ B$
17		vieta.f	$⊢ F = \underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (Z (n)))$
18		vieta.k	$⊢ φ \to K \in (0 \dots H)$
19		vieta.c	$⊢ C = {coe}_{1} (F)$
20		fveq1	$⊢ z = Z \to z (n) = Z (n)$
21	20	fveq2d	$⊢ z = Z \to A (z (n)) = A (Z (n))$
22	21	oveq2d	$⊢ z = Z \to X \underset{˙}{-} A (z (n)) = X \underset{˙}{-} A (Z (n))$
23	22	mpteq2dv	$⊢ z = Z \to (n \in I ⟼ X \underset{˙}{-} A (z (n))) = (n \in I ⟼ X \underset{˙}{-} A (Z (n)))$
24	23	oveq2d	$⊢ z = Z \to \underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = \underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (Z (n)))$
25	24 17	eqtr4di	$⊢ z = Z \to \underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = F$
26	25	fveq2d	$⊢ z = Z \to {coe}_{1} (\underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) = {coe}_{1} (F)$
27	26 19	eqtr4di	$⊢ z = Z \to {coe}_{1} (\underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) = C$
28	27	fveq1d	$⊢ z = Z \to {coe}_{1} (\underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (H - k) = C (H - k)$
29		fveq2	$⊢ z = Z \to Q (E (k)) (z) = Q (E (k)) (Z)$
30	29	oveq2d	$⊢ z = Z \to (k \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (k)) (z) = (k \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (k)) (Z)$
31	28 30	eqeq12d	$⊢ z = Z \to ({coe}_{1} (\underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (H - k) = (k \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (k)) (z) \leftrightarrow C (H - k) = (k \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (k)) (Z))$
32		oveq2	$⊢ k = K \to H - k = H - K$
33	32	fveq2d	$⊢ k = K \to C (H - k) = C (H - K)$
34		oveq1	$⊢ k = K \to k \underset{˙}{\times} N (\underset{˙}{1}) = K \underset{˙}{\times} N (\underset{˙}{1})$
35		2fveq3	$⊢ k = K \to Q (E (k)) = Q (E (K))$
36	35	fveq1d	$⊢ k = K \to Q (E (k)) (Z) = Q (E (K)) (Z)$
37	34 36	oveq12d	$⊢ k = K \to (k \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (k)) (Z) = (K \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (K)) (Z)$
38	33 37	eqeq12d	$⊢ k = K \to (C (H - k) = (k \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (k)) (Z) \leftrightarrow C (H - K) = (K \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (K)) (Z))$
39		oveq2	$⊢ j = \emptyset \to B^{j} = B^{\emptyset}$
40	2	fvexi	$⊢ B \in V$
41		mapdm0	$⊢ B \in V \to B^{\emptyset} = \{\emptyset\}$
42	40 41	ax-mp	$⊢ B^{\emptyset} = \{\emptyset\}$
43	39 42	eqtrdi	$⊢ j = \emptyset \to B^{j} = \{\emptyset\}$
44		fveq2	$⊢ j = \emptyset \to \|j\| = \|\emptyset\|$
45	44	oveq2d	$⊢ j = \emptyset \to (0 \dots \|j\|) = (0 \dots \|\emptyset\|)$
46		hash0	$⊢ \|\emptyset\| = 0$
47	46	oveq2i	$⊢ (0 \dots \|\emptyset\|) = (0 \dots 0)$
48		fz0sn	$⊢ (0 \dots 0) = \{0\}$
49	47 48	eqtri	$⊢ (0 \dots \|\emptyset\|) = \{0\}$
50	45 49	eqtrdi	$⊢ j = \emptyset \to (0 \dots \|j\|) = \{0\}$
51		mpteq1	$⊢ j = \emptyset \to (n \in j ⟼ X \underset{˙}{-} A (z (n))) = (n \in \emptyset ⟼ X \underset{˙}{-} A (z (n)))$
52		mpt0	$⊢ (n \in \emptyset ⟼ X \underset{˙}{-} A (z (n))) = \emptyset$
53	51 52	eqtrdi	$⊢ j = \emptyset \to (n \in j ⟼ X \underset{˙}{-} A (z (n))) = \emptyset$
54	53	oveq2d	$⊢ j = \emptyset \to \underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = \sum_{M} \emptyset$
55		eqid	$⊢ 0_{M} = 0_{M}$
56	55	gsum0	$⊢ \sum_{M} \emptyset = 0_{M}$
57	54 56	eqtrdi	$⊢ j = \emptyset \to \underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = 0_{M}$
58	57	fveq2d	$⊢ j = \emptyset \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) = {coe}_{1} (0_{M})$
59	44	oveq1d	$⊢ j = \emptyset \to \|j\| - k = \|\emptyset\| - k$
60	46	oveq1i	$⊢ \|\emptyset\| - k = 0 - k$
61	59 60	eqtrdi	$⊢ j = \emptyset \to \|j\| - k = 0 - k$
62	58 61	fveq12d	$⊢ j = \emptyset \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (\|j\| - k) = {coe}_{1} (0_{M}) (0 - k)$
63		oveq1	$⊢ j = \emptyset \to j eval R = \emptyset 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 \|j\| = \|i\|$
74	73	oveq2d	$⊢ j = i \to (0 \dots \|j\|) = (0 \dots \|i\|)$
75		mpteq1	$⊢ j = i \to (n \in j ⟼ X \underset{˙}{-} A (z (n))) = (n \in i ⟼ X \underset{˙}{-} A (z (n)))$
76	75	oveq2d	$⊢ j = i \to \underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = \underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (z (n)))$
77	76	fveq2d	$⊢ j = i \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) = {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (z (n))))$
78	73	oveq1d	$⊢ j = i \to \|j\| - k = \|i\| - k$
79	77 78	fveq12d	$⊢ j = i \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (\|j\| - k) = {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (\|i\| - k)$
80		oveq1	$⊢ j = i \to j eval R = i 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 \{m\} \to B^{j} = B^{(i \cup \{m\})}$
90		fveq2	$⊢ j = i \cup \{m\} \to \|j\| = \|i \cup \{m\}\|$
91	90	oveq2d	$⊢ j = i \cup \{m\} \to (0 \dots \|j\|) = (0 \dots \|i \cup \{m\}\|)$
92		mpteq1	$⊢ j = i \cup \{m\} \to (n \in j ⟼ X \underset{˙}{-} A (z (n))) = (n \in (i \cup \{m\}) ⟼ X \underset{˙}{-} A (z (n)))$
93	92	oveq2d	$⊢ j = i \cup \{m\} \to \underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = \underset{n \in i \cup \{m\}}{\sum_{M}} (X \underset{˙}{-} A (z (n)))$
94	93	fveq2d	$⊢ j = i \cup \{m\} \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) = {coe}_{1} (\underset{n \in i \cup \{m\}}{\sum_{M}} (X \underset{˙}{-} A (z (n))))$
95	90	oveq1d	$⊢ j = i \cup \{m\} \to \|j\| - k = \|i \cup \{m\}\| - k$
96	94 95	fveq12d	$⊢ j = i \cup \{m\} \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (\|j\| - k) = {coe}_{1} (\underset{n \in i \cup \{m\}}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (\|i \cup \{m\}\| - k)$
97		oveq1	$⊢ j = i \cup \{m\} \to j eval R = (i \cup \{m\}) 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 \|j\| = \|I\|$
108	107 13	eqtr4di	$⊢ j = I \to \|j\| = H$
109	108	oveq2d	$⊢ j = I \to (0 \dots \|j\|) = (0 \dots H)$
110		mpteq1	$⊢ j = I \to (n \in j ⟼ X \underset{˙}{-} A (z (n))) = (n \in I ⟼ X \underset{˙}{-} A (z (n)))$
111	110	oveq2d	$⊢ j = I \to \underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = \underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n)))$
112	111	fveq2d	$⊢ j = I \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) = {coe}_{1} (\underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n))))$
113	108	oveq1d	$⊢ j = I \to \|j\| - k = H - k$
114	112 113	fveq12d	$⊢ j = I \to {coe}_{1} (\underset{n \in j}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (\|j\| - k) = {coe}_{1} (\underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (H - k)$
115		oveq1	$⊢ j = I \to j eval R = I eval R$
116	115 5	eqtr4di	$⊢ j = I \to j 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	$⊢ φ \to R \in Ring$
127	2 8 126	ringidcld	$⊢ φ \to \underset{˙}{1} \in B$
128	2 9 8 126 127	ringlidmd	$⊢ φ \to \underset{˙}{1} \underset{˙}{\cdot} \underset{˙}{1} = \underset{˙}{1}$
129	126	ringgrpd	$⊢ φ \to R \in Grp$
130	2 7 129 127	grpinvcld	$⊢ φ \to N (\underset{˙}{1}) \in B$
131		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
132	131 2	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
133	131 8	ringidval	$⊢ \underset{˙}{1} = 0_{{mulGrp}_{R}}$
134	132 133 12	mulg0	$⊢ N (\underset{˙}{1}) \in B \to 0 \underset{˙}{\times} N (\underset{˙}{1}) = \underset{˙}{1}$
135	130 134	syl	$⊢ φ \to 0 \underset{˙}{\times} N (\underset{˙}{1}) = \underset{˙}{1}$
136		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
137	136 8	zrh1	$⊢ R \in Ring \to ℤRHom (R) (1) = \underset{˙}{1}$
138	126 137	syl	$⊢ φ \to ℤRHom (R) (1) = \underset{˙}{1}$
139	138	sneqd	$⊢ φ \to \{ℤRHom (R) (1)\} = \{\underset{˙}{1}\}$
140	139	xpeq2d	$⊢ φ \to \{\emptyset\} \times \{ℤRHom (R) (1)\} = \{\emptyset\} \times \{\underset{˙}{1}\}$
141		0ex	$⊢ \emptyset \in V$
142	141	a1i	$⊢ φ \to \emptyset \in V$
143	8	fvexi	$⊢ \underset{˙}{1} \in V$
144	143	a1i	$⊢ φ \to \underset{˙}{1} \in V$
145		xpsng	$⊢ (\emptyset \in V \land \underset{˙}{1} \in V) \to \{\emptyset\} \times \{\underset{˙}{1}\} = \{⟨\emptyset, \underset{˙}{1}⟩\}$
146	142 144 145	syl2anc	$⊢ φ \to \{\emptyset\} \times \{\underset{˙}{1}\} = \{⟨\emptyset, \underset{˙}{1}⟩\}$
147		0xp	$⊢ \emptyset \times \{0\} = \emptyset$
148	147	eqcomi	$⊢ \emptyset = \emptyset \times \{0\}$
149	148	eqeq2i	$⊢ f = \emptyset \leftrightarrow f = \emptyset \times \{0\}$
150	149	biimpi	$⊢ f = \emptyset \to f = \emptyset \times \{0\}$
151	150	adantl	$⊢ (φ \land f = \emptyset) \to f = \emptyset \times \{0\}$
152	151	iftrued	$⊢ (φ \land f = \emptyset) \to if (f = \emptyset \times \{0\}, \underset{˙}{1}, 0_{R}) = \underset{˙}{1}$
153	152 142 144	fmptsnd	$⊢ φ \to \{⟨\emptyset, \underset{˙}{1}⟩\} = (f \in \{\emptyset\} ⟼ if (f = \emptyset \times \{0\}, \underset{˙}{1}, 0_{R}))$
154	140 146 153	3eqtrd	$⊢ φ \to \{\emptyset\} \times \{ℤRHom (R) (1)\} = (f \in \{\emptyset\} ⟼ if (f = \emptyset \times \{0\}, \underset{˙}{1}, 0_{R}))$
155		elsni	$⊢ h \in \{\emptyset\} \to h = \emptyset$
156		nn0ex	$⊢ ℕ_{0} \in V$
157		mapdm0	$⊢ ℕ_{0} \in V \to {ℕ_{0}}^{\emptyset} = \{\emptyset\}$
158	156 157	ax-mp	$⊢ {ℕ_{0}}^{\emptyset} = \{\emptyset\}$
159	155 158	eleq2s	$⊢ h \in ({ℕ_{0}}^{\emptyset}) \to h = \emptyset$
160	159	cnveqd	$⊢ h \in ({ℕ_{0}}^{\emptyset}) \to h^{-1} = \emptyset^{-1}$
161	160	imaeq1d	$⊢ h \in ({ℕ_{0}}^{\emptyset}) \to h^{-1} [ℕ] = \emptyset^{-1} [ℕ]$
162		cnv0	$⊢ \emptyset^{-1} = \emptyset$
163	162	imaeq1i	$⊢ \emptyset^{-1} [ℕ] = \emptyset [ℕ]$
164		0ima	$⊢ \emptyset [ℕ] = \emptyset$
165	163 164	eqtri	$⊢ \emptyset^{-1} [ℕ] = \emptyset$
166	161 165	eqtrdi	$⊢ h \in ({ℕ_{0}}^{\emptyset}) \to h^{-1} [ℕ] = \emptyset$
167		0fi	$⊢ \emptyset \in Fin$
168	166 167	eqeltrdi	$⊢ h \in ({ℕ_{0}}^{\emptyset}) \to h^{-1} [ℕ] \in Fin$
169	168	rabeqc	$⊢ \{h \in ({ℕ_{0}}^{\emptyset}) \| h^{-1} [ℕ] \in Fin\} = {ℕ_{0}}^{\emptyset}$
170	169 158	eqtr2i	$⊢ \{\emptyset\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| h^{-1} [ℕ] \in Fin\}$
171		eqid	$⊢ \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
172	171	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| h^{-1} [ℕ] \in Fin\}$
173	170 172	eqtr4i	$⊢ \{\emptyset\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
174		0nn0	$⊢ 0 \in ℕ_{0}$
175	174	a1i	$⊢ φ \to 0 \in ℕ_{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 = \emptyset \to (\|c\| = 0 \leftrightarrow \|\emptyset\| = 0)$
178		0elpw	$⊢ \emptyset \in 𝒫 \emptyset$
179	178	a1i	$⊢ φ \to \emptyset \in 𝒫 \emptyset$
180	46	a1i	$⊢ φ \to \|\emptyset\| = 0$
181		hasheq0	$⊢ c \in 𝒫 \emptyset \to (\|c\| = 0 \leftrightarrow c = \emptyset)$
182	181	biimpa	$⊢ (c \in 𝒫 \emptyset \land \|c\| = 0) \to c = \emptyset$
183	182	adantll	$⊢ ((φ \land c \in 𝒫 \emptyset) \land \|c\| = 0) \to c = \emptyset$
184	177 179 180 183	rabeqsnd	$⊢ φ \to \{c \in 𝒫 \emptyset \| \|c\| = 0\} = \{\emptyset\}$
185	184	imaeq2d	$⊢ φ \to 𝟙_{\emptyset} [\{c \in 𝒫 \emptyset \| \|c\| = 0\}] = 𝟙_{\emptyset} [\{\emptyset\}]$
186		pw0	$⊢ 𝒫 \emptyset = \{\emptyset\}$
187	186	a1i	$⊢ φ \to 𝒫 \emptyset = \{\emptyset\}$
188		indf1o	$⊢ \emptyset \in V \to 𝟙_{\emptyset} : 𝒫 \emptyset \underset{1-1 onto}{⟶} {\{0, 1\}}^{\emptyset}$
189		f1of	$⊢ 𝟙_{\emptyset} : 𝒫 \emptyset \underset{1-1 onto}{⟶} {\{0, 1\}}^{\emptyset} \to 𝟙_{\emptyset} : 𝒫 \emptyset ⟶ {\{0, 1\}}^{\emptyset}$
190	142 188 189	3syl	$⊢ φ \to 𝟙_{\emptyset} : 𝒫 \emptyset ⟶ {\{0, 1\}}^{\emptyset}$
191	187 190	feq2dd	$⊢ φ \to 𝟙_{\emptyset} : \{\emptyset\} ⟶ {\{0, 1\}}^{\emptyset}$
192	191	ffnd	$⊢ φ \to 𝟙_{\emptyset} Fn \{\emptyset\}$
193	141	snid	$⊢ \emptyset \in \{\emptyset\}$
194	193	a1i	$⊢ φ \to \emptyset \in \{\emptyset\}$
195	192 194	fnimasnd	$⊢ φ \to 𝟙_{\emptyset} [\{\emptyset\}] = \{𝟙_{\emptyset} (\emptyset)\}$
196		ssidd	$⊢ φ \to \emptyset \subseteq \emptyset$
197		indf	$⊢ (\emptyset \in V \land \emptyset \subseteq \emptyset) \to 𝟙_{\emptyset} (\emptyset) : \emptyset ⟶ \{0, 1\}$
198	142 196 197	syl2anc	$⊢ φ \to 𝟙_{\emptyset} (\emptyset) : \emptyset ⟶ \{0, 1\}$
199		f0bi	$⊢ 𝟙_{\emptyset} (\emptyset) : \emptyset ⟶ \{0, 1\} \leftrightarrow 𝟙_{\emptyset} (\emptyset) = \emptyset$
200	198 199	sylib	$⊢ φ \to 𝟙_{\emptyset} (\emptyset) = \emptyset$
201	200	sneqd	$⊢ φ \to \{𝟙_{\emptyset} (\emptyset)\} = \{\emptyset\}$
202	185 195 201	3eqtrd	$⊢ φ \to 𝟙_{\emptyset} [\{c \in 𝒫 \emptyset \| \|c\| = 0\}] = \{\emptyset\}$
203	202	fveq2d	$⊢ φ \to 𝟙_{\{\emptyset\}} (𝟙_{\emptyset} [\{c \in 𝒫 \emptyset \| \|c\| = 0\}]) = 𝟙_{\{\emptyset\}} (\{\emptyset\})$
204		p0ex	$⊢ \{\emptyset\} \in V$
205		indconst1	$⊢ \{\emptyset\} \in V \to 𝟙_{\{\emptyset\}} (\{\emptyset\}) = \{\emptyset\} \times \{1\}$
206	204 205	ax-mp	$⊢ 𝟙_{\{\emptyset\}} (\{\emptyset\}) = \{\emptyset\} \times \{1\}$
207	203 206	eqtrdi	$⊢ φ \to 𝟙_{\{\emptyset\}} (𝟙_{\emptyset} [\{c \in 𝒫 \emptyset \| \|c\| = 0\}]) = \{\emptyset\} \times \{1\}$
208	207	coeq2d	$⊢ φ \to ℤRHom (R) \circ 𝟙_{\{\emptyset\}} (𝟙_{\emptyset} [\{c \in 𝒫 \emptyset \| \|c\| = 0\}]) = ℤRHom (R) \circ (\{\emptyset\} \times \{1\})$
209	136	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
210		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
211	210 2	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ B$
212	126 209 211	3syl	$⊢ φ \to ℤRHom (R) : ℤ ⟶ B$
213	212	ffnd	$⊢ φ \to ℤRHom (R) Fn ℤ$
214		1zzd	$⊢ φ \to 1 \in ℤ$
215		fcoconst	$⊢ (ℤRHom (R) Fn ℤ \land 1 \in ℤ) \to ℤRHom (R) \circ (\{\emptyset\} \times \{1\}) = \{\emptyset\} \times \{ℤRHom (R) (1)\}$
216	213 214 215	syl2anc	$⊢ φ \to ℤRHom (R) \circ (\{\emptyset\} \times \{1\}) = \{\emptyset\} \times \{ℤRHom (R) (1)\}$
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	$⊢ \emptyset mPoly R = \emptyset mPoly R$
219		eqid	$⊢ 0_{R} = 0_{R}$
220		eqid	$⊢ algSc (\emptyset mPoly R) = algSc (\emptyset mPoly R)$
221	218 170 219 2 220 142 126 127	mplascl	$⊢ φ \to algSc (\emptyset mPoly R) (\underset{˙}{1}) = (f \in \{\emptyset\} ⟼ if (f = \emptyset \times \{0\}, \underset{˙}{1}, 0_{R}))$
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	$⊢ \emptyset eval R = \emptyset eval R$
226	193 158	eleqtrri	$⊢ \emptyset \in ({ℕ_{0}}^{\emptyset})$
227	226	a1i	$⊢ φ \to \emptyset \in ({ℕ_{0}}^{\emptyset})$
228	15	idomcringd	$⊢ φ \to R \in CRing$
229	225 218 2 220 227 228 127	evlsca	$⊢ φ \to (\emptyset eval R) (algSc (\emptyset mPoly R) (\underset{˙}{1})) = (B^{\emptyset}) \times \{\underset{˙}{1}\}$
230	229	fveq1d	$⊢ φ \to (\emptyset eval R) (algSc (\emptyset mPoly R) (\underset{˙}{1})) (\emptyset) = ((B^{\emptyset}) \times \{\underset{˙}{1}\}) (\emptyset)$
231	193 42	eleqtrri	$⊢ \emptyset \in (B^{\emptyset})$
232	143	fvconst2	$⊢ \emptyset \in (B^{\emptyset}) \to ((B^{\emptyset}) \times \{\underset{˙}{1}\}) (\emptyset) = \underset{˙}{1}$
233	231 232	mp1i	$⊢ φ \to ((B^{\emptyset}) \times \{\underset{˙}{1}\}) (\emptyset) = \underset{˙}{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 (l = 0, \underset{˙}{1}, 0_{R}) = \underset{˙}{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 Ring \to {coe}_{1} (0_{M}) = (l \in ℕ_{0} ⟼ if (l = 0, \underset{˙}{1}, 0_{R}))$
241	126 240	syl	$⊢ φ \to {coe}_{1} (0_{M}) = (l \in ℕ_{0} ⟼ if (l = 0, \underset{˙}{1}, 0_{R}))$
242	236 241 175 144	fvmptd4	$⊢ φ \to {coe}_{1} (0_{M}) (0) = \underset{˙}{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 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 {coe}_{1} (0_{M}) (0 - k) = {coe}_{1} (0_{M}) (0)$
253		oveq1	$⊢ k = 0 \to k \underset{˙}{\times} N (\underset{˙}{1}) = 0 \underset{˙}{\times} N (\underset{˙}{1})$
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 ((φ \land i \subseteq I) \land m \in (I ∖ i))$
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 ((φ \land i \subseteq I) \land m \in (I ∖ i))$
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	$⊢ Ⅎ k z \in (B^{(i \cup \{m\})})$
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	$⊢ (i \cup \{m\}) eval R = (i \cup \{m\}) 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	$⊢ \|i \cup \{m\}\| = \|i \cup \{m\}\|$
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	$⊢ \{m\} \in 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 (z (n)) = A (z (o))$
284	283	oveq2d	$⊢ n = o \to X \underset{˙}{-} A (z (n)) = X \underset{˙}{-} A (z (o))$
285	284	cbvmptv	$⊢ (n \in (i \cup \{m\}) ⟼ X \underset{˙}{-} A (z (n))) = (o \in (i \cup \{m\}) ⟼ X \underset{˙}{-} A (z (o)))$
286	285	oveq2i	$⊢ \underset{n \in i \cup \{m\}}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = \underset{o \in i \cup \{m\}}{\sum_{M}} (X \underset{˙}{-} A (z (o)))$
287		fznn0sub2	$⊢ k \in (0 \dots \|i \cup \{m\}\|) \to \|i \cup \{m\}\| - k \in (0 \dots \|i \cup \{m\}\|)$
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	$⊢ \{m\} \subseteq i \cup \{m\}$
290		vsnid	$⊢ m \in \{m\}$
291	289 290	sselii	$⊢ m \in (i \cup \{m\})$
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	$⊢ (i \cup \{m\}) ∖ \{m\} = (i \cup \{m\}) ∖ \{m\}$
294		fveq1	$⊢ z = y \to z (n) = y (n)$
295	294	fveq2d	$⊢ z = y \to A (z (n)) = A (y (n))$
296	295	oveq2d	$⊢ z = y \to X \underset{˙}{-} A (z (n)) = X \underset{˙}{-} A (y (n))$
297	296	mpteq2dv	$⊢ z = y \to (n \in i ⟼ X \underset{˙}{-} A (z (n))) = (n \in i ⟼ X \underset{˙}{-} A (y (n)))$
298	297	oveq2d	$⊢ z = y \to \underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (z (n))) = \underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n)))$
299	298	fveq2d	$⊢ z = y \to {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) = {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n))))$
300	299	fveq1d	$⊢ z = y \to {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (\|i\| - k) = {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n)))) (\|i\| - k)$
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	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to m \in (I ∖ i)$
307	306	eldifbd	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to \neg m \in i$
308		disjsn	$⊢ i \cap \{m\} = \emptyset \leftrightarrow \neg m \in i$
309	307 308	sylibr	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to i \cap \{m\} = \emptyset$
310		undif5	$⊢ i \cap \{m\} = \emptyset \to (i \cup \{m\}) ∖ \{m\} = i$
311	309 310	syl	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to (i \cup \{m\}) ∖ \{m\} = i$
312	311	eqcomd	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to i = (i \cup \{m\}) ∖ \{m\}$
313	312	oveq2d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to B^{i} = B^{((i \cup \{m\}) ∖ \{m\})}$
314		oveq2	$⊢ k = l \to \|i\| - k = \|i\| - l$
315	314	fveq2d	$⊢ k = l \to {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n)))) (\|i\| - k) = {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n)))) (\|i\| - l)$
316		oveq1	$⊢ k = l \to k \underset{˙}{\times} N (\underset{˙}{1}) = l \underset{˙}{\times} N (\underset{˙}{1})$
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	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to \|i\| = \|(i \cup \{m\}) ∖ \{m\}\|$
323	322	oveq2d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to (0 \dots \|i\|) = (0 \dots \|(i \cup \{m\}) ∖ \{m\}\|)$
324		2fveq3	$⊢ n = o \to A (y (n)) = A (y (o))$
325	324	oveq2d	$⊢ n = o \to X \underset{˙}{-} A (y (n)) = X \underset{˙}{-} A (y (o))$
326	325	cbvmptv	$⊢ (n \in i ⟼ X \underset{˙}{-} A (y (n))) = (o \in i ⟼ X \underset{˙}{-} A (y (o)))$
327	312	mpteq1d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to (o \in i ⟼ X \underset{˙}{-} A (y (o))) = (o \in ((i \cup \{m\}) ∖ \{m\}) ⟼ X \underset{˙}{-} A (y (o)))$
328	326 327	eqtrid	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to (n \in i ⟼ X \underset{˙}{-} A (y (n))) = (o \in ((i \cup \{m\}) ∖ \{m\}) ⟼ X \underset{˙}{-} A (y (o)))$
329	328	oveq2d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to \underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n))) = \underset{o \in (i \cup \{m\}) ∖ \{m\}}{\sum_{M}} (X \underset{˙}{-} A (y (o)))$
330	329	fveq2d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n)))) = {coe}_{1} (\underset{o \in (i \cup \{m\}) ∖ \{m\}}{\sum_{M}} (X \underset{˙}{-} A (y (o))))$
331	322	oveq1d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to \|i\| - l = \|(i \cup \{m\}) ∖ \{m\}\| - l$
332	330 331	fveq12d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to {coe}_{1} (\underset{n \in i}{\sum_{M}} (X \underset{˙}{-} A (y (n)))) (\|i\| - l) = {coe}_{1} (\underset{o \in (i \cup \{m\}) ∖ \{m\}}{\sum_{M}} (X \underset{˙}{-} A (y (o)))) (\|(i \cup \{m\}) ∖ \{m\}\| - l)$
333	312	oveq1d	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to i eval R = ((i \cup \{m\}) ∖ \{m\}) 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	$⊢ ((i \cup \{m\}) ∖ \{m\}) eval R = ((i \cup \{m\}) ∖ \{m\}) 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	$⊢ \|(i \cup \{m\}) ∖ \{m\}\| = \|(i \cup \{m\}) ∖ \{m\}\|$
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 (i \cup \{m\}) ∖ \{m\}}{\sum_{M}} (X \underset{˙}{-} A (({z ↾}_{((i \cup \{m\}) ∖ \{m\})}) (o))) = \underset{o \in (i \cup \{m\}) ∖ \{m\}}{\sum_{M}} (X \underset{˙}{-} A (({z ↾}_{((i \cup \{m\}) ∖ \{m\})}) (o)))$
353		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
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	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to I \in Fin$
357		simplr	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to i \subseteq I$
358	356 357	ssfid	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to i \in Fin$
359	276	a1i	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to \{m\} \in Fin$
360	358 359	unfid	$⊢ ((φ \land i \subseteq I) \land m \in (I ∖ i)) \to i \cup \{m\} \in Fin$
361	360	adantr	$⊢ (((φ \land i \subseteq I) \land m \in (I ∖ i)) \land k \in (0 \dots \|i \cup \{m\}\|)) \to i \cup \{m\} \in Fin$
362		hashcl	$⊢ i \cup \{m\} \in Fin \to \|i \cup \{m\}\| \in ℕ_{0}$
363	361 362	syl	$⊢ (((φ \land i \subseteq I) \land m \in (I ∖ i)) \land k \in (0 \dots \|i \cup \{m\}\|)) \to \|i \cup \{m\}\| \in ℕ_{0}$
364	363	nn0cnd	$⊢ (((φ \land i \subseteq I) \land m \in (I ∖ i)) \land k \in (0 \dots \|i \cup \{m\}\|)) \to \|i \cup \{m\}\| \in ℂ$
365		elfznn0	$⊢ k \in (0 \dots \|i \cup \{m\}\|) \to k \in ℕ_{0}$
366	365	adantl	$⊢ (((φ \land i \subseteq I) \land m \in (I ∖ i)) \land k \in (0 \dots \|i \cup \{m\}\|)) \to k \in ℕ_{0}$
367	366	nn0cnd	$⊢ (((φ \land i \subseteq I) \land m \in (I ∖ i)) \land k \in (0 \dots \|i \cup \{m\}\|)) \to k \in ℂ$
368	364 367	nncand	$⊢ (((φ \land i \subseteq I) \land m \in (I ∖ i)) \land k \in (0 \dots \|i \cup \{m\}\|)) \to \|i \cup \{m\}\| - (\|i \cup \{m\}\| - k) = k$
369	368	oveq1d	$⊢ (((φ \land i \subseteq I) \land m \in (I ∖ i)) \land k \in (0 \dots \|i \cup \{m\}\|)) \to (\|i \cup \{m\}\| - (\|i \cup \{m\}\| - k)) \underset{˙}{\times} N (\underset{˙}{1}) = k \underset{˙}{\times} N (\underset{˙}{1})$
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	$⊢ φ \to \forall z \in (B^{I}) \forall k \in (0 \dots H) {coe}_{1} (\underset{n \in I}{\sum_{M}} (X \underset{˙}{-} A (z (n)))) (H - k) = (k \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (k)) (z)$
381	40	a1i	$⊢ φ \to B \in V$
382	381 14 16	elmapdd	$⊢ φ \to Z \in (B^{I})$
383	31 38 380 382 18	rspc2dv	$⊢ φ \to C (H - K) = (K \underset{˙}{\times} N (\underset{˙}{1})) \underset{˙}{\cdot} Q (E (K)) (Z)$

Metamath Proof Explorer

Theorem vieta

Proof