Theorem vieta 33911

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 26438 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 6878	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧‘𝑛) = (𝑍‘𝑛))
2	1	fveq2d 6883	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑍‘𝑛)))
3	2	oveq2d 7424	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
4	3	mpteq2dv 5206	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
5	4	oveq2d 7424	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
6		vieta.f	. . . . . . 7 ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
7	5, 6	eqtr4di 2822	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = 𝐹)
8	7	fveq2d 6883	. . . . 5 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘𝐹))
9		vieta.c	. . . . 5 ⊢ 𝐶 = (coe1‘𝐹)
10	8, 9	eqtr4di 2822	. . . 4 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = 𝐶)
11	10	fveq1d 6881	. . 3 ⊢ (𝑧 = 𝑍 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝑘)))
12		fveq2 6879	. . . 4 ⊢ (𝑧 = 𝑍 → ((𝑄‘(𝐸‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑍))
13	12	oveq2d 7424	. . 3 ⊢ (𝑧 = 𝑍 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)))
14	11, 13	eqeq12d 2785	. 2 ⊢ (𝑧 = 𝑍 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) ↔ (𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))))
15		oveq2 7416	. . . 4 ⊢ (𝑘 = 𝐾 → (𝐻 − 𝑘) = (𝐻 − 𝐾))
16	15	fveq2d 6883	. . 3 ⊢ (𝑘 = 𝐾 → (𝐶‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝐾)))
17		oveq1 7415	. . . 4 ⊢ (𝑘 = 𝐾 → (𝑘 ↑ (𝑁‘ 1 )) = (𝐾 ↑ (𝑁‘ 1 )))
18		2fveq3 6884	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝐾)))
19	18	fveq1d 6881	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝐾))‘𝑍))
20	17, 19	oveq12d 7426	. . 3 ⊢ (𝑘 = 𝐾 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))
21	16, 20	eqeq12d 2785	. 2 ⊢ (𝑘 = 𝐾 → ((𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ↔ (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍))))
22		oveq2 7416	. . . . 5 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = (𝐵 ↑m ∅))
23		vieta.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
24	23	fvexi 6893	. . . . . 6 ⊢ 𝐵 ∈ V
25		mapdm0 8835	. . . . . 6 ⊢ (𝐵 ∈ V → (𝐵 ↑m ∅) = {∅})
26	24, 25	ax-mp 5	. . . . 5 ⊢ (𝐵 ↑m ∅) = {∅}
27	22, 26	eqtrdi 2820	. . . 4 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = {∅})
28		fveq2 6879	. . . . . . 7 ⊢ (𝑗 = ∅ → (♯‘𝑗) = (♯‘∅))
29	28	oveq2d 7424	. . . . . 6 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = (0...(♯‘∅)))
30		hash0 14399	. . . . . . . 8 ⊢ (♯‘∅) = 0
31	30	oveq2i 7419	. . . . . . 7 ⊢ (0...(♯‘∅)) = (0...0)
32		fz0sn 13651	. . . . . . 7 ⊢ (0...0) = {0}
33	31, 32	eqtri 2792	. . . . . 6 ⊢ (0...(♯‘∅)) = {0}
34	29, 33	eqtrdi 2820	. . . . 5 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = {0})
35		mpteq1 5201	. . . . . . . . . . 11 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
36		mpt0 6675	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅
37	35, 36	eqtrdi 2820	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅)
38	37	oveq2d 7424	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg ∅))
39		eqid 2769	. . . . . . . . . 10 ⊢ (0g‘𝑀) = (0g‘𝑀)
40	39	gsum0 18738	. . . . . . . . 9 ⊢ (𝑀 Σg ∅) = (0g‘𝑀)
41	38, 40	eqtrdi 2820	. . . . . . . 8 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (0g‘𝑀))
42	41	fveq2d 6883	. . . . . . 7 ⊢ (𝑗 = ∅ → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(0g‘𝑀)))
43	28	oveq1d 7423	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = ((♯‘∅) − 𝑘))
44	30	oveq1i 7418	. . . . . . . 8 ⊢ ((♯‘∅) − 𝑘) = (0 − 𝑘)
45	43, 44	eqtrdi 2820	. . . . . . 7 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = (0 − 𝑘))
46	42, 45	fveq12d 6886	. . . . . 6 ⊢ (𝑗 = ∅ → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(0g‘𝑀))‘(0 − 𝑘)))
47		oveq1 7415	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑗 eval 𝑅) = (∅ eval 𝑅))
48		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑗eSymPoly𝑅) = (∅eSymPoly𝑅))
49	48	fveq1d 6881	. . . . . . . . 9 ⊢ (𝑗 = ∅ → ((𝑗eSymPoly𝑅)‘𝑘) = ((∅eSymPoly𝑅)‘𝑘))
50	47, 49	fveq12d 6886	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)))
51	50	fveq1d 6881	. . . . . . 7 ⊢ (𝑗 = ∅ → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))
52	51	oveq2d 7424	. . . . . 6 ⊢ (𝑗 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
53	46, 52	eqeq12d 2785	. . . . 5 ⊢ (𝑗 = ∅ → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
54	34, 53	raleqbidv 3345	. . . 4 ⊢ (𝑗 = ∅ → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
55	27, 54	raleqbidv 3345	. . 3 ⊢ (𝑗 = ∅ → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
56		oveq2 7416	. . . 4 ⊢ (𝑗 = 𝑖 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝑖))
57		fveq2 6879	. . . . . 6 ⊢ (𝑗 = 𝑖 → (♯‘𝑗) = (♯‘𝑖))
58	57	oveq2d 7424	. . . . 5 ⊢ (𝑗 = 𝑖 → (0...(♯‘𝑗)) = (0...(♯‘𝑖)))
59		mpteq1 5201	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
60	59	oveq2d 7424	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
61	60	fveq2d 6883	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
62	57	oveq1d 7423	. . . . . . 7 ⊢ (𝑗 = 𝑖 → ((♯‘𝑗) − 𝑘) = ((♯‘𝑖) − 𝑘))
63	61, 62	fveq12d 6886	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
64		oveq1 7415	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑗 eval 𝑅) = (𝑖 eval 𝑅))
65		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗eSymPoly𝑅) = (𝑖eSymPoly𝑅))
66	65	fveq1d 6881	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → ((𝑗eSymPoly𝑅)‘𝑘) = ((𝑖eSymPoly𝑅)‘𝑘))
67	64, 66	fveq12d 6886	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)))
68	67	fveq1d 6881	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
69	68	oveq2d 7424	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
70	63, 69	eqeq12d 2785	. . . . 5 ⊢ (𝑗 = 𝑖 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
71	58, 70	raleqbidv 3345	. . . 4 ⊢ (𝑗 = 𝑖 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
72	56, 71	raleqbidv 3345	. . 3 ⊢ (𝑗 = 𝑖 → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
73		oveq2 7416	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝐵 ↑m 𝑗) = (𝐵 ↑m (𝑖 ∪ {𝑚})))
74		fveq2 6879	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (♯‘𝑗) = (♯‘(𝑖 ∪ {𝑚})))
75	74	oveq2d 7424	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (0...(♯‘𝑗)) = (0...(♯‘(𝑖 ∪ {𝑚}))))
76		mpteq1 5201	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
77	76	oveq2d 7424	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
78	77	fveq2d 6883	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
79	74	oveq1d 7423	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((♯‘𝑗) − 𝑘) = ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))
80	78, 79	fveq12d 6886	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))
81		oveq1 7415	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗 eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅))
82		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅))
83	82	fveq1d 6881	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗eSymPoly𝑅)‘𝑘) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
84	81, 83	fveq12d 6886	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
85	84	fveq1d 6881	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
86	85	oveq2d 7424	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
87	80, 86	eqeq12d 2785	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
88	75, 87	raleqbidv 3345	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
89	73, 88	raleqbidv 3345	. . 3 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
90		oveq2 7416	. . . 4 ⊢ (𝑗 = 𝐼 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝐼))
91		fveq2 6879	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = (♯‘𝐼))
92		vieta.h	. . . . . . 7 ⊢ 𝐻 = (♯‘𝐼)
93	91, 92	eqtr4di 2822	. . . . . 6 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = 𝐻)
94	93	oveq2d 7424	. . . . 5 ⊢ (𝑗 = 𝐼 → (0...(♯‘𝑗)) = (0...𝐻))
95		mpteq1 5201	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
96	95	oveq2d 7424	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
97	96	fveq2d 6883	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
98	93	oveq1d 7423	. . . . . . 7 ⊢ (𝑗 = 𝐼 → ((♯‘𝑗) − 𝑘) = (𝐻 − 𝑘))
99	97, 98	fveq12d 6886	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)))
100		oveq1 7415	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = (𝐼 eval 𝑅))
101		vieta.q	. . . . . . . . . 10 ⊢ 𝑄 = (𝐼 eval 𝑅)
102	100, 101	eqtr4di 2822	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = 𝑄)
103		oveq1 7415	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = (𝐼eSymPoly𝑅))
104		vieta.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
105	103, 104	eqtr4di 2822	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = 𝐸)
106	105	fveq1d 6881	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → ((𝑗eSymPoly𝑅)‘𝑘) = (𝐸‘𝑘))
107	102, 106	fveq12d 6886	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (𝑄‘(𝐸‘𝑘)))
108	107	fveq1d 6881	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑧))
109	108	oveq2d 7424	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
110	99, 109	eqeq12d 2785	. . . . 5 ⊢ (𝑗 = 𝐼 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
111	94, 110	raleqbidv 3345	. . . 4 ⊢ (𝑗 = 𝐼 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
112	90, 111	raleqbidv 3345	. . 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 20808	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
117	23, 114, 116	ringidcld 20345	. . . . . 6 ⊢ (𝜑 → 1 ∈ 𝐵)
118	23, 113, 114, 116, 117	ringlidmd 20351	. . . . 5 ⊢ (𝜑 → ( 1 · 1 ) = 1 )
119		vieta.n	. . . . . . . 8 ⊢ 𝑁 = (invg‘𝑅)
120	116	ringgrpd 20320	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
121	23, 119, 120, 117	grpinvcld 19051	. . . . . . 7 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
122		eqid 2769	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
123	122, 23	mgpbas 20217	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
124	122, 114	ringidval 20261	. . . . . . . 8 ⊢ 1 = (0g‘(mulGrp‘𝑅))
125		vieta.p	. . . . . . . 8 ⊢ ↑ = (.g‘(mulGrp‘𝑅))
126	123, 124, 125	mulg0 19136	. . . . . . 7 ⊢ ((𝑁‘ 1 ) ∈ 𝐵 → (0 ↑ (𝑁‘ 1 )) = 1 )
127	121, 126	syl 18	. . . . . 6 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) = 1 )
128		eqid 2769	. . . . . . . . . . . . . . 15 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
129	128, 114	zrh1 21627	. . . . . . . . . . . . . 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 5689	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = ({∅} × { 1 }))
133		0ex 5269	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
134	133	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ V)
135	114	fvexi 6893	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
136	135	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ V)
137		xpsng 7133	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ 1 ∈ V) → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
138	134, 136, 137	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
139		0xp 5758	. . . . . . . . . . . . . . . 16 ⊢ (∅ × {0}) = ∅
140	139	eqcomi 2778	. . . . . . . . . . . . . . 15 ⊢ ∅ = (∅ × {0})
141	140	eqeq2i 2782	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ∅ ↔ 𝑓 = (∅ × {0}))
142	141	bilani 509	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 = ∅) → 𝑓 = (∅ × {0}))
143	142	iftrued 4497	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 = ∅) → if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅)) = 1 )
144	143, 134, 136	fmptsnd 7165	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨∅, 1 ⟩} = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
145	132, 138, 144	3eqtrd 2808	. . . . . . . . . 10 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
146		elsni 4608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ {∅} → ℎ = ∅)
147		nn0ex 12506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ∈ V
148		mapdm0 8835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ0 ∈ V → (ℕ0 ↑m ∅) = {∅})
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℕ0 ↑m ∅) = {∅}
150	146, 149	eleq2s 2887	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ℎ = ∅)
151	150	cnveqd 5859	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ◡ℎ = ◡∅)
152	151	imaeq1d 6059	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = (◡∅ “ ℕ))
153		cnv0 5867	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡∅ = ∅
154	153	imaeq1i 6057	. . . . . . . . . . . . . . . . . 18 ⊢ (◡∅ “ ℕ) = (∅ “ ℕ)
155		0ima 6078	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ “ ℕ) = ∅
156	154, 155	eqtri 2792	. . . . . . . . . . . . . . . . 17 ⊢ (◡∅ “ ℕ) = ∅
157	152, 156	eqtrdi 2820	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = ∅)
158		0fi 9035	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Fin
159	157, 158	eqeltrdi 2877	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) ∈ Fin)
160	159	rabeqc 3435	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin} = (ℕ0 ↑m ∅)
161	160, 149	eqtr2i 2793	. . . . . . . . . . . . 13 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
162		eqid 2769	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
163	162	psrbasfsupp 33842	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
164	161, 163	eqtr4i 2795	. . . . . . . . . . . 12 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
165		0nn0 12515	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
166	165	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ0)
167	164, 134, 115, 166	esplyfval 33894	. . . . . . . . . . 11 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))))
168		fveqeq2 6888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ∅ → ((♯‘𝑐) = 0 ↔ (♯‘∅) = 0))
169		0elpw 5324	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 ∅
170	169	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ ∈ 𝒫 ∅)
171	30	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘∅) = 0)
172		hasheq0 14395	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ 𝒫 ∅ → ((♯‘𝑐) = 0 ↔ 𝑐 = ∅))
173	172	biimpa 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ 𝒫 ∅ ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
174	173	adantll 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝒫 ∅) ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
175	168, 170, 171, 174	rabeqsnd 4637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0} = {∅})
176	175	imaeq2d 6060	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = ((𝟭‘∅) “ {∅}))
177		pw0 4779	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∅ = {∅}
178	177	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝒫 ∅ = {∅})
179		indf1o 33121	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ V → (𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅))
180		f1of 6818	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅) → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
181	134, 179, 180	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
182	178, 181	feq2dd 6689	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝟭‘∅):{∅}⟶({0, 1} ↑m ∅))
183	182	ffnd 6704	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝟭‘∅) Fn {∅})
184	133	snid 4630	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ {∅}
185	184	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∅ ∈ {∅})
186	183, 185	fnimasnd 7361	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {∅}) = {((𝟭‘∅)‘∅)})
187		ssidd 3968	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∅ ⊆ ∅)
188		indf 12220	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ V ∧ ∅ ⊆ ∅) → ((𝟭‘∅)‘∅):∅⟶{0, 1})
189	134, 187, 188	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝟭‘∅)‘∅):∅⟶{0, 1})
190		f0bi 6759	. . . . . . . . . . . . . . . . 17 ⊢ (((𝟭‘∅)‘∅):∅⟶{0, 1} ↔ ((𝟭‘∅)‘∅) = ∅)
191	189, 190	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝟭‘∅)‘∅) = ∅)
192	191	sneqd 4603	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {((𝟭‘∅)‘∅)} = {∅})
193	176, 186, 192	3eqtrd 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = {∅})
194	193	fveq2d 6883	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ((𝟭‘{∅})‘{∅}))
195		p0ex 5353	. . . . . . . . . . . . . 14 ⊢ {∅} ∈ V
196		indconst1 12227	. . . . . . . . . . . . . 14 ⊢ ({∅} ∈ V → ((𝟭‘{∅})‘{∅}) = ({∅} × {1}))
197	195, 196	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝟭‘{∅})‘{∅}) = ({∅} × {1})
198	194, 197	eqtrdi 2820	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ({∅} × {1}))
199	198	coeq2d 5846	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))) = ((ℤRHom‘𝑅) ∘ ({∅} × {1})))
200	128	zrhrhm 21626	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
201		zringbas 21568	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤring)
202	201, 23	rhmf 20562	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
203	116, 200, 202	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝑅):ℤ⟶𝐵)
204	203	ffnd 6704	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤRHom‘𝑅) Fn ℤ)
205		1zzd 12621	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
206		fcoconst 7128	. . . . . . . . . . . 12 ⊢ (((ℤRHom‘𝑅) Fn ℤ ∧ 1 ∈ ℤ) → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
207	204, 205, 206	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
208	167, 199, 207	3eqtrd 2808	. . . . . . . . . 10 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
209		eqid 2769	. . . . . . . . . . 11 ⊢ (∅ mPoly 𝑅) = (∅ mPoly 𝑅)
210		eqid 2769	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
211		eqid 2769	. . . . . . . . . . 11 ⊢ (algSc‘(∅ mPoly 𝑅)) = (algSc‘(∅ mPoly 𝑅))
212	209, 161, 210, 23, 211, 134, 116, 117	mplascl 22180	. . . . . . . . . 10 ⊢ (𝜑 → ((algSc‘(∅ mPoly 𝑅))‘ 1 ) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
213	145, 208, 212	3eqtr4d 2814	. . . . . . . . 9 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((algSc‘(∅ mPoly 𝑅))‘ 1 ))
214	213	fveq2d 6883	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)) = ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )))
215	214	fveq1d 6881	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅))
216		eqid 2769	. . . . . . . . 9 ⊢ (∅ eval 𝑅) = (∅ eval 𝑅)
217	184, 149	eleqtrri 2868	. . . . . . . . . 10 ⊢ ∅ ∈ (ℕ0 ↑m ∅)
218	217	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ (ℕ0 ↑m ∅))
219	115	idomcringd 20807	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
220	216, 209, 23, 211, 218, 219, 117	evlsca 22222	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )) = ((𝐵 ↑m ∅) × { 1 }))
221	220	fveq1d 6881	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅) = (((𝐵 ↑m ∅) × { 1 })‘∅))
222	184, 26	eleqtrri 2868	. . . . . . . 8 ⊢ ∅ ∈ (𝐵 ↑m ∅)
223	135	fvconst2 7200	. . . . . . . 8 ⊢ (∅ ∈ (𝐵 ↑m ∅) → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
224	222, 223	mp1i 14	. . . . . . 7 ⊢ (𝜑 → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
225	215, 221, 224	3eqtrd 2808	. . . . . 6 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = 1 )
226	127, 225	oveq12d 7426	. . . . 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 2769	. . . . . . . . . 10 ⊢ (1r‘𝑊) = (1r‘𝑊)
231	229, 230	ringidval 20261	. . . . . . . . 9 ⊢ (1r‘𝑊) = (0g‘𝑀)
232	231	eqcomi 2778	. . . . . . . 8 ⊢ (0g‘𝑀) = (1r‘𝑊)
233	228, 232, 210, 114	coe1id 22419	. . . . . . 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 7012	. . . . 5 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = 1 )
236	118, 226, 235	3eqtr4rd 2815	. . . 4 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
237		fveq2 6879	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))
238	237	oveq2d 7424	. . . . . . . 8 ⊢ (𝑧 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)))
239	238	eqeq2d 2780	. . . . . . 7 ⊢ (𝑧 = ∅ → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
240	239	ralbidv 3194	. . . . . 6 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
241		c0ex 11196	. . . . . . 7 ⊢ 0 ∈ V
242		oveq2 7416	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (0 − 𝑘) = (0 − 0))
243		0m0e0 12355	. . . . . . . . . 10 ⊢ (0 − 0) = 0
244	242, 243	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝑘 = 0 → (0 − 𝑘) = 0)
245	244	fveq2d 6883	. . . . . . . 8 ⊢ (𝑘 = 0 → ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((coe1‘(0g‘𝑀))‘0))
246		oveq1 7415	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
247		2fveq3 6884	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)))
248	247	fveq1d 6881	. . . . . . . . 9 ⊢ (𝑘 = 0 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))
249	246, 248	oveq12d 7426	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
250	245, 249	eqeq12d 2785	. . . . . . 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 1941	. . . . . . 7 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
256		nfra1 3295	. . . . . . 7 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
257	255, 256	nfan 1926	. . . . . 6 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
258		nfv 1941	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
259		nfra2w 3307	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
260	258, 259	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
261		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))
262	260, 261	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
263		vieta.3	. . . . . . . . 9 ⊢ − = (-g‘𝑊)
264		eqid 2769	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅)
265		eqid 2769	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚})eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅)
266		vieta.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑅)
267		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
268		eqid 2769	. . . . . . . . 9 ⊢ (♯‘(𝑖 ∪ {𝑚})) = (♯‘(𝑖 ∪ {𝑚}))
269		vieta.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
270	269	ad5antr 746	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝐼 ∈ Fin)
271		simp-5r 797	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ⊆ 𝐼)
272	270, 271	ssfid 9225	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ∈ Fin)
273		snfi 9036	. . . . . . . . . . 11 ⊢ {𝑚} ∈ Fin
274	273	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → {𝑚} ∈ Fin)
275	272, 274	unfid 9152	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
276	115	ad5antr 746	. . . . . . . . 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 780	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
279	275, 277, 278	elmaprd 32962	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧:(𝑖 ∪ {𝑚})⟶𝐵)
280		2fveq3 6884	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑧‘𝑜)))
281	280	oveq2d 7424	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑧‘𝑜))))
282	281	cbvmptv 5216	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜))))
283	282	oveq2i 7419	. . . . . . . . 9 ⊢ (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜)))))
284		fznn0sub2 13659	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
285	284	adantl 486	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
286		ssun2 4140	. . . . . . . . . . 11 ⊢ {𝑚} ⊆ (𝑖 ∪ {𝑚})
287		vsnid 4631	. . . . . . . . . . 11 ⊢ 𝑚 ∈ {𝑚}
288	286, 287	sselii 3942	. . . . . . . . . 10 ⊢ 𝑚 ∈ (𝑖 ∪ {𝑚})
289	288	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑚 ∈ (𝑖 ∪ {𝑚}))
290		eqid 2769	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = ((𝑖 ∪ {𝑚}) ∖ {𝑚})
291		fveq1 6878	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑦 → (𝑧‘𝑛) = (𝑦‘𝑛))
292	291	fveq2d 6883	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑦 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑦‘𝑛)))
293	292	oveq2d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑛))))
294	293	mpteq2dv 5206	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))
295	294	oveq2d 7424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))
296	295	fveq2d 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))))
297	296	fveq1d 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
298		fveq2 6879	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))
299	298	oveq2d 7424	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
300	297, 299	eqeq12d 2785	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
301	300	ralbidv 3194	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
302	301	cbvralvw 3249	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
303		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑚 ∈ (𝐼 ∖ 𝑖))
304	303	eldifbd 3926	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ¬ 𝑚 ∈ 𝑖)
305		disjsn 4679	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∩ {𝑚}) = ∅ ↔ ¬ 𝑚 ∈ 𝑖)
306	304, 305	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∩ {𝑚}) = ∅)
307		undif5 4447	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∩ {𝑚}) = ∅ → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
308	306, 307	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
309	308	eqcomd 2775	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 = ((𝑖 ∪ {𝑚}) ∖ {𝑚}))
310	309	oveq2d 7424	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝐵 ↑m 𝑖) = (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚})))
311		oveq2 7416	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((♯‘𝑖) − 𝑘) = ((♯‘𝑖) − 𝑙))
312	311	fveq2d 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)))
313		oveq1 7415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
314		2fveq3 6884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)))
315	314	fveq1d 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))
316	313, 315	oveq12d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
317	312, 316	eqeq12d 2785	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))))
318	317	cbvralvw 3249	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
319	309	fveq2d 6883	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (♯‘𝑖) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
320	319	oveq2d 7424	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (0...(♯‘𝑖)) = (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))))
321		2fveq3 6884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑦‘𝑛)) = (𝐴‘(𝑦‘𝑜)))
322	321	oveq2d 7424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑦‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑜))))
323	322	cbvmptv 5216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))
324	309	mpteq1d 5202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
325	323, 324	eqtrid 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
326	325	oveq2d 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))
327	326	fveq2d 6883	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))))
328	319	oveq1d 7423	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((♯‘𝑖) − 𝑙) = ((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙))
329	327, 328	fveq12d 6886	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)))
330	309	oveq1d 7423	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅))
331	309	oveq1d 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅))
332	331	fveq1d 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖eSymPoly𝑅)‘𝑙) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))
333	330, 332	fveq12d 6886	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙)))
334	333	fveq1d 6881	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦) = (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))
335	334	oveq2d 7424	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
336	329, 335	eqeq12d 2785	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
337	320, 336	raleqbidv 3345	. . . . . . . . . . . . . 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 3345	. . . . . . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
342	341	ad2antrr 738	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
343		eqid 2769	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)
344		eqid 2769	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)
345		eqid 2769	. . . . . . . . . 10 ⊢ (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))
346		difssd 4099	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ⊆ (𝑖 ∪ {𝑚}))
347	275, 346	ssfid 9225	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ∈ Fin)
348	279, 346	fssresd 6743	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚})):((𝑖 ∪ {𝑚}) ∖ {𝑚})⟶𝐵)
349		eqid 2769	. . . . . . . . . 10 ⊢ (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))
350		eqid 2769	. . . . . . . . . 10 ⊢ (deg1‘𝑅) = (deg1‘𝑅)
351	228, 23, 263, 229, 343, 344, 119, 114, 113, 266, 267, 125, 345, 347, 276, 348, 349, 350	vietadeg1 33909	. . . . . . . . 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 33910	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)))
353	269	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝐼 ∈ Fin)
354		simplr 780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ⊆ 𝐼)
355	353, 354	ssfid 9225	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ∈ Fin)
356	273	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → {𝑚} ∈ Fin)
357	355, 356	unfid 9152	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∪ {𝑚}) ∈ Fin)
358	357	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
359		hashcl 14388	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∪ {𝑚}) ∈ Fin → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
360	358, 359	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
361	360	nn0cnd 12563	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℂ)
362		elfznn0 13644	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → 𝑘 ∈ ℕ0)
363	362	adantl 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℕ0)
364	363	nn0cnd 12563	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℂ)
365	361, 364	nncand 11570	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = 𝑘)
366	365	oveq1d 7423	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
367	365	fveq2d 6883	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
368	367	fveq2d 6883	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
369	368	fveq1d 6881	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
370	366, 369	oveq12d 7426	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
371	370	ad4ant14 764	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
372	352, 371	eqtrd 2804	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
373	262, 372	ralrimia 3270	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) → ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
374	257, 373	ralrimia 3270	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
375	374	ex 417	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
376	375	anasss 471	. . 3 ⊢ ((𝜑 ∧ (𝑖 ⊆ 𝐼 ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
377	55, 72, 89, 112, 254, 376, 269	findcard2d 9147	. 2 ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑m 𝐼)∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
378	24	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
379		vieta.z	. . 3 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
380	378, 269, 379	elmapdd 8834	. 2 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m 𝐼))
381		vieta.k	. 2 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
382	14, 21, 377, 380, 381	rspc2dv 3605	1 ⊢ (𝜑 → (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  {crab 3423  Vcvv 3463   ∖ cdif 3910   ∪ cun 3911   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  ifcif 4489  𝒫 cpw 4564  {csn 4591  {cpr 4593  ⟨cop 4597   class class class wbr 5110   ↦ cmpt 5193   × cxp 5657  ^◡ccnv 5658   ↾ cres 5661   “ cima 5662   ∘ ccom 5663   Fn wfn 6528  ⟶wf 6529  –1-1-onto→wf1o 6532  ‘cfv 6533  (class class class)co 7408   ↑_m cmap 8820  Fincfn 8939   finSupp cfsupp 9317  0cc0 11096  1c1 11097   − cmin 11437  𝟭cind 12214  ℕcn 12229  ℕ₀cn0 12500  ℤcz 12587  ...cfz 13531  ♯chash 14362  Basecbs 17265  ._rcmulr 17307  0_gc0g 17488   Σ_g cgsu 17489  inv_gcminusg 18997  -_gcsg 18998  ._gcmg 19129  mulGrpcmgp 20212  1_rcur 20259  Ringcrg 20311   RingHom crh 20547  IDomncidom 20774  ℤ_ringczring 21561  ℤRHomczrh 21614  algSccascl 21967   mPoly cmpl 22021   eval cevl 22189  var₁cv1 22301  Poly₁cpl1 22302  coe₁cco1 22303  deg₁cdg1 26176  eSymPolycesply 33887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-inf2 9606  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173  ax-pre-sup 11174  ax-addf 11175  ax-mulf 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4874  df-int 4914  df-iun 4959  df-iin 4960  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-of 7672  df-ofr 7673  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-tpos 8218  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-oadd 8453  df-er 8690  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-sup 9398  df-oi 9468  df-dju 9883  df-card 9921  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440  df-div 11868  df-ind 12215  df-nn 12230  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304  df-8 12305  df-9 12306  df-n0 12501  df-xnn0 12574  df-z 12588  df-dec 12708  df-uz 12859  df-rp 13013  df-fz 13532  df-fzo 13679  df-seq 14034  df-exp 14094  df-fac 14306  df-bc 14335  df-hash 14363  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-clim 15535  df-sum 15734  df-struct 17203  df-sets 17220  df-slot 17238  df-ndx 17250  df-base 17266  df-ress 17287  df-plusg 17319  df-mulr 17320  df-starv 17321  df-sca 17322  df-vsca 17323  df-ip 17324  df-tset 17325  df-ple 17326  df-ds 17328  df-unif 17329  df-hom 17330  df-cco 17331  df-0g 17490  df-gsum 17491  df-prds 17496  df-pws 17498  df-mre 17634  df-mrc 17635  df-acs 17637  df-mgm 18694  df-sgrp 18773  df-mnd 18789  df-mhm 18837  df-submnd 18838  df-grp 18999  df-minusg 19000  df-sbg 19001  df-mulg 19130  df-subg 19185  df-ghm 19280  df-cntz 19383  df-cmn 19848  df-abl 19849  df-mgp 20213  df-rng 20227  df-ur 20260  df-srg 20265  df-ring 20313  df-cring 20314  df-oppr 20415  df-dvdsr 20435  df-unit 20436  df-invr 20466  df-rhm 20550  df-nzr 20592  df-subrng 20627  df-subrg 20651  df-rlreg 20775  df-domn 20776  df-idom 20777  df-lmod 20957  df-lss 21027  df-lsp 21067  df-cnfld 21488  df-zring 21562  df-zrh 21618  df-assa 21968  df-asp 21969  df-ascl 21970  df-psr 22024  df-mvr 22025  df-mpl 22026  df-opsr 22028  df-evls 22190  df-evl 22191  df-psr1 22305  df-vr1 22306  df-ply1 22307  df-coe1 22308  df-mdeg 26177  df-deg1 26178  df-extv 33861  df-esply 33889

This theorem is referenced by: (None)