Theorem vieta 33993

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

Hypotheses

Ref	Expression
vieta.w	⊢ 𝑊 = (Poly1‘𝑅)
vieta.b	⊢ 𝐵 = (Base‘𝑅)
vieta.3	⊢ − = (-g‘𝑊)
vieta.m	⊢ 𝑀 = (mulGrp‘𝑊)
vieta.q	⊢ 𝑄 = (𝐼 eval 𝑅)
vieta.e	⊢ 𝐸 = (𝐼eSymPoly𝑅)
vieta.n	⊢ 𝑁 = (invg‘𝑅)
vieta.1	⊢ 1 = (1r‘𝑅)
vieta.t	⊢ · = (.r‘𝑅)
vieta.x	⊢ 𝑋 = (var1‘𝑅)
vieta.a	⊢ 𝐴 = (algSc‘𝑊)
vieta.p	⊢ ↑ = (.g‘(mulGrp‘𝑅))
vieta.h	⊢ 𝐻 = (♯‘𝐼)
vieta.i	⊢ (𝜑 → 𝐼 ∈ Fin)
vieta.r	⊢ (𝜑 → 𝑅 ∈ IDomn)
vieta.z	⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
vieta.f	⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
vieta.k	⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
vieta.c	⊢ 𝐶 = (coe1‘𝐹)

Assertion

Ref	Expression
vieta	⊢ (𝜑 → (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))

Distinct variable groups:   − ,𝑛   𝐴,𝑛   𝑛,𝐼   𝑛,𝑋   𝑛,𝑍

Allowed substitution hints:   𝜑(𝑛)   𝐵(𝑛)   𝐶(𝑛)   𝑄(𝑛)   𝑅(𝑛)   · (𝑛)   1 (𝑛)   𝐸(𝑛)   ↑ (𝑛)   𝐹(𝑛)   𝐻(𝑛)   𝐾(𝑛)   𝑀(𝑛)   𝑁(𝑛)   𝑊(𝑛)

Proof of Theorem vieta

Dummy variables 𝑖 𝑗 𝑘 𝑚 𝑧 𝑙 𝑜 𝑦 𝑓 ℎ 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq1 6884	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧‘𝑛) = (𝑍‘𝑛))
2	1	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑍‘𝑛)))
3	2	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
4	3	mpteq2dv 5207	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
5	4	oveq2d 7432	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
6		vieta.f	. . . . . . 7 ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
7	5, 6	eqtr4di 2818	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = 𝐹)
8	7	fveq2d 6889	. . . . 5 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘𝐹))
9		vieta.c	. . . . 5 ⊢ 𝐶 = (coe1‘𝐹)
10	8, 9	eqtr4di 2818	. . . 4 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = 𝐶)
11	10	fveq1d 6887	. . 3 ⊢ (𝑧 = 𝑍 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝑘)))
12		fveq2 6885	. . . 4 ⊢ (𝑧 = 𝑍 → ((𝑄‘(𝐸‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑍))
13	12	oveq2d 7432	. . 3 ⊢ (𝑧 = 𝑍 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)))
14	11, 13	eqeq12d 2781	. 2 ⊢ (𝑧 = 𝑍 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) ↔ (𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))))
15		oveq2 7424	. . . 4 ⊢ (𝑘 = 𝐾 → (𝐻 − 𝑘) = (𝐻 − 𝐾))
16	15	fveq2d 6889	. . 3 ⊢ (𝑘 = 𝐾 → (𝐶‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝐾)))
17		oveq1 7423	. . . 4 ⊢ (𝑘 = 𝐾 → (𝑘 ↑ (𝑁‘ 1 )) = (𝐾 ↑ (𝑁‘ 1 )))
18		2fveq3 6890	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝐾)))
19	18	fveq1d 6887	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝐾))‘𝑍))
20	17, 19	oveq12d 7434	. . 3 ⊢ (𝑘 = 𝐾 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))
21	16, 20	eqeq12d 2781	. 2 ⊢ (𝑘 = 𝐾 → ((𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ↔ (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍))))
22		oveq2 7424	. . . . 5 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = (𝐵 ↑m ∅))
23		vieta.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
24	23	fvexi 6899	. . . . . 6 ⊢ 𝐵 ∈ V
25		mapdm0 8841	. . . . . 6 ⊢ (𝐵 ∈ V → (𝐵 ↑m ∅) = {∅})
26	24, 25	ax-mp 5	. . . . 5 ⊢ (𝐵 ↑m ∅) = {∅}
27	22, 26	eqtrdi 2816	. . . 4 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = {∅})
28		fveq2 6885	. . . . . . 7 ⊢ (𝑗 = ∅ → (♯‘𝑗) = (♯‘∅))
29	28	oveq2d 7432	. . . . . 6 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = (0...(♯‘∅)))
30		hash0 14416	. . . . . . . 8 ⊢ (♯‘∅) = 0
31	30	oveq2i 7427	. . . . . . 7 ⊢ (0...(♯‘∅)) = (0...0)
32		fz0sn 13667	. . . . . . 7 ⊢ (0...0) = {0}
33	31, 32	eqtri 2788	. . . . . 6 ⊢ (0...(♯‘∅)) = {0}
34	29, 33	eqtrdi 2816	. . . . 5 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = {0})
35		mpteq1 5202	. . . . . . . . . . 11 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
36		mpt0 6681	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅
37	35, 36	eqtrdi 2816	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅)
38	37	oveq2d 7432	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg ∅))
39		eqid 2765	. . . . . . . . . 10 ⊢ (0g‘𝑀) = (0g‘𝑀)
40	39	gsum0 18763	. . . . . . . . 9 ⊢ (𝑀 Σg ∅) = (0g‘𝑀)
41	38, 40	eqtrdi 2816	. . . . . . . 8 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (0g‘𝑀))
42	41	fveq2d 6889	. . . . . . 7 ⊢ (𝑗 = ∅ → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(0g‘𝑀)))
43	28	oveq1d 7431	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = ((♯‘∅) − 𝑘))
44	30	oveq1i 7426	. . . . . . . 8 ⊢ ((♯‘∅) − 𝑘) = (0 − 𝑘)
45	43, 44	eqtrdi 2816	. . . . . . 7 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = (0 − 𝑘))
46	42, 45	fveq12d 6892	. . . . . 6 ⊢ (𝑗 = ∅ → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(0g‘𝑀))‘(0 − 𝑘)))
47		oveq1 7423	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑗 eval 𝑅) = (∅ eval 𝑅))
48		oveq1 7423	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑗eSymPoly𝑅) = (∅eSymPoly𝑅))
49	48	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑗 = ∅ → ((𝑗eSymPoly𝑅)‘𝑘) = ((∅eSymPoly𝑅)‘𝑘))
50	47, 49	fveq12d 6892	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)))
51	50	fveq1d 6887	. . . . . . 7 ⊢ (𝑗 = ∅ → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))
52	51	oveq2d 7432	. . . . . 6 ⊢ (𝑗 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
53	46, 52	eqeq12d 2781	. . . . 5 ⊢ (𝑗 = ∅ → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
54	34, 53	raleqbidv 3340	. . . 4 ⊢ (𝑗 = ∅ → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
55	27, 54	raleqbidv 3340	. . 3 ⊢ (𝑗 = ∅ → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
56		oveq2 7424	. . . 4 ⊢ (𝑗 = 𝑖 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝑖))
57		fveq2 6885	. . . . . 6 ⊢ (𝑗 = 𝑖 → (♯‘𝑗) = (♯‘𝑖))
58	57	oveq2d 7432	. . . . 5 ⊢ (𝑗 = 𝑖 → (0...(♯‘𝑗)) = (0...(♯‘𝑖)))
59		mpteq1 5202	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
60	59	oveq2d 7432	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
61	60	fveq2d 6889	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
62	57	oveq1d 7431	. . . . . . 7 ⊢ (𝑗 = 𝑖 → ((♯‘𝑗) − 𝑘) = ((♯‘𝑖) − 𝑘))
63	61, 62	fveq12d 6892	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
64		oveq1 7423	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑗 eval 𝑅) = (𝑖 eval 𝑅))
65		oveq1 7423	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗eSymPoly𝑅) = (𝑖eSymPoly𝑅))
66	65	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → ((𝑗eSymPoly𝑅)‘𝑘) = ((𝑖eSymPoly𝑅)‘𝑘))
67	64, 66	fveq12d 6892	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)))
68	67	fveq1d 6887	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
69	68	oveq2d 7432	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
70	63, 69	eqeq12d 2781	. . . . 5 ⊢ (𝑗 = 𝑖 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
71	58, 70	raleqbidv 3340	. . . 4 ⊢ (𝑗 = 𝑖 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
72	56, 71	raleqbidv 3340	. . 3 ⊢ (𝑗 = 𝑖 → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
73		oveq2 7424	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝐵 ↑m 𝑗) = (𝐵 ↑m (𝑖 ∪ {𝑚})))
74		fveq2 6885	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (♯‘𝑗) = (♯‘(𝑖 ∪ {𝑚})))
75	74	oveq2d 7432	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (0...(♯‘𝑗)) = (0...(♯‘(𝑖 ∪ {𝑚}))))
76		mpteq1 5202	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
77	76	oveq2d 7432	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
78	77	fveq2d 6889	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
79	74	oveq1d 7431	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((♯‘𝑗) − 𝑘) = ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))
80	78, 79	fveq12d 6892	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))
81		oveq1 7423	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗 eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅))
82		oveq1 7423	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅))
83	82	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗eSymPoly𝑅)‘𝑘) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
84	81, 83	fveq12d 6892	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
85	84	fveq1d 6887	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
86	85	oveq2d 7432	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
87	80, 86	eqeq12d 2781	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
88	75, 87	raleqbidv 3340	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
89	73, 88	raleqbidv 3340	. . 3 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
90		oveq2 7424	. . . 4 ⊢ (𝑗 = 𝐼 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝐼))
91		fveq2 6885	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = (♯‘𝐼))
92		vieta.h	. . . . . . 7 ⊢ 𝐻 = (♯‘𝐼)
93	91, 92	eqtr4di 2818	. . . . . 6 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = 𝐻)
94	93	oveq2d 7432	. . . . 5 ⊢ (𝑗 = 𝐼 → (0...(♯‘𝑗)) = (0...𝐻))
95		mpteq1 5202	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
96	95	oveq2d 7432	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
97	96	fveq2d 6889	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
98	93	oveq1d 7431	. . . . . . 7 ⊢ (𝑗 = 𝐼 → ((♯‘𝑗) − 𝑘) = (𝐻 − 𝑘))
99	97, 98	fveq12d 6892	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)))
100		oveq1 7423	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = (𝐼 eval 𝑅))
101		vieta.q	. . . . . . . . . 10 ⊢ 𝑄 = (𝐼 eval 𝑅)
102	100, 101	eqtr4di 2818	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = 𝑄)
103		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = (𝐼eSymPoly𝑅))
104		vieta.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
105	103, 104	eqtr4di 2818	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = 𝐸)
106	105	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → ((𝑗eSymPoly𝑅)‘𝑘) = (𝐸‘𝑘))
107	102, 106	fveq12d 6892	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (𝑄‘(𝐸‘𝑘)))
108	107	fveq1d 6887	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑧))
109	108	oveq2d 7432	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
110	99, 109	eqeq12d 2781	. . . . 5 ⊢ (𝑗 = 𝐼 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
111	94, 110	raleqbidv 3340	. . . 4 ⊢ (𝑗 = 𝐼 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
112	90, 111	raleqbidv 3340	. . 3 ⊢ (𝑗 = 𝐼 → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m 𝐼)∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
113		vieta.t	. . . . . 6 ⊢ · = (.r‘𝑅)
114		vieta.1	. . . . . 6 ⊢ 1 = (1r‘𝑅)
115		vieta.r	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ IDomn)
116	115	idomringd 20855	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
117	23, 114, 116	ringidcld 20373	. . . . . 6 ⊢ (𝜑 → 1 ∈ 𝐵)
118	23, 113, 114, 116, 117	ringlidmd 20379	. . . . 5 ⊢ (𝜑 → ( 1 · 1 ) = 1 )
119		vieta.n	. . . . . . . 8 ⊢ 𝑁 = (invg‘𝑅)
120	116	ringgrpd 20347	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
121	23, 119, 120, 117	grpinvcld 19078	. . . . . . 7 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
122		eqid 2765	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
123	122, 23	mgpbas 20244	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
124	122, 114	ringidval 20288	. . . . . . . 8 ⊢ 1 = (0g‘(mulGrp‘𝑅))
125		vieta.p	. . . . . . . 8 ⊢ ↑ = (.g‘(mulGrp‘𝑅))
126	123, 124, 125	mulg0 19163	. . . . . . 7 ⊢ ((𝑁‘ 1 ) ∈ 𝐵 → (0 ↑ (𝑁‘ 1 )) = 1 )
127	121, 126	syl 18	. . . . . 6 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) = 1 )
128		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
129	128, 114	zrh1 21691	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → ((ℤRHom‘𝑅)‘1) = 1 )
130	116, 129	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℤRHom‘𝑅)‘1) = 1 )
131	130	sneqd 4603	. . . . . . . . . . . 12 ⊢ (𝜑 → {((ℤRHom‘𝑅)‘1)} = { 1 })
132	131	xpeq2d 5693	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = ({∅} × { 1 }))
133		0ex 5272	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
134	133	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ V)
135	114	fvexi 6899	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
136	135	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ V)
137		xpsng 7139	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ 1 ∈ V) → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
138	134, 136, 137	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
139		0xp 5762	. . . . . . . . . . . . . . . 16 ⊢ (∅ × {0}) = ∅
140	139	eqcomi 2774	. . . . . . . . . . . . . . 15 ⊢ ∅ = (∅ × {0})
141	140	eqeq2i 2778	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ∅ ↔ 𝑓 = (∅ × {0}))
142	141	bilani 510	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 = ∅) → 𝑓 = (∅ × {0}))
143	142	iftrued 4497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 = ∅) → if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅)) = 1 )
144	143, 134, 136	fmptsnd 7171	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨∅, 1 ⟩} = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
145	132, 138, 144	3eqtrd 2804	. . . . . . . . . 10 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
146		elsni 4608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ {∅} → ℎ = ∅)
147		nn0ex 12521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ∈ V
148		mapdm0 8841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ0 ∈ V → (ℕ0 ↑m ∅) = {∅})
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℕ0 ↑m ∅) = {∅}
150	146, 149	eleq2s 2883	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ℎ = ∅)
151	150	cnveqd 5863	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ◡ℎ = ◡∅)
152	151	imaeq1d 6063	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = (◡∅ “ ℕ))
153		cnv0 5871	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡∅ = ∅
154	153	imaeq1i 6061	. . . . . . . . . . . . . . . . . 18 ⊢ (◡∅ “ ℕ) = (∅ “ ℕ)
155		0ima 6082	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ “ ℕ) = ∅
156	154, 155	eqtri 2788	. . . . . . . . . . . . . . . . 17 ⊢ (◡∅ “ ℕ) = ∅
157	152, 156	eqtrdi 2816	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = ∅)
158		0fi 9042	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Fin
159	157, 158	eqeltrdi 2873	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) ∈ Fin)
160	159	rabeqc 3430	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin} = (ℕ0 ↑m ∅)
161	160, 149	eqtr2i 2789	. . . . . . . . . . . . 13 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
162		eqid 2765	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
163	162	psrbasfsupp 33924	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
164	161, 163	eqtr4i 2791	. . . . . . . . . . . 12 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
165		0nn0 12530	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
166	165	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ0)
167	164, 134, 115, 166	esplyfval 33976	. . . . . . . . . . 11 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))))
168		fveqeq2 6894	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ∅ → ((♯‘𝑐) = 0 ↔ (♯‘∅) = 0))
169		0elpw 5328	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 ∅
170	169	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ ∈ 𝒫 ∅)
171	30	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘∅) = 0)
172		hasheq0 14412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ 𝒫 ∅ → ((♯‘𝑐) = 0 ↔ 𝑐 = ∅))
173	172	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ 𝒫 ∅ ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
174	173	adantll 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝒫 ∅) ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
175	168, 170, 171, 174	rabeqsnd 4637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0} = {∅})
176	175	imaeq2d 6064	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = ((𝟭‘∅) “ {∅}))
177		pw0 4780	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∅ = {∅}
178	177	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝒫 ∅ = {∅})
179		indf1o 33213	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ V → (𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅))
180		f1of 6824	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅) → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
181	134, 179, 180	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
182	178, 181	feq2dd 6695	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝟭‘∅):{∅}⟶({0, 1} ↑m ∅))
183	182	ffnd 6710	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝟭‘∅) Fn {∅})
184	133	snid 4630	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ {∅}
185	184	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∅ ∈ {∅})
186	183, 185	fnimasnd 7369	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {∅}) = {((𝟭‘∅)‘∅)})
187		ssidd 3961	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∅ ⊆ ∅)
188		indf 12235	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ V ∧ ∅ ⊆ ∅) → ((𝟭‘∅)‘∅):∅⟶{0, 1})
189	134, 187, 188	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝟭‘∅)‘∅):∅⟶{0, 1})
190		f0bi 6765	. . . . . . . . . . . . . . . . 17 ⊢ (((𝟭‘∅)‘∅):∅⟶{0, 1} ↔ ((𝟭‘∅)‘∅) = ∅)
191	189, 190	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝟭‘∅)‘∅) = ∅)
192	191	sneqd 4603	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {((𝟭‘∅)‘∅)} = {∅})
193	176, 186, 192	3eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = {∅})
194	193	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ((𝟭‘{∅})‘{∅}))
195		p0ex 5357	. . . . . . . . . . . . . 14 ⊢ {∅} ∈ V
196		indconst1 12242	. . . . . . . . . . . . . 14 ⊢ ({∅} ∈ V → ((𝟭‘{∅})‘{∅}) = ({∅} × {1}))
197	195, 196	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝟭‘{∅})‘{∅}) = ({∅} × {1})
198	194, 197	eqtrdi 2816	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ({∅} × {1}))
199	198	coeq2d 5850	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))) = ((ℤRHom‘𝑅) ∘ ({∅} × {1})))
200	128	zrhrhm 21690	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
201		zringbas 21632	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤring)
202	201, 23	rhmf 20592	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
203	116, 200, 202	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝑅):ℤ⟶𝐵)
204	203	ffnd 6710	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤRHom‘𝑅) Fn ℤ)
205		1zzd 12636	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
206		fcoconst 7134	. . . . . . . . . . . 12 ⊢ (((ℤRHom‘𝑅) Fn ℤ ∧ 1 ∈ ℤ) → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
207	204, 205, 206	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
208	167, 199, 207	3eqtrd 2804	. . . . . . . . . 10 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
209		eqid 2765	. . . . . . . . . . 11 ⊢ (∅ mPoly 𝑅) = (∅ mPoly 𝑅)
210		eqid 2765	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
211		eqid 2765	. . . . . . . . . . 11 ⊢ (algSc‘(∅ mPoly 𝑅)) = (algSc‘(∅ mPoly 𝑅))
212	209, 161, 210, 23, 211, 134, 116, 117	mplascl 22244	. . . . . . . . . 10 ⊢ (𝜑 → ((algSc‘(∅ mPoly 𝑅))‘ 1 ) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
213	145, 208, 212	3eqtr4d 2810	. . . . . . . . 9 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((algSc‘(∅ mPoly 𝑅))‘ 1 ))
214	213	fveq2d 6889	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)) = ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )))
215	214	fveq1d 6887	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅))
216		eqid 2765	. . . . . . . . 9 ⊢ (∅ eval 𝑅) = (∅ eval 𝑅)
217	184, 149	eleqtrri 2864	. . . . . . . . . 10 ⊢ ∅ ∈ (ℕ0 ↑m ∅)
218	217	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ (ℕ0 ↑m ∅))
219	115	idomcringd 20854	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
220	216, 209, 23, 211, 218, 219, 117	evlsca 22286	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )) = ((𝐵 ↑m ∅) × { 1 }))
221	220	fveq1d 6887	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅) = (((𝐵 ↑m ∅) × { 1 })‘∅))
222	184, 26	eleqtrri 2864	. . . . . . . 8 ⊢ ∅ ∈ (𝐵 ↑m ∅)
223	135	fvconst2 7206	. . . . . . . 8 ⊢ (∅ ∈ (𝐵 ↑m ∅) → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
224	222, 223	mp1i 14	. . . . . . 7 ⊢ (𝜑 → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
225	215, 221, 224	3eqtrd 2804	. . . . . 6 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = 1 )
226	127, 225	oveq12d 7434	. . . . 5 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)) = ( 1 · 1 ))
227		iftrue 4495	. . . . . 6 ⊢ (𝑙 = 0 → if(𝑙 = 0, 1 , (0g‘𝑅)) = 1 )
228		vieta.w	. . . . . . . 8 ⊢ 𝑊 = (Poly1‘𝑅)
229		vieta.m	. . . . . . . . . 10 ⊢ 𝑀 = (mulGrp‘𝑊)
230		eqid 2765	. . . . . . . . . 10 ⊢ (1r‘𝑊) = (1r‘𝑊)
231	229, 230	ringidval 20288	. . . . . . . . 9 ⊢ (1r‘𝑊) = (0g‘𝑀)
232	231	eqcomi 2774	. . . . . . . 8 ⊢ (0g‘𝑀) = (1r‘𝑊)
233	228, 232, 210, 114	coe1id 22483	. . . . . . 7 ⊢ (𝑅 ∈ Ring → (coe1‘(0g‘𝑀)) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, 1 , (0g‘𝑅))))
234	116, 233	syl 18	. . . . . 6 ⊢ (𝜑 → (coe1‘(0g‘𝑀)) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, 1 , (0g‘𝑅))))
235	227, 234, 166, 136	fvmptd4 7018	. . . . 5 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = 1 )
236	118, 226, 235	3eqtr4rd 2811	. . . 4 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
237		fveq2 6885	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))
238	237	oveq2d 7432	. . . . . . . 8 ⊢ (𝑧 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)))
239	238	eqeq2d 2776	. . . . . . 7 ⊢ (𝑧 = ∅ → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
240	239	ralbidv 3190	. . . . . 6 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
241		c0ex 11211	. . . . . . 7 ⊢ 0 ∈ V
242		oveq2 7424	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (0 − 𝑘) = (0 − 0))
243		0m0e0 12370	. . . . . . . . . 10 ⊢ (0 − 0) = 0
244	242, 243	eqtrdi 2816	. . . . . . . . 9 ⊢ (𝑘 = 0 → (0 − 𝑘) = 0)
245	244	fveq2d 6889	. . . . . . . 8 ⊢ (𝑘 = 0 → ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((coe1‘(0g‘𝑀))‘0))
246		oveq1 7423	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
247		2fveq3 6890	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)))
248	247	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑘 = 0 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))
249	246, 248	oveq12d 7434	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
250	245, 249	eqeq12d 2781	. . . . . . 7 ⊢ (𝑘 = 0 → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))))
251	241, 250	ralsn 4649	. . . . . 6 ⊢ (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
252	240, 251	bitrdi 290	. . . . 5 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))))
253	133, 252	ralsn 4649	. . . 4 ⊢ (∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
254	236, 253	sylibr 237	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
255		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
256		nfra1 3291	. . . . . . 7 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
257	255, 256	nfan 1932	. . . . . 6 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
258		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
259		nfra2w 3303	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
260	258, 259	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
261		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))
262	260, 261	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
263		vieta.3	. . . . . . . . 9 ⊢ − = (-g‘𝑊)
264		eqid 2765	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅)
265		eqid 2765	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚})eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅)
266		vieta.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑅)
267		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
268		eqid 2765	. . . . . . . . 9 ⊢ (♯‘(𝑖 ∪ {𝑚})) = (♯‘(𝑖 ∪ {𝑚}))
269		vieta.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
270	269	ad5antr 747	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝐼 ∈ Fin)
271		simp-5r 798	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ⊆ 𝐼)
272	270, 271	ssfid 9232	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ∈ Fin)
273		snfi 9043	. . . . . . . . . . 11 ⊢ {𝑚} ∈ Fin
274	273	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → {𝑚} ∈ Fin)
275	272, 274	unfid 9159	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
276	115	ad5antr 747	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑅 ∈ IDomn)
277	24	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝐵 ∈ V)
278		simplr 781	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
279	275, 277, 278	elmaprd 33054	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧:(𝑖 ∪ {𝑚})⟶𝐵)
280		2fveq3 6890	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑧‘𝑜)))
281	280	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑧‘𝑜))))
282	281	cbvmptv 5217	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜))))
283	282	oveq2i 7427	. . . . . . . . 9 ⊢ (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜)))))
284		fznn0sub2 13675	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
285	284	adantl 487	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
286		ssun2 4132	. . . . . . . . . . 11 ⊢ {𝑚} ⊆ (𝑖 ∪ {𝑚})
287		vsnid 4631	. . . . . . . . . . 11 ⊢ 𝑚 ∈ {𝑚}
288	286, 287	sselii 3935	. . . . . . . . . 10 ⊢ 𝑚 ∈ (𝑖 ∪ {𝑚})
289	288	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑚 ∈ (𝑖 ∪ {𝑚}))
290		eqid 2765	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = ((𝑖 ∪ {𝑚}) ∖ {𝑚})
291		fveq1 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑦 → (𝑧‘𝑛) = (𝑦‘𝑛))
292	291	fveq2d 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑦 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑦‘𝑛)))
293	292	oveq2d 7432	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑛))))
294	293	mpteq2dv 5207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))
295	294	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))
296	295	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))))
297	296	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
298		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))
299	298	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
300	297, 299	eqeq12d 2781	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
301	300	ralbidv 3190	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
302	301	cbvralvw 3245	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
303		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑚 ∈ (𝐼 ∖ 𝑖))
304	303	eldifbd 3919	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ¬ 𝑚 ∈ 𝑖)
305		disjsn 4679	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∩ {𝑚}) = ∅ ↔ ¬ 𝑚 ∈ 𝑖)
306	304, 305	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∩ {𝑚}) = ∅)
307		undif5 4447	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∩ {𝑚}) = ∅ → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
308	306, 307	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
309	308	eqcomd 2771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 = ((𝑖 ∪ {𝑚}) ∖ {𝑚}))
310	309	oveq2d 7432	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝐵 ↑m 𝑖) = (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚})))
311		oveq2 7424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((♯‘𝑖) − 𝑘) = ((♯‘𝑖) − 𝑙))
312	311	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)))
313		oveq1 7423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
314		2fveq3 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)))
315	314	fveq1d 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))
316	313, 315	oveq12d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
317	312, 316	eqeq12d 2781	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))))
318	317	cbvralvw 3245	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
319	309	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (♯‘𝑖) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
320	319	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (0...(♯‘𝑖)) = (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))))
321		2fveq3 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑦‘𝑛)) = (𝐴‘(𝑦‘𝑜)))
322	321	oveq2d 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑦‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑜))))
323	322	cbvmptv 5217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))
324	309	mpteq1d 5203	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
325	323, 324	eqtrid 2812	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
326	325	oveq2d 7432	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))
327	326	fveq2d 6889	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))))
328	319	oveq1d 7431	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((♯‘𝑖) − 𝑙) = ((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙))
329	327, 328	fveq12d 6892	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)))
330	309	oveq1d 7431	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅))
331	309	oveq1d 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅))
332	331	fveq1d 6887	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖eSymPoly𝑅)‘𝑙) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))
333	330, 332	fveq12d 6892	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙)))
334	333	fveq1d 6887	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦) = (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))
335	334	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
336	329, 335	eqeq12d 2781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
337	320, 336	raleqbidv 3340	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
338	318, 337	bitrid 286	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
339	310, 338	raleqbidv 3340	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
340	302, 339	bitrid 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
341	340	biimpa 482	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
342	341	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
343		eqid 2765	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)
344		eqid 2765	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)
345		eqid 2765	. . . . . . . . . 10 ⊢ (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))
346		difssd 4091	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ⊆ (𝑖 ∪ {𝑚}))
347	275, 346	ssfid 9232	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ∈ Fin)
348	279, 346	fssresd 6749	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚})):((𝑖 ∪ {𝑚}) ∖ {𝑚})⟶𝐵)
349		eqid 2765	. . . . . . . . . 10 ⊢ (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))
350		eqid 2765	. . . . . . . . . 10 ⊢ (deg1‘𝑅) = (deg1‘𝑅)
351	228, 23, 263, 229, 343, 344, 119, 114, 113, 266, 267, 125, 345, 347, 276, 348, 349, 350	vietadeg1 33991	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((deg1‘𝑅)‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
352	228, 23, 263, 229, 264, 265, 119, 114, 113, 266, 267, 125, 268, 275, 276, 279, 283, 285, 289, 290, 342, 351	vietalem 33992	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)))
353	269	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝐼 ∈ Fin)
354		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ⊆ 𝐼)
355	353, 354	ssfid 9232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ∈ Fin)
356	273	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → {𝑚} ∈ Fin)
357	355, 356	unfid 9159	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∪ {𝑚}) ∈ Fin)
358	357	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
359		hashcl 14405	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∪ {𝑚}) ∈ Fin → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
360	358, 359	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
361	360	nn0cnd 12578	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℂ)
362		elfznn0 13660	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → 𝑘 ∈ ℕ0)
363	362	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℕ0)
364	363	nn0cnd 12578	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℂ)
365	361, 364	nncand 11585	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = 𝑘)
366	365	oveq1d 7431	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
367	365	fveq2d 6889	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
368	367	fveq2d 6889	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
369	368	fveq1d 6887	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
370	366, 369	oveq12d 7434	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
371	370	ad4ant14 765	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
372	352, 371	eqtrd 2800	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
373	262, 372	ralrimia 3266	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) → ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
374	257, 373	ralrimia 3266	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
375	374	ex 418	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
376	375	anasss 472	. . 3 ⊢ ((𝜑 ∧ (𝑖 ⊆ 𝐼 ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
377	55, 72, 89, 112, 254, 376, 269	findcard2d 9154	. 2 ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑m 𝐼)∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
378	24	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
379		vieta.z	. . 3 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
380	378, 269, 379	elmapdd 8840	. 2 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m 𝐼))
381		vieta.k	. 2 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
382	14, 21, 377, 380, 381	rspc2dv 3598	1 ⊢ (𝜑 → (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  {crab 3418  Vcvv 3457   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  ifcif 4489  𝒫 cpw 4564  {csn 4591  {cpr 4593  ⟨cop 4597   class class class wbr 5111   ↦ cmpt 5194   × cxp 5661  ^◡ccnv 5662   ↾ cres 5665   “ cima 5666   ∘ ccom 5667   Fn wfn 6535  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7416   ↑_m cmap 8826  Fincfn 8945   finSupp cfsupp 9324  0cc0 11111  1c1 11112   − cmin 11452  𝟭cind 12229  ℕcn 12244  ℕ₀cn0 12515  ℤcz 12602  ...cfz 13546  ♯chash 14379  Basecbs 17286  ._rcmulr 17328  0_gc0g 17509   Σ_g cgsu 17510  inv_gcminusg 19024  -_gcsg 19025  ._gcmg 19156  mulGrpcmgp 20239  1_rcur 20286  Ringcrg 20338   RingHom crh 20576  IDomncidom 20821  ℤ_ringczring 21625  ℤRHomczrh 21678  algSccascl 22031   mPoly cmpl 22085   eval cevl 22253  var₁cv1 22365  Poly₁cpl1 22366  coe₁cco1 22367  deg₁cdg1 26240  eSymPolycesply 33969

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-inf2 9613  ax-cnex 11167  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188  ax-pre-sup 11189  ax-addf 11190  ax-mulf 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7680  df-ofr 7681  df-om 7865  df-1st 7988  df-2nd 7989  df-supp 8159  df-tpos 8224  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-er 8696  df-map 8828  df-pm 8829  df-ixp 8898  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-fsupp 9325  df-sup 9405  df-oi 9475  df-dju 9899  df-card 9937  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455  df-div 11883  df-ind 12230  df-nn 12245  df-2 12314  df-3 12315  df-4 12316  df-5 12317  df-6 12318  df-7 12319  df-8 12320  df-9 12321  df-n0 12516  df-xnn0 12589  df-z 12603  df-dec 12723  df-uz 12874  df-rp 13028  df-fz 13547  df-fzo 13695  df-seq 14051  df-exp 14111  df-fac 14323  df-bc 14352  df-hash 14380  df-cj 15169  df-re 15170  df-im 15171  df-sqrt 15305  df-abs 15306  df-clim 15558  df-sum 15757  df-struct 17224  df-sets 17241  df-slot 17259  df-ndx 17271  df-base 17287  df-ress 17308  df-plusg 17340  df-mulr 17341  df-starv 17342  df-sca 17343  df-vsca 17344  df-ip 17345  df-tset 17346  df-ple 17347  df-ds 17349  df-unif 17350  df-hom 17351  df-cco 17352  df-0g 17511  df-gsum 17512  df-prds 17517  df-pws 17519  df-mre 17655  df-mrc 17656  df-acs 17658  df-mgm 18715  df-sgrp 18798  df-mnd 18814  df-mhm 18864  df-submnd 18865  df-grp 19026  df-minusg 19027  df-sbg 19028  df-mulg 19157  df-subg 19212  df-ghm 19307  df-cntz 19410  df-cmn 19875  df-abl 19876  df-mgp 20240  df-rng 20254  df-ur 20287  df-srg 20292  df-ring 20340  df-cring 20341  df-oppr 20444  df-dvdsr 20464  df-unit 20465  df-invr 20495  df-rhm 20579  df-nzr 20639  df-subrng 20674  df-subrg 20698  df-rlreg 20822  df-domn 20823  df-idom 20824  df-lmod 21012  df-lss 21082  df-lsp 21122  df-cnfld 21552  df-zring 21626  df-zrh 21682  df-assa 22032  df-asp 22033  df-ascl 22034  df-psr 22088  df-mvr 22089  df-mpl 22090  df-opsr 22092  df-evls 22254  df-evl 22255  df-psr1 22369  df-vr1 22370  df-ply1 22371  df-coe1 22372  df-mdeg 26241  df-deg1 26242  df-extv 33943  df-esply 33971

This theorem is used by: (None)