Theorem vieta 33739

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 26289 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 6833	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → (𝑧‘𝑛) = (𝑍‘𝑛))
2	1	fveq2d 6838	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑍‘𝑛)))
3	2	oveq2d 7376	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
4	3	mpteq2dv 5180	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
5	4	oveq2d 7376	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
6		vieta.f	. . . . . . 7 ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
7	5, 6	eqtr4di 2790	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = 𝐹)
8	7	fveq2d 6838	. . . . 5 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘𝐹))
9		vieta.c	. . . . 5 ⊢ 𝐶 = (coe1‘𝐹)
10	8, 9	eqtr4di 2790	. . . 4 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = 𝐶)
11	10	fveq1d 6836	. . 3 ⊢ (𝑧 = 𝑍 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝑘)))
12		fveq2 6834	. . . 4 ⊢ (𝑧 = 𝑍 → ((𝑄‘(𝐸‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑍))
13	12	oveq2d 7376	. . 3 ⊢ (𝑧 = 𝑍 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)))
14	11, 13	eqeq12d 2753	. 2 ⊢ (𝑧 = 𝑍 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) ↔ (𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))))
15		oveq2 7368	. . . 4 ⊢ (𝑘 = 𝐾 → (𝐻 − 𝑘) = (𝐻 − 𝐾))
16	15	fveq2d 6838	. . 3 ⊢ (𝑘 = 𝐾 → (𝐶‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝐾)))
17		oveq1 7367	. . . 4 ⊢ (𝑘 = 𝐾 → (𝑘 ↑ (𝑁‘ 1 )) = (𝐾 ↑ (𝑁‘ 1 )))
18		2fveq3 6839	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝐾)))
19	18	fveq1d 6836	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝐾))‘𝑍))
20	17, 19	oveq12d 7378	. . 3 ⊢ (𝑘 = 𝐾 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))
21	16, 20	eqeq12d 2753	. 2 ⊢ (𝑘 = 𝐾 → ((𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ↔ (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍))))
22		oveq2 7368	. . . . 5 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = (𝐵 ↑m ∅))
23		vieta.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
24	23	fvexi 6848	. . . . . 6 ⊢ 𝐵 ∈ V
25		mapdm0 8782	. . . . . 6 ⊢ (𝐵 ∈ V → (𝐵 ↑m ∅) = {∅})
26	24, 25	ax-mp 5	. . . . 5 ⊢ (𝐵 ↑m ∅) = {∅}
27	22, 26	eqtrdi 2788	. . . 4 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = {∅})
28		fveq2 6834	. . . . . . 7 ⊢ (𝑗 = ∅ → (♯‘𝑗) = (♯‘∅))
29	28	oveq2d 7376	. . . . . 6 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = (0...(♯‘∅)))
30		hash0 14320	. . . . . . . 8 ⊢ (♯‘∅) = 0
31	30	oveq2i 7371	. . . . . . 7 ⊢ (0...(♯‘∅)) = (0...0)
32		fz0sn 13572	. . . . . . 7 ⊢ (0...0) = {0}
33	31, 32	eqtri 2760	. . . . . 6 ⊢ (0...(♯‘∅)) = {0}
34	29, 33	eqtrdi 2788	. . . . 5 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = {0})
35		mpteq1 5175	. . . . . . . . . . 11 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
36		mpt0 6634	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅
37	35, 36	eqtrdi 2788	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅)
38	37	oveq2d 7376	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg ∅))
39		eqid 2737	. . . . . . . . . 10 ⊢ (0g‘𝑀) = (0g‘𝑀)
40	39	gsum0 18643	. . . . . . . . 9 ⊢ (𝑀 Σg ∅) = (0g‘𝑀)
41	38, 40	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (0g‘𝑀))
42	41	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = ∅ → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(0g‘𝑀)))
43	28	oveq1d 7375	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = ((♯‘∅) − 𝑘))
44	30	oveq1i 7370	. . . . . . . 8 ⊢ ((♯‘∅) − 𝑘) = (0 − 𝑘)
45	43, 44	eqtrdi 2788	. . . . . . 7 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = (0 − 𝑘))
46	42, 45	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = ∅ → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(0g‘𝑀))‘(0 − 𝑘)))
47		oveq1 7367	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑗 eval 𝑅) = (∅ eval 𝑅))
48		oveq1 7367	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑗eSymPoly𝑅) = (∅eSymPoly𝑅))
49	48	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑗 = ∅ → ((𝑗eSymPoly𝑅)‘𝑘) = ((∅eSymPoly𝑅)‘𝑘))
50	47, 49	fveq12d 6841	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)))
51	50	fveq1d 6836	. . . . . . 7 ⊢ (𝑗 = ∅ → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))
52	51	oveq2d 7376	. . . . . 6 ⊢ (𝑗 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
53	46, 52	eqeq12d 2753	. . . . 5 ⊢ (𝑗 = ∅ → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
54	34, 53	raleqbidv 3312	. . . 4 ⊢ (𝑗 = ∅ → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
55	27, 54	raleqbidv 3312	. . 3 ⊢ (𝑗 = ∅ → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
56		oveq2 7368	. . . 4 ⊢ (𝑗 = 𝑖 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝑖))
57		fveq2 6834	. . . . . 6 ⊢ (𝑗 = 𝑖 → (♯‘𝑗) = (♯‘𝑖))
58	57	oveq2d 7376	. . . . 5 ⊢ (𝑗 = 𝑖 → (0...(♯‘𝑗)) = (0...(♯‘𝑖)))
59		mpteq1 5175	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
60	59	oveq2d 7376	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
61	60	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
62	57	oveq1d 7375	. . . . . . 7 ⊢ (𝑗 = 𝑖 → ((♯‘𝑗) − 𝑘) = ((♯‘𝑖) − 𝑘))
63	61, 62	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
64		oveq1 7367	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑗 eval 𝑅) = (𝑖 eval 𝑅))
65		oveq1 7367	. . . . . . . . . 10 ⊢ (𝑗 = 𝑖 → (𝑗eSymPoly𝑅) = (𝑖eSymPoly𝑅))
66	65	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → ((𝑗eSymPoly𝑅)‘𝑘) = ((𝑖eSymPoly𝑅)‘𝑘))
67	64, 66	fveq12d 6841	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)))
68	67	fveq1d 6836	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
69	68	oveq2d 7376	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
70	63, 69	eqeq12d 2753	. . . . 5 ⊢ (𝑗 = 𝑖 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
71	58, 70	raleqbidv 3312	. . . 4 ⊢ (𝑗 = 𝑖 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
72	56, 71	raleqbidv 3312	. . 3 ⊢ (𝑗 = 𝑖 → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
73		oveq2 7368	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝐵 ↑m 𝑗) = (𝐵 ↑m (𝑖 ∪ {𝑚})))
74		fveq2 6834	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (♯‘𝑗) = (♯‘(𝑖 ∪ {𝑚})))
75	74	oveq2d 7376	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (0...(♯‘𝑗)) = (0...(♯‘(𝑖 ∪ {𝑚}))))
76		mpteq1 5175	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
77	76	oveq2d 7376	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
78	77	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
79	74	oveq1d 7375	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((♯‘𝑗) − 𝑘) = ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))
80	78, 79	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))
81		oveq1 7367	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗 eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅))
82		oveq1 7367	. . . . . . . . . 10 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅))
83	82	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗eSymPoly𝑅)‘𝑘) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
84	81, 83	fveq12d 6841	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
85	84	fveq1d 6836	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
86	85	oveq2d 7376	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
87	80, 86	eqeq12d 2753	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
88	75, 87	raleqbidv 3312	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
89	73, 88	raleqbidv 3312	. . 3 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
90		oveq2 7368	. . . 4 ⊢ (𝑗 = 𝐼 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝐼))
91		fveq2 6834	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = (♯‘𝐼))
92		vieta.h	. . . . . . 7 ⊢ 𝐻 = (♯‘𝐼)
93	91, 92	eqtr4di 2790	. . . . . 6 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = 𝐻)
94	93	oveq2d 7376	. . . . 5 ⊢ (𝑗 = 𝐼 → (0...(♯‘𝑗)) = (0...𝐻))
95		mpteq1 5175	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
96	95	oveq2d 7376	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
97	96	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
98	93	oveq1d 7375	. . . . . . 7 ⊢ (𝑗 = 𝐼 → ((♯‘𝑗) − 𝑘) = (𝐻 − 𝑘))
99	97, 98	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)))
100		oveq1 7367	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = (𝐼 eval 𝑅))
101		vieta.q	. . . . . . . . . 10 ⊢ 𝑄 = (𝐼 eval 𝑅)
102	100, 101	eqtr4di 2790	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = 𝑄)
103		oveq1 7367	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = (𝐼eSymPoly𝑅))
104		vieta.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
105	103, 104	eqtr4di 2790	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = 𝐸)
106	105	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → ((𝑗eSymPoly𝑅)‘𝑘) = (𝐸‘𝑘))
107	102, 106	fveq12d 6841	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → ((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘)) = (𝑄‘(𝐸‘𝑘)))
108	107	fveq1d 6836	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑧))
109	108	oveq2d 7376	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
110	99, 109	eqeq12d 2753	. . . . 5 ⊢ (𝑗 = 𝐼 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
111	94, 110	raleqbidv 3312	. . . 4 ⊢ (𝑗 = 𝐼 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
112	90, 111	raleqbidv 3312	. . 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 20696	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
117	23, 114, 116	ringidcld 20238	. . . . . 6 ⊢ (𝜑 → 1 ∈ 𝐵)
118	23, 113, 114, 116, 117	ringlidmd 20244	. . . . 5 ⊢ (𝜑 → ( 1 · 1 ) = 1 )
119		vieta.n	. . . . . . . 8 ⊢ 𝑁 = (invg‘𝑅)
120	116	ringgrpd 20214	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
121	23, 119, 120, 117	grpinvcld 18955	. . . . . . 7 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
122		eqid 2737	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
123	122, 23	mgpbas 20117	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
124	122, 114	ringidval 20155	. . . . . . . 8 ⊢ 1 = (0g‘(mulGrp‘𝑅))
125		vieta.p	. . . . . . . 8 ⊢ ↑ = (.g‘(mulGrp‘𝑅))
126	123, 124, 125	mulg0 19041	. . . . . . 7 ⊢ ((𝑁‘ 1 ) ∈ 𝐵 → (0 ↑ (𝑁‘ 1 )) = 1 )
127	121, 126	syl 17	. . . . . 6 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) = 1 )
128		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
129	128, 114	zrh1 21502	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → ((ℤRHom‘𝑅)‘1) = 1 )
130	116, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℤRHom‘𝑅)‘1) = 1 )
131	130	sneqd 4580	. . . . . . . . . . . 12 ⊢ (𝜑 → {((ℤRHom‘𝑅)‘1)} = { 1 })
132	131	xpeq2d 5654	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = ({∅} × { 1 }))
133		0ex 5242	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
134	133	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ V)
135	114	fvexi 6848	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
136	135	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ V)
137		xpsng 7086	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ 1 ∈ V) → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
138	134, 136, 137	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
139		0xp 5723	. . . . . . . . . . . . . . . . 17 ⊢ (∅ × {0}) = ∅
140	139	eqcomi 2746	. . . . . . . . . . . . . . . 16 ⊢ ∅ = (∅ × {0})
141	140	eqeq2i 2750	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = ∅ ↔ 𝑓 = (∅ × {0}))
142	141	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ∅ → 𝑓 = (∅ × {0}))
143	142	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 = ∅) → 𝑓 = (∅ × {0}))
144	143	iftrued 4475	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 = ∅) → if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅)) = 1 )
145	144, 134, 136	fmptsnd 7117	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨∅, 1 ⟩} = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
146	132, 138, 145	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
147		elsni 4585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ {∅} → ℎ = ∅)
148		nn0ex 12434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ∈ V
149		mapdm0 8782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ0 ∈ V → (ℕ0 ↑m ∅) = {∅})
150	148, 149	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℕ0 ↑m ∅) = {∅}
151	147, 150	eleq2s 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ℎ = ∅)
152	151	cnveqd 5824	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ◡ℎ = ◡∅)
153	152	imaeq1d 6018	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = (◡∅ “ ℕ))
154		cnv0 6097	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡∅ = ∅
155	154	imaeq1i 6016	. . . . . . . . . . . . . . . . . 18 ⊢ (◡∅ “ ℕ) = (∅ “ ℕ)
156		0ima 6037	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ “ ℕ) = ∅
157	155, 156	eqtri 2760	. . . . . . . . . . . . . . . . 17 ⊢ (◡∅ “ ℕ) = ∅
158	153, 157	eqtrdi 2788	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = ∅)
159		0fi 8982	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Fin
160	158, 159	eqeltrdi 2845	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) ∈ Fin)
161	160	rabeqc 3402	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin} = (ℕ0 ↑m ∅)
162	161, 150	eqtr2i 2761	. . . . . . . . . . . . 13 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
163		eqid 2737	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
164	163	psrbasfsupp 33687	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
165	162, 164	eqtr4i 2763	. . . . . . . . . . . 12 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
166		0nn0 12443	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
167	166	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ0)
168	165, 134, 115, 167	esplyfval 33722	. . . . . . . . . . 11 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))))
169		fveqeq2 6843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ∅ → ((♯‘𝑐) = 0 ↔ (♯‘∅) = 0))
170		0elpw 5293	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 ∅
171	170	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ ∈ 𝒫 ∅)
172	30	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘∅) = 0)
173		hasheq0 14316	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ 𝒫 ∅ → ((♯‘𝑐) = 0 ↔ 𝑐 = ∅))
174	173	biimpa 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ 𝒫 ∅ ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
175	174	adantll 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝒫 ∅) ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
176	169, 171, 172, 175	rabeqsnd 4614	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0} = {∅})
177	176	imaeq2d 6019	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = ((𝟭‘∅) “ {∅}))
178		pw0 4756	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∅ = {∅}
179	178	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝒫 ∅ = {∅})
180		indf1o 32939	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ V → (𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅))
181		f1of 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅) → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
182	134, 180, 181	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
183	179, 182	feq2dd 6648	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝟭‘∅):{∅}⟶({0, 1} ↑m ∅))
184	183	ffnd 6663	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝟭‘∅) Fn {∅})
185	133	snid 4607	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ {∅}
186	185	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∅ ∈ {∅})
187	184, 186	fnimasnd 7313	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {∅}) = {((𝟭‘∅)‘∅)})
188		ssidd 3946	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∅ ⊆ ∅)
189		indf 12156	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ V ∧ ∅ ⊆ ∅) → ((𝟭‘∅)‘∅):∅⟶{0, 1})
190	134, 188, 189	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝟭‘∅)‘∅):∅⟶{0, 1})
191		f0bi 6717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝟭‘∅)‘∅):∅⟶{0, 1} ↔ ((𝟭‘∅)‘∅) = ∅)
192	190, 191	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝟭‘∅)‘∅) = ∅)
193	192	sneqd 4580	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {((𝟭‘∅)‘∅)} = {∅})
194	177, 187, 193	3eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = {∅})
195	194	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ((𝟭‘{∅})‘{∅}))
196		p0ex 5321	. . . . . . . . . . . . . 14 ⊢ {∅} ∈ V
197		indconst1 12163	. . . . . . . . . . . . . 14 ⊢ ({∅} ∈ V → ((𝟭‘{∅})‘{∅}) = ({∅} × {1}))
198	196, 197	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝟭‘{∅})‘{∅}) = ({∅} × {1})
199	195, 198	eqtrdi 2788	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ({∅} × {1}))
200	199	coeq2d 5811	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))) = ((ℤRHom‘𝑅) ∘ ({∅} × {1})))
201	128	zrhrhm 21501	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
202		zringbas 21443	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤring)
203	202, 23	rhmf 20455	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
204	116, 201, 203	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝑅):ℤ⟶𝐵)
205	204	ffnd 6663	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤRHom‘𝑅) Fn ℤ)
206		1zzd 12549	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
207		fcoconst 7081	. . . . . . . . . . . 12 ⊢ (((ℤRHom‘𝑅) Fn ℤ ∧ 1 ∈ ℤ) → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
208	205, 206, 207	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
209	168, 200, 208	3eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
210		eqid 2737	. . . . . . . . . . 11 ⊢ (∅ mPoly 𝑅) = (∅ mPoly 𝑅)
211		eqid 2737	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
212		eqid 2737	. . . . . . . . . . 11 ⊢ (algSc‘(∅ mPoly 𝑅)) = (algSc‘(∅ mPoly 𝑅))
213	210, 162, 211, 23, 212, 134, 116, 117	mplascl 22052	. . . . . . . . . 10 ⊢ (𝜑 → ((algSc‘(∅ mPoly 𝑅))‘ 1 ) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
214	146, 209, 213	3eqtr4d 2782	. . . . . . . . 9 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((algSc‘(∅ mPoly 𝑅))‘ 1 ))
215	214	fveq2d 6838	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)) = ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )))
216	215	fveq1d 6836	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅))
217		eqid 2737	. . . . . . . . 9 ⊢ (∅ eval 𝑅) = (∅ eval 𝑅)
218	185, 150	eleqtrri 2836	. . . . . . . . . 10 ⊢ ∅ ∈ (ℕ0 ↑m ∅)
219	218	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ (ℕ0 ↑m ∅))
220	115	idomcringd 20695	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
221	217, 210, 23, 212, 219, 220, 117	evlsca 22094	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )) = ((𝐵 ↑m ∅) × { 1 }))
222	221	fveq1d 6836	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅) = (((𝐵 ↑m ∅) × { 1 })‘∅))
223	185, 26	eleqtrri 2836	. . . . . . . 8 ⊢ ∅ ∈ (𝐵 ↑m ∅)
224	135	fvconst2 7152	. . . . . . . 8 ⊢ (∅ ∈ (𝐵 ↑m ∅) → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
225	223, 224	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
226	216, 222, 225	3eqtrd 2776	. . . . . 6 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = 1 )
227	127, 226	oveq12d 7378	. . . . 5 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)) = ( 1 · 1 ))
228		iftrue 4473	. . . . . 6 ⊢ (𝑙 = 0 → if(𝑙 = 0, 1 , (0g‘𝑅)) = 1 )
229		vieta.w	. . . . . . . 8 ⊢ 𝑊 = (Poly1‘𝑅)
230		vieta.m	. . . . . . . . . 10 ⊢ 𝑀 = (mulGrp‘𝑊)
231		eqid 2737	. . . . . . . . . 10 ⊢ (1r‘𝑊) = (1r‘𝑊)
232	230, 231	ringidval 20155	. . . . . . . . 9 ⊢ (1r‘𝑊) = (0g‘𝑀)
233	232	eqcomi 2746	. . . . . . . 8 ⊢ (0g‘𝑀) = (1r‘𝑊)
234	229, 233, 211, 114	coe1id 22268	. . . . . . 7 ⊢ (𝑅 ∈ Ring → (coe1‘(0g‘𝑀)) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, 1 , (0g‘𝑅))))
235	116, 234	syl 17	. . . . . 6 ⊢ (𝜑 → (coe1‘(0g‘𝑀)) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, 1 , (0g‘𝑅))))
236	228, 235, 167, 136	fvmptd4 6966	. . . . 5 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = 1 )
237	118, 227, 236	3eqtr4rd 2783	. . . 4 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
238		fveq2 6834	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))
239	238	oveq2d 7376	. . . . . . . 8 ⊢ (𝑧 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)))
240	239	eqeq2d 2748	. . . . . . 7 ⊢ (𝑧 = ∅ → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
241	240	ralbidv 3161	. . . . . 6 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
242		c0ex 11129	. . . . . . 7 ⊢ 0 ∈ V
243		oveq2 7368	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (0 − 𝑘) = (0 − 0))
244		0m0e0 12287	. . . . . . . . . 10 ⊢ (0 − 0) = 0
245	243, 244	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑘 = 0 → (0 − 𝑘) = 0)
246	245	fveq2d 6838	. . . . . . . 8 ⊢ (𝑘 = 0 → ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((coe1‘(0g‘𝑀))‘0))
247		oveq1 7367	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
248		2fveq3 6839	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)))
249	248	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑘 = 0 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))
250	247, 249	oveq12d 7378	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
251	246, 250	eqeq12d 2753	. . . . . . 7 ⊢ (𝑘 = 0 → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))))
252	242, 251	ralsn 4626	. . . . . 6 ⊢ (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
253	241, 252	bitrdi 287	. . . . 5 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))))
254	133, 253	ralsn 4626	. . . 4 ⊢ (∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
255	237, 254	sylibr 234	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
256		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
257		nfra1 3262	. . . . . . 7 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
258	256, 257	nfan 1901	. . . . . 6 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
259		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
260		nfra2w 3274	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
261	259, 260	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
262		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))
263	261, 262	nfan 1901	. . . . . . 7 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
264		vieta.3	. . . . . . . . 9 ⊢ − = (-g‘𝑊)
265		eqid 2737	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅)
266		eqid 2737	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚})eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅)
267		vieta.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑅)
268		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
269		eqid 2737	. . . . . . . . 9 ⊢ (♯‘(𝑖 ∪ {𝑚})) = (♯‘(𝑖 ∪ {𝑚}))
270		vieta.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
271	270	ad5antr 735	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝐼 ∈ Fin)
272		simp-5r 786	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ⊆ 𝐼)
273	271, 272	ssfid 9172	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ∈ Fin)
274		snfi 8983	. . . . . . . . . . 11 ⊢ {𝑚} ∈ Fin
275	274	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → {𝑚} ∈ Fin)
276	273, 275	unfid 9099	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
277	115	ad5antr 735	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑅 ∈ IDomn)
278	24	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝐵 ∈ V)
279		simplr 769	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
280	276, 278, 279	elmaprd 32768	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧:(𝑖 ∪ {𝑚})⟶𝐵)
281		2fveq3 6839	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑧‘𝑜)))
282	281	oveq2d 7376	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑧‘𝑜))))
283	282	cbvmptv 5190	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜))))
284	283	oveq2i 7371	. . . . . . . . 9 ⊢ (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜)))))
285		fznn0sub2 13580	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
286	285	adantl 481	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
287		ssun2 4120	. . . . . . . . . . 11 ⊢ {𝑚} ⊆ (𝑖 ∪ {𝑚})
288		vsnid 4608	. . . . . . . . . . 11 ⊢ 𝑚 ∈ {𝑚}
289	287, 288	sselii 3919	. . . . . . . . . 10 ⊢ 𝑚 ∈ (𝑖 ∪ {𝑚})
290	289	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑚 ∈ (𝑖 ∪ {𝑚}))
291		eqid 2737	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = ((𝑖 ∪ {𝑚}) ∖ {𝑚})
292		fveq1 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑦 → (𝑧‘𝑛) = (𝑦‘𝑛))
293	292	fveq2d 6838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑦 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑦‘𝑛)))
294	293	oveq2d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑛))))
295	294	mpteq2dv 5180	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))
296	295	oveq2d 7376	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))
297	296	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))))
298	297	fveq1d 6836	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
299		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))
300	299	oveq2d 7376	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
301	298, 300	eqeq12d 2753	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
302	301	ralbidv 3161	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
303	302	cbvralvw 3216	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
304		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑚 ∈ (𝐼 ∖ 𝑖))
305	304	eldifbd 3903	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ¬ 𝑚 ∈ 𝑖)
306		disjsn 4656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∩ {𝑚}) = ∅ ↔ ¬ 𝑚 ∈ 𝑖)
307	305, 306	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∩ {𝑚}) = ∅)
308		undif5 4425	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∩ {𝑚}) = ∅ → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
309	307, 308	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
310	309	eqcomd 2743	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 = ((𝑖 ∪ {𝑚}) ∖ {𝑚}))
311	310	oveq2d 7376	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝐵 ↑m 𝑖) = (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚})))
312		oveq2 7368	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((♯‘𝑖) − 𝑘) = ((♯‘𝑖) − 𝑙))
313	312	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)))
314		oveq1 7367	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
315		2fveq3 6839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)))
316	315	fveq1d 6836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))
317	314, 316	oveq12d 7378	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
318	313, 317	eqeq12d 2753	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))))
319	318	cbvralvw 3216	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
320	310	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (♯‘𝑖) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
321	320	oveq2d 7376	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (0...(♯‘𝑖)) = (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))))
322		2fveq3 6839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑦‘𝑛)) = (𝐴‘(𝑦‘𝑜)))
323	322	oveq2d 7376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑦‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑜))))
324	323	cbvmptv 5190	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))
325	310	mpteq1d 5176	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
326	324, 325	eqtrid 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
327	326	oveq2d 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))
328	327	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))))
329	320	oveq1d 7375	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((♯‘𝑖) − 𝑙) = ((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙))
330	328, 329	fveq12d 6841	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)))
331	310	oveq1d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅))
332	310	oveq1d 7375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅))
333	332	fveq1d 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖eSymPoly𝑅)‘𝑙) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))
334	331, 333	fveq12d 6841	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙)))
335	334	fveq1d 6836	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦) = (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))
336	335	oveq2d 7376	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
337	330, 336	eqeq12d 2753	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
338	321, 337	raleqbidv 3312	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
339	319, 338	bitrid 283	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
340	311, 339	raleqbidv 3312	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
341	303, 340	bitrid 283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
342	341	biimpa 476	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
343	342	ad2antrr 727	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
344		eqid 2737	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)
345		eqid 2737	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)
346		eqid 2737	. . . . . . . . . 10 ⊢ (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))
347		difssd 4078	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ⊆ (𝑖 ∪ {𝑚}))
348	276, 347	ssfid 9172	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ∈ Fin)
349	280, 347	fssresd 6701	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚})):((𝑖 ∪ {𝑚}) ∖ {𝑚})⟶𝐵)
350		eqid 2737	. . . . . . . . . 10 ⊢ (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))
351		eqid 2737	. . . . . . . . . 10 ⊢ (deg1‘𝑅) = (deg1‘𝑅)
352	229, 23, 264, 230, 344, 345, 119, 114, 113, 267, 268, 125, 346, 348, 277, 349, 350, 351	vietadeg1 33737	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((deg1‘𝑅)‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
353	229, 23, 264, 230, 265, 266, 119, 114, 113, 267, 268, 125, 269, 276, 277, 280, 284, 286, 290, 291, 343, 352	vietalem 33738	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)))
354	270	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝐼 ∈ Fin)
355		simplr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ⊆ 𝐼)
356	354, 355	ssfid 9172	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ∈ Fin)
357	274	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → {𝑚} ∈ Fin)
358	356, 357	unfid 9099	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∪ {𝑚}) ∈ Fin)
359	358	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
360		hashcl 14309	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∪ {𝑚}) ∈ Fin → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
361	359, 360	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
362	361	nn0cnd 12491	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℂ)
363		elfznn0 13565	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → 𝑘 ∈ ℕ0)
364	363	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℕ0)
365	364	nn0cnd 12491	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℂ)
366	362, 365	nncand 11501	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = 𝑘)
367	366	oveq1d 7375	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
368	366	fveq2d 6838	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
369	368	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
370	369	fveq1d 6836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
371	367, 370	oveq12d 7378	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
372	371	ad4ant14 753	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
373	353, 372	eqtrd 2772	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
374	263, 373	ralrimia 3237	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) → ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
375	258, 374	ralrimia 3237	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
376	375	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
377	376	anasss 466	. . 3 ⊢ ((𝜑 ∧ (𝑖 ⊆ 𝐼 ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
378	55, 72, 89, 112, 255, 377, 270	findcard2d 9094	. 2 ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑m 𝐼)∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
379	24	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
380		vieta.z	. . 3 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
381	379, 270, 380	elmapdd 8781	. 2 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m 𝐼))
382		vieta.k	. 2 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
383	14, 21, 378, 381, 382	rspc2dv 3580	1 ⊢ (𝜑 → (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  {crab 3390  Vcvv 3430   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889   ⊆ wss 3890  ∅c0 4274  ifcif 4467  𝒫 cpw 4542  {csn 4568  {cpr 4570  ⟨cop 4574   class class class wbr 5086   ↦ cmpt 5167   × cxp 5622  ^◡ccnv 5623   ↾ cres 5626   “ cima 5627   ∘ ccom 5628   Fn wfn 6487  ⟶wf 6488  –1-1-onto→wf1o 6491  ‘cfv 6492  (class class class)co 7360   ↑_m cmap 8766  Fincfn 8886   finSupp cfsupp 9267  0cc0 11029  1c1 11030   − cmin 11368  𝟭cind 12150  ℕcn 12165  ℕ₀cn0 12428  ℤcz 12515  ...cfz 13452  ♯chash 14283  Basecbs 17170  ._rcmulr 17212  0_gc0g 17393   Σ_g cgsu 17394  inv_gcminusg 18901  -_gcsg 18902  ._gcmg 19034  mulGrpcmgp 20112  1_rcur 20153  Ringcrg 20205   RingHom crh 20440  IDomncidom 20661  ℤ_ringczring 21436  ℤRHomczrh 21489  algSccascl 21842   mPoly cmpl 21896   eval cevl 22061  var₁cv1 22149  Poly₁cpl1 22150  coe₁cco1 22151  deg₁cdg1 26029  eSymPolycesply 33715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108  ax-mulf 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-ofr 7625  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8104  df-tpos 8169  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-oadd 8402  df-er 8636  df-map 8768  df-pm 8769  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9268  df-sup 9348  df-oi 9418  df-dju 9816  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-ind 12151  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-xnn0 12502  df-z 12516  df-dec 12636  df-uz 12780  df-rp 12934  df-fz 13453  df-fzo 13600  df-seq 13955  df-exp 14015  df-fac 14227  df-bc 14256  df-hash 14284  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15441  df-sum 15640  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-starv 17226  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-hom 17235  df-cco 17236  df-0g 17395  df-gsum 17396  df-prds 17401  df-pws 17403  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mhm 18742  df-submnd 18743  df-grp 18903  df-minusg 18904  df-sbg 18905  df-mulg 19035  df-subg 19090  df-ghm 19179  df-cntz 19283  df-cmn 19748  df-abl 19749  df-mgp 20113  df-rng 20125  df-ur 20154  df-srg 20159  df-ring 20207  df-cring 20208  df-oppr 20308  df-dvdsr 20328  df-unit 20329  df-invr 20359  df-rhm 20443  df-nzr 20481  df-subrng 20514  df-subrg 20538  df-rlreg 20662  df-domn 20663  df-idom 20664  df-lmod 20848  df-lss 20918  df-lsp 20958  df-cnfld 21345  df-zring 21437  df-zrh 21493  df-assa 21843  df-asp 21844  df-ascl 21845  df-psr 21899  df-mvr 21900  df-mpl 21901  df-opsr 21903  df-evls 22062  df-evl 22063  df-psr1 22153  df-vr1 22154  df-ply1 22155  df-coe1 22156  df-mdeg 26030  df-deg1 26031  df-extv 33689  df-esply 33717

This theorem is referenced by: (None)