Theorem vieta 34205

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 26628 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 6882	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧‘𝑛) = (𝑍‘𝑛))
2	1	fveq2d 6887	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑍‘𝑛)))
3	2	oveq2d 7434	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
4	3	mpteq2dv 5199	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
5	4	oveq2d 7434	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
6		vieta.f	. . . . . . 7 ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
7	5, 6	eqtr4di 2814	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = 𝐹)
8	7	fveq2d 6887	. . . . 5 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘𝐹))
9		vieta.c	. . . . 5 ⊢ 𝐶 = (coe1‘𝐹)
10	8, 9	eqtr4di 2814	. . . 4 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = 𝐶)
11	10	fveq1d 6885	. . 3 ⊢ (𝑧 = 𝑍 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝑘)))
12		fveq2 6883	. . . 4 ⊢ (𝑧 = 𝑍 → ((𝑄‘(𝐸‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑍))
13	12	oveq2d 7434	. . 3 ⊢ (𝑧 = 𝑍 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)))
14	11, 13	eqeq12d 2777	. 2 ⊢ (𝑧 = 𝑍 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) ↔ (𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))))
15		oveq2 7426	. . . 4 ⊢ (𝑘 = 𝐾 → (𝐻 − 𝑘) = (𝐻 − 𝐾))
16	15	fveq2d 6887	. . 3 ⊢ (𝑘 = 𝐾 → (𝐶‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝐾)))
17		oveq1 7425	. . . 4 ⊢ (𝑘 = 𝐾 → (𝑘 ↑ (𝑁‘ 1 )) = (𝐾 ↑ (𝑁‘ 1 )))
18		2fveq3 6888	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝐾)))
19	18	fveq1d 6885	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝐾))‘𝑍))
20	17, 19	oveq12d 7436	. . 3 ⊢ (𝑘 = 𝐾 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))
21	16, 20	eqeq12d 2777	. 2 ⊢ (𝑘 = 𝐾 → ((𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ↔ (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍))))
22		oveq2 7426	. . . . 5 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = (𝐵 ↑m ∅))
23		vieta.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
24	23	fvexi 6897	. . . . . 6 ⊢ 𝐵 ∈ V
25		mapdm0 8855	. . . . . 6 ⊢ (𝐵 ∈ V → (𝐵 ↑m ∅) = {∅})
26	24, 25	ax-mp 5	. . . . 5 ⊢ (𝐵 ↑m ∅) = {∅}
27	22, 26	eqtrdi 2812	. . . 4 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = {∅})
28		fveq2 6883	. . . . . . 7 ⊢ (𝑗 = ∅ → (♯‘𝑗) = (♯‘∅))
29	28	oveq2d 7434	. . . . . 6 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = (0...(♯‘∅)))
30		hash0 14504	. . . . . . . 8 ⊢ (♯‘∅) = 0
31	30	oveq2i 7429	. . . . . . 7 ⊢ (0...(♯‘∅)) = (0...0)
32		fz0sn 13754	. . . . . . 7 ⊢ (0...0) = {0}
33	31, 32	eqtri 2784	. . . . . 6 ⊢ (0...(♯‘∅)) = {0}
34	29, 33	eqtrdi 2812	. . . . 5 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = {0})
35		mpteq1 5194	. . . . . . . . . . 11 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
36		mpt0 6679	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅
37	35, 36	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅)
38	37	oveq2d 7434	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg ∅))
39		eqid 2761	. . . . . . . . . 10 ⊢ (0g‘𝑀) = (0g‘𝑀)
40	39	gsum0 18866	. . . . . . . . 9 ⊢ (𝑀 Σg ∅) = (0g‘𝑀)
41	38, 40	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (0g‘𝑀))
42	41	fveq2d 6887	. . . . . . 7 ⊢ (𝑗 = ∅ → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(0g‘𝑀)))
43	28	oveq1d 7433	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = ((♯‘∅) − 𝑘))
44	30	oveq1i 7428	. . . . . . . 8 ⊢ ((♯‘∅) − 𝑘) = (0 − 𝑘)
45	43, 44	eqtrdi 2812	. . . . . . 7 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = (0 − 𝑘))
46	42, 45	fveq12d 6890	. . . . . 6 ⊢ (𝑗 = ∅ → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(0g‘𝑀))‘(0 − 𝑘)))
47		oveq1 7425	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑗 eval 𝑅) = (∅ eval 𝑅))
48		oveq1 7425	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑗eSymPoly𝑅) = (∅eSymPoly𝑅))
49	48	fveq1d 6885	. . . . . . . . 9 ⊢ (𝑗 = ∅ → ((𝑗eSymPoly𝑅)‘𝑘) = ((∅eSymPoly𝑅)‘𝑘))
50	47, 49	fveq12d 6890	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)))
51	50	fveq1d 6885	. . . . . . 7 ⊢ (𝑗 = ∅ → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))
52	51	oveq2d 7434	. . . . . 6 ⊢ (𝑗 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
53	46, 52	eqeq12d 2777	. . . . 5 ⊢ (𝑗 = ∅ → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
54	34, 53	raleqbidv 3335	. . . 4 ⊢ (𝑗 = ∅ → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
55	27, 54	raleqbidv 3335	. . 3 ⊢ (𝑗 = ∅ → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
56		oveq2 7426	. . . 4 ⊢ (𝑗 = 𝑖 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝑖))
57		fveq2 6883	. . . . . 6 ⊢ (𝑗 = 𝑖 → (♯‘𝑗) = (♯‘𝑖))
58	57	oveq2d 7434	. . . . 5 ⊢ (𝑗 = 𝑖 → (0...(♯‘𝑗)) = (0...(♯‘𝑖)))
59		mpteq1 5194	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
60	59	oveq2d 7434	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
61	60	fveq2d 6887	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
62	57	oveq1d 7433	. . . . . . 7 ⊢ (𝑗 = 𝑖 → ((♯‘𝑗) − 𝑘) = ((♯‘𝑖) − 𝑘))
63	61, 62	fveq12d 6890	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
64		oveq1 7425	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑗 eval 𝑅) = (𝑖 eval 𝑅))
65		oveq1 7425	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗eSymPoly𝑅) = (𝑖eSymPoly𝑅))
66	65	fveq1d 6885	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → ((𝑗eSymPoly𝑅)‘𝑘) = ((𝑖eSymPoly𝑅)‘𝑘))
67	64, 66	fveq12d 6890	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)))
68	67	fveq1d 6885	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
69	68	oveq2d 7434	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
70	63, 69	eqeq12d 2777	. . . . 5 ⊢ (𝑗 = 𝑖 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
71	58, 70	raleqbidv 3335	. . . 4 ⊢ (𝑗 = 𝑖 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
72	56, 71	raleqbidv 3335	. . 3 ⊢ (𝑗 = 𝑖 → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
73		oveq2 7426	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝐵 ↑m 𝑗) = (𝐵 ↑m (𝑖 ∪ {𝑚})))
74		fveq2 6883	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (♯‘𝑗) = (♯‘(𝑖 ∪ {𝑚})))
75	74	oveq2d 7434	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (0...(♯‘𝑗)) = (0...(♯‘(𝑖 ∪ {𝑚}))))
76		mpteq1 5194	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
77	76	oveq2d 7434	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
78	77	fveq2d 6887	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
79	74	oveq1d 7433	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((♯‘𝑗) − 𝑘) = ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))
80	78, 79	fveq12d 6890	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))
81		oveq1 7425	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗 eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅))
82		oveq1 7425	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅))
83	82	fveq1d 6885	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗eSymPoly𝑅)‘𝑘) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
84	81, 83	fveq12d 6890	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
85	84	fveq1d 6885	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
86	85	oveq2d 7434	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
87	80, 86	eqeq12d 2777	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
88	75, 87	raleqbidv 3335	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
89	73, 88	raleqbidv 3335	. . 3 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
90		oveq2 7426	. . . 4 ⊢ (𝑗 = 𝐼 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝐼))
91		fveq2 6883	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = (♯‘𝐼))
92		vieta.h	. . . . . . 7 ⊢ 𝐻 = (♯‘𝐼)
93	91, 92	eqtr4di 2814	. . . . . 6 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = 𝐻)
94	93	oveq2d 7434	. . . . 5 ⊢ (𝑗 = 𝐼 → (0...(♯‘𝑗)) = (0...𝐻))
95		mpteq1 5194	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
96	95	oveq2d 7434	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
97	96	fveq2d 6887	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
98	93	oveq1d 7433	. . . . . . 7 ⊢ (𝑗 = 𝐼 → ((♯‘𝑗) − 𝑘) = (𝐻 − 𝑘))
99	97, 98	fveq12d 6890	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)))
100		oveq1 7425	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = (𝐼 eval 𝑅))
101		vieta.q	. . . . . . . . . 10 ⊢ 𝑄 = (𝐼 eval 𝑅)
102	100, 101	eqtr4di 2814	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = 𝑄)
103		oveq1 7425	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = (𝐼eSymPoly𝑅))
104		vieta.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
105	103, 104	eqtr4di 2814	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = 𝐸)
106	105	fveq1d 6885	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → ((𝑗eSymPoly𝑅)‘𝑘) = (𝐸‘𝑘))
107	102, 106	fveq12d 6890	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (𝑄‘(𝐸‘𝑘)))
108	107	fveq1d 6885	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑧))
109	108	oveq2d 7434	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
110	99, 109	eqeq12d 2777	. . . . 5 ⊢ (𝑗 = 𝐼 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
111	94, 110	raleqbidv 3335	. . . 4 ⊢ (𝑗 = 𝐼 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
112	90, 111	raleqbidv 3335	. . 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 20972	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
117	23, 114, 116	ringidcld 20488	. . . . . 6 ⊢ (𝜑 → 1 ∈ 𝐵)
118	23, 113, 114, 116, 117	ringlidmd 20494	. . . . 5 ⊢ (𝜑 → ( 1 · 1 ) = 1 )
119		vieta.n	. . . . . . . 8 ⊢ 𝑁 = (invg‘𝑅)
120	116	ringgrpd 20462	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
121	23, 119, 120, 117	grpinvcld 19192	. . . . . . 7 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
122		eqid 2761	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
123	122, 23	mgpbas 20358	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
124	122, 114	ringidval 20402	. . . . . . . 8 ⊢ 1 = (0g‘(mulGrp‘𝑅))
125		vieta.p	. . . . . . . 8 ⊢ ↑ = (.g‘(mulGrp‘𝑅))
126	123, 124, 125	mulg0 19277	. . . . . . 7 ⊢ ((𝑁‘ 1 ) ∈ 𝐵 → (0 ↑ (𝑁‘ 1 )) = 1 )
127	121, 126	syl 18	. . . . . 6 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) = 1 )
128		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
129	128, 114	zrh1 21811	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → ((ℤRHom‘𝑅)‘1) = 1 )
130	116, 129	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℤRHom‘𝑅)‘1) = 1 )
131	130	sneqd 4596	. . . . . . . . . . . 12 ⊢ (𝜑 → {((ℤRHom‘𝑅)‘1)} = { 1 })
132	131	xpeq2d 5681	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = ({∅} × { 1 }))
133		0ex 5261	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
134	133	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ V)
135	114	fvexi 6897	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
136	135	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ V)
137		xpsng 7138	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ 1 ∈ V) → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
138	134, 136, 137	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
139		0xp 5750	. . . . . . . . . . . . . . . 16 ⊢ (∅ × {0}) = ∅
140	139	eqcomi 2770	. . . . . . . . . . . . . . 15 ⊢ ∅ = (∅ × {0})
141	140	eqeq2i 2774	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ∅ ↔ 𝑓 = (∅ × {0}))
142	141	bilani 510	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 = ∅) → 𝑓 = (∅ × {0}))
143	142	iftrued 4490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 = ∅) → if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅)) = 1 )
144	143, 134, 136	fmptsnd 7172	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨∅, 1 ⟩} = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
145	132, 138, 144	3eqtrd 2800	. . . . . . . . . 10 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
146		elsni 4601	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ {∅} → ℎ = ∅)
147		nn0ex 12605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ∈ V
148		mapdm0 8855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ0 ∈ V → (ℕ0 ↑m ∅) = {∅})
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℕ0 ↑m ∅) = {∅}
150	146, 149	eleq2s 2879	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ℎ = ∅)
151	150	cnveqd 5853	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ◡ℎ = ◡∅)
152	151	imaeq1d 6051	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = (◡∅ “ ℕ))
153		cnv0 5861	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡∅ = ∅
154	153	imaeq1i 6049	. . . . . . . . . . . . . . . . . 18 ⊢ (◡∅ “ ℕ) = (∅ “ ℕ)
155		0ima 6199	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ “ ℕ) = ∅
156	154, 155	eqtri 2784	. . . . . . . . . . . . . . . . 17 ⊢ (◡∅ “ ℕ) = ∅
157	152, 156	eqtrdi 2812	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = ∅)
158		0fi 9063	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Fin
159	157, 158	eqeltrdi 2869	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) ∈ Fin)
160	159	rabeqc 3425	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin} = (ℕ0 ↑m ∅)
161	160, 149	eqtr2i 2785	. . . . . . . . . . . . 13 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
162		eqid 2761	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
163	162	psrbasfsupp 34136	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
164	161, 163	eqtr4i 2787	. . . . . . . . . . . 12 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
165		0nn0 12614	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
166	165	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ0)
167	164, 134, 115, 166	esplyfval 34188	. . . . . . . . . . 11 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))))
168		fveqeq2 6892	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ∅ → ((♯‘𝑐) = 0 ↔ (♯‘∅) = 0))
169		0elpw 5317	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 ∅
170	169	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ ∈ 𝒫 ∅)
171	30	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘∅) = 0)
172		hasheq0 14500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ 𝒫 ∅ → ((♯‘𝑐) = 0 ↔ 𝑐 = ∅))
173	172	biimpa 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ 𝒫 ∅ ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
174	173	adantll 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝒫 ∅) ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
175	168, 170, 171, 174	rabeqsnd 4630	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0} = {∅})
176	175	imaeq2d 6052	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = ((𝟭‘∅) “ {∅}))
177		pw0 4773	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∅ = {∅}
178	177	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝒫 ∅ = {∅})
179		indf1o 33424	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ V → (𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅))
180		f1of 6822	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅) → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
181	134, 179, 180	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
182	178, 181	feq2dd 6693	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝟭‘∅):{∅}⟶({0, 1} ↑m ∅))
183	182	ffnd 6708	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝟭‘∅) Fn {∅})
184	133	snid 4623	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ {∅}
185	184	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∅ ∈ {∅})
186	183, 185	fnimasnd 7371	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {∅}) = {((𝟭‘∅)‘∅)})
187		ssidd 3954	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∅ ⊆ ∅)
188		indf 12319	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ V ∧ ∅ ⊆ ∅) → ((𝟭‘∅)‘∅):∅⟶{0, 1})
189	134, 187, 188	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝟭‘∅)‘∅):∅⟶{0, 1})
190		f0bi 6763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝟭‘∅)‘∅):∅⟶{0, 1} ↔ ((𝟭‘∅)‘∅) = ∅)
191	189, 190	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝟭‘∅)‘∅) = ∅)
192	191	sneqd 4596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {((𝟭‘∅)‘∅)} = {∅})
193	176, 186, 192	3eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = {∅})
194	193	fveq2d 6887	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ((𝟭‘{∅})‘{∅}))
195		p0ex 5346	. . . . . . . . . . . . . 14 ⊢ {∅} ∈ V
196		indconst1 12326	. . . . . . . . . . . . . 14 ⊢ ({∅} ∈ V → ((𝟭‘{∅})‘{∅}) = ({∅} × {1}))
197	195, 196	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝟭‘{∅})‘{∅}) = ({∅} × {1})
198	194, 197	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ({∅} × {1}))
199	198	coeq2d 5840	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))) = ((ℤRHom‘𝑅) ∘ ({∅} × {1})))
200	128	zrhrhm 21810	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
201		zringbas 21752	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤring)
202	201, 23	rhmf 20708	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
203	116, 200, 202	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝑅):ℤ⟶𝐵)
204	203	ffnd 6708	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤRHom‘𝑅) Fn ℤ)
205		1zzd 12720	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
206		fcoconst 7133	. . . . . . . . . . . 12 ⊢ (((ℤRHom‘𝑅) Fn ℤ ∧ 1 ∈ ℤ) → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
207	204, 205, 206	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
208	167, 199, 207	3eqtrd 2800	. . . . . . . . . 10 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
209		eqid 2761	. . . . . . . . . . 11 ⊢ (∅ mPoly 𝑅) = (∅ mPoly 𝑅)
210		eqid 2761	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
211		eqid 2761	. . . . . . . . . . 11 ⊢ (algSc‘(∅ mPoly 𝑅)) = (algSc‘(∅ mPoly 𝑅))
212	209, 161, 210, 23, 211, 134, 116, 117	mplascl 22366	. . . . . . . . . 10 ⊢ (𝜑 → ((algSc‘(∅ mPoly 𝑅))‘ 1 ) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
213	145, 208, 212	3eqtr4d 2806	. . . . . . . . 9 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((algSc‘(∅ mPoly 𝑅))‘ 1 ))
214	213	fveq2d 6887	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)) = ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )))
215	214	fveq1d 6885	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅))
216		eqid 2761	. . . . . . . . 9 ⊢ (∅ eval 𝑅) = (∅ eval 𝑅)
217	184, 149	eleqtrri 2860	. . . . . . . . . 10 ⊢ ∅ ∈ (ℕ0 ↑m ∅)
218	217	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ (ℕ0 ↑m ∅))
219	115	idomcringd 20971	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
220	216, 209, 23, 211, 218, 219, 117	evlsca 22408	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )) = ((𝐵 ↑m ∅) × { 1 }))
221	220	fveq1d 6885	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅) = (((𝐵 ↑m ∅) × { 1 })‘∅))
222	184, 26	eleqtrri 2860	. . . . . . . 8 ⊢ ∅ ∈ (𝐵 ↑m ∅)
223	135	fvconst2 7208	. . . . . . . 8 ⊢ (∅ ∈ (𝐵 ↑m ∅) → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
224	222, 223	mp1i 14	. . . . . . 7 ⊢ (𝜑 → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
225	215, 221, 224	3eqtrd 2800	. . . . . 6 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = 1 )
226	127, 225	oveq12d 7436	. . . . 5 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)) = ( 1 · 1 ))
227		iftrue 4488	. . . . . 6 ⊢ (𝑙 = 0 → if(𝑙 = 0, 1 , (0g‘𝑅)) = 1 )
228		vieta.w	. . . . . . . 8 ⊢ 𝑊 = (Poly1‘𝑅)
229		vieta.m	. . . . . . . . . 10 ⊢ 𝑀 = (mulGrp‘𝑊)
230		eqid 2761	. . . . . . . . . 10 ⊢ (1r‘𝑊) = (1r‘𝑊)
231	229, 230	ringidval 20402	. . . . . . . . 9 ⊢ (1r‘𝑊) = (0g‘𝑀)
232	231	eqcomi 2770	. . . . . . . 8 ⊢ (0g‘𝑀) = (1r‘𝑊)
233	228, 232, 210, 114	coe1id 22605	. . . . . . 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 7016	. . . . 5 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = 1 )
236	118, 226, 235	3eqtr4rd 2807	. . . 4 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
237		fveq2 6883	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))
238	237	oveq2d 7434	. . . . . . . 8 ⊢ (𝑧 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)))
239	238	eqeq2d 2772	. . . . . . 7 ⊢ (𝑧 = ∅ → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
240	239	ralbidv 3186	. . . . . 6 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
241		c0ex 11293	. . . . . . 7 ⊢ 0 ∈ V
242		oveq2 7426	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (0 − 𝑘) = (0 − 0))
243		0m0e0 12454	. . . . . . . . . 10 ⊢ (0 − 0) = 0
244	242, 243	eqtrdi 2812	. . . . . . . . 9 ⊢ (𝑘 = 0 → (0 − 𝑘) = 0)
245	244	fveq2d 6887	. . . . . . . 8 ⊢ (𝑘 = 0 → ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((coe1‘(0g‘𝑀))‘0))
246		oveq1 7425	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
247		2fveq3 6888	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)))
248	247	fveq1d 6885	. . . . . . . . 9 ⊢ (𝑘 = 0 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))
249	246, 248	oveq12d 7436	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
250	245, 249	eqeq12d 2777	. . . . . . 7 ⊢ (𝑘 = 0 → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))))
251	241, 250	ralsn 4642	. . . . . 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 4642	. . . 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 3287	. . . . . . 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 3299	. . . . . . . . 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 2761	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅)
265		eqid 2761	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚})eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅)
266		vieta.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑅)
267		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
268		eqid 2761	. . . . . . . . 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 9253	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ∈ Fin)
273		snfi 9064	. . . . . . . . . . 11 ⊢ {𝑚} ∈ Fin
274	273	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → {𝑚} ∈ Fin)
275	272, 274	unfid 9180	. . . . . . . . 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		simplr 781	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
278	277	elmaprd 8863	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧:(𝑖 ∪ {𝑚})⟶𝐵)
279		2fveq3 6888	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑧‘𝑜)))
280	279	oveq2d 7434	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑧‘𝑜))))
281	280	cbvmptv 5209	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜))))
282	281	oveq2i 7429	. . . . . . . . 9 ⊢ (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜)))))
283		fznn0sub2 13762	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
284	283	adantl 487	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
285		ssun2 4125	. . . . . . . . . . 11 ⊢ {𝑚} ⊆ (𝑖 ∪ {𝑚})
286		vsnid 4624	. . . . . . . . . . 11 ⊢ 𝑚 ∈ {𝑚}
287	285, 286	sselii 3928	. . . . . . . . . 10 ⊢ 𝑚 ∈ (𝑖 ∪ {𝑚})
288	287	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑚 ∈ (𝑖 ∪ {𝑚}))
289		eqid 2761	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = ((𝑖 ∪ {𝑚}) ∖ {𝑚})
290		fveq1 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑦 → (𝑧‘𝑛) = (𝑦‘𝑛))
291	290	fveq2d 6887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑦 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑦‘𝑛)))
292	291	oveq2d 7434	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑛))))
293	292	mpteq2dv 5199	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))
294	293	oveq2d 7434	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))
295	294	fveq2d 6887	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))))
296	295	fveq1d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
297		fveq2 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))
298	297	oveq2d 7434	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
299	296, 298	eqeq12d 2777	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
300	299	ralbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
301	300	cbvralvw 3241	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
302		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑚 ∈ (𝐼 ∖ 𝑖))
303	302	eldifbd 3912	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ¬ 𝑚 ∈ 𝑖)
304		disjsn 4672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∩ {𝑚}) = ∅ ↔ ¬ 𝑚 ∈ 𝑖)
305	303, 304	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∩ {𝑚}) = ∅)
306		undif5 4440	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∩ {𝑚}) = ∅ → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
307	305, 306	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
308	307	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 = ((𝑖 ∪ {𝑚}) ∖ {𝑚}))
309	308	oveq2d 7434	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝐵 ↑m 𝑖) = (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚})))
310		oveq2 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((♯‘𝑖) − 𝑘) = ((♯‘𝑖) − 𝑙))
311	310	fveq2d 6887	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)))
312		oveq1 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
313		2fveq3 6888	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)))
314	313	fveq1d 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))
315	312, 314	oveq12d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
316	311, 315	eqeq12d 2777	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))))
317	316	cbvralvw 3241	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
318	308	fveq2d 6887	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (♯‘𝑖) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
319	318	oveq2d 7434	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (0...(♯‘𝑖)) = (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))))
320		2fveq3 6888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑦‘𝑛)) = (𝐴‘(𝑦‘𝑜)))
321	320	oveq2d 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑦‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑜))))
322	321	cbvmptv 5209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))
323	308	mpteq1d 5195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
324	322, 323	eqtrid 2808	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
325	324	oveq2d 7434	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))
326	325	fveq2d 6887	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))))
327	318	oveq1d 7433	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((♯‘𝑖) − 𝑙) = ((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙))
328	326, 327	fveq12d 6890	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)))
329	308	oveq1d 7433	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅))
330	308	oveq1d 7433	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅))
331	330	fveq1d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖eSymPoly𝑅)‘𝑙) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))
332	329, 331	fveq12d 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙)))
333	332	fveq1d 6885	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦) = (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))
334	333	oveq2d 7434	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
335	328, 334	eqeq12d 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
336	319, 335	raleqbidv 3335	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
337	317, 336	bitrid 286	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
338	309, 337	raleqbidv 3335	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
339	301, 338	bitrid 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
340	339	biimpa 482	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
341	340	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
342		eqid 2761	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)
343		eqid 2761	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)
344		eqid 2761	. . . . . . . . . 10 ⊢ (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))
345		difssd 4084	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ⊆ (𝑖 ∪ {𝑚}))
346	275, 345	ssfid 9253	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ∈ Fin)
347	278, 345	fssresd 6747	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚})):((𝑖 ∪ {𝑚}) ∖ {𝑚})⟶𝐵)
348		eqid 2761	. . . . . . . . . 10 ⊢ (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))
349		eqid 2761	. . . . . . . . . 10 ⊢ (deg1‘𝑅) = (deg1‘𝑅)
350	228, 23, 263, 229, 342, 343, 119, 114, 113, 266, 267, 125, 344, 346, 276, 347, 348, 349	vietadeg1 34203	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((deg1‘𝑅)‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
351	228, 23, 263, 229, 264, 265, 119, 114, 113, 266, 267, 125, 268, 275, 276, 278, 282, 284, 288, 289, 341, 350	vietalem 34204	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)))
352	269	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝐼 ∈ Fin)
353		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ⊆ 𝐼)
354	352, 353	ssfid 9253	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ∈ Fin)
355	273	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → {𝑚} ∈ Fin)
356	354, 355	unfid 9180	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∪ {𝑚}) ∈ Fin)
357	356	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
358		hashcl 14493	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∪ {𝑚}) ∈ Fin → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
359	357, 358	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
360	359	nn0cnd 12662	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℂ)
361		elfznn0 13747	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → 𝑘 ∈ ℕ0)
362	361	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℕ0)
363	362	nn0cnd 12662	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℂ)
364	360, 363	nncand 11667	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = 𝑘)
365	364	oveq1d 7433	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
366	364	fveq2d 6887	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
367	366	fveq2d 6887	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
368	367	fveq1d 6885	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
369	365, 368	oveq12d 7436	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
370	369	ad4ant14 765	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
371	351, 370	eqtrd 2796	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
372	262, 371	ralrimia 3262	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) → ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
373	257, 372	ralrimia 3262	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
374	373	ex 418	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
375	374	anasss 472	. . 3 ⊢ ((𝜑 ∧ (𝑖 ⊆ 𝐼 ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
376	55, 72, 89, 112, 254, 375, 269	findcard2d 9175	. 2 ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑m 𝐼)∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
377	24	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
378		vieta.z	. . 3 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
379	377, 269, 378	elmapdd 8854	. 2 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m 𝐼))
380		vieta.k	. 2 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
381	14, 21, 376, 379, 380	rspc2dv 3591	1 ⊢ (𝜑 → (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  {crab 3413  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  ifcif 4482  𝒫 cpw 4557  {csn 4584  {cpr 4586  ⟨cop 4590   class class class wbr 5103   ↦ cmpt 5186   × cxp 5649  ^◡ccnv 5650   ↾ cres 5653   “ cima 5654   ∘ ccom 5655   Fn wfn 6532  ⟶wf 6533  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7418   ↑_m cmap 8840  Fincfn 8966   finSupp cfsupp 9346  0cc0 11193  1c1 11194   − cmin 11534  𝟭cind 12313  ℕcn 12328  ℕ₀cn0 12599  ℤcz 12686  ...cfz 13632  ♯chash 14467  Basecbs 17380  ._rcmulr 17422  0_gc0g 17603   Σ_g cgsu 17604  inv_gcminusg 19138  -_gcsg 19139  ._gcmg 19270  mulGrpcmgp 20353  1_rcur 20400  Ringcrg 20452   RingHom crh 20692  IDomncidom 20938  ℤ_ringczring 21745  ℤRHomczrh 21798  algSccascl 22153   mPoly cmpl 22207   eval cevl 22375  var₁cv1 22487  Poly₁cpl1 22488  coe₁cco1 22489  deg₁cdg1 26365  eSymPolycesply 34181

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-inf2 9635  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270  ax-pre-sup 11271  ax-addf 11272  ax-mulf 11273

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-ofr 7692  df-om 7876  df-1st 7999  df-2nd 8000  df-supp 8171  df-tpos 8236  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-2o 8470  df-oadd 8473  df-er 8710  df-map 8842  df-pm 8843  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9347  df-sup 9427  df-oi 9497  df-dju 9975  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-div 11967  df-ind 12314  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404  df-9 12405  df-n0 12600  df-xnn0 12673  df-z 12687  df-dec 12808  df-uz 12959  df-rp 13114  df-fz 13633  df-fzo 13782  df-seq 14138  df-exp 14198  df-fac 14411  df-bc 14440  df-hash 14468  df-cj 15259  df-re 15260  df-im 15261  df-sqrt 15395  df-abs 15396  df-clim 15648  df-sum 15847  df-struct 17318  df-sets 17335  df-slot 17353  df-ndx 17365  df-base 17381  df-ress 17402  df-plusg 17434  df-mulr 17435  df-starv 17436  df-sca 17437  df-vsca 17438  df-ip 17439  df-tset 17440  df-ple 17441  df-ds 17443  df-unif 17444  df-hom 17445  df-cco 17446  df-0g 17605  df-gsum 17606  df-prds 17611  df-pws 17613  df-mre 17749  df-mrc 17750  df-acs 17752  df-mgm 18809  df-sgrp 18901  df-mnd 18917  df-mhm 18971  df-submnd 18972  df-grp 19140  df-minusg 19141  df-sbg 19142  df-mulg 19271  df-subg 19326  df-ghm 19421  df-cntz 19524  df-cmn 19989  df-abl 19990  df-mgp 20354  df-rng 20368  df-ur 20401  df-srg 20406  df-ring 20454  df-cring 20455  df-oppr 20560  df-dvdsr 20580  df-unit 20581  df-invr 20611  df-rhm 20695  df-nzr 20756  df-subrng 20791  df-subrg 20815  df-rlreg 20939  df-domn 20940  df-idom 20941  df-lmod 21130  df-lss 21200  df-lsp 21240  df-cnfld 21672  df-zring 21746  df-zrh 21802  df-assa 22154  df-asp 22155  df-ascl 22156  df-psr 22210  df-mvr 22211  df-mpl 22212  df-opsr 22214  df-evls 22376  df-evl 22377  df-psr1 22491  df-vr1 22492  df-ply1 22493  df-coe1 22494  df-mdeg 26366  df-deg1 26367  df-extv 34155  df-esply 34183

This theorem is used by: (None)