Theorem vieta 33771

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 26303 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 7379	. . . . . . . . 9 ⊢ (𝑧 = 𝑍 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
4	3	mpteq2dv 5173	. . . . . . . 8 ⊢ (𝑧 = 𝑍 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
5	4	oveq2d 7379	. . . . . . 7 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
6		vieta.f	. . . . . . 7 ⊢ 𝐹 = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
7	5, 6	eqtr4di 2793	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = 𝐹)
8	7	fveq2d 6838	. . . . 5 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘𝐹))
9		vieta.c	. . . . 5 ⊢ 𝐶 = (coe1‘𝐹)
10	8, 9	eqtr4di 2793	. . . 4 ⊢ (𝑧 = 𝑍 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = 𝐶)
11	10	fveq1d 6836	. . 3 ⊢ (𝑧 = 𝑍 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝑘)))
12		fveq2 6834	. . . 4 ⊢ (𝑧 = 𝑍 → ((𝑄‘(𝐸‘𝑘))‘𝑧) = ((𝑄‘(𝐸‘𝑘))‘𝑍))
13	12	oveq2d 7379	. . 3 ⊢ (𝑧 = 𝑍 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)))
14	11, 13	eqeq12d 2756	. 2 ⊢ (𝑧 = 𝑍 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)) ↔ (𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))))
15		oveq2 7371	. . . 4 ⊢ (𝑘 = 𝐾 → (𝐻 − 𝑘) = (𝐻 − 𝐾))
16	15	fveq2d 6838	. . 3 ⊢ (𝑘 = 𝐾 → (𝐶‘(𝐻 − 𝑘)) = (𝐶‘(𝐻 − 𝐾)))
17		oveq1 7370	. . . 4 ⊢ (𝑘 = 𝐾 → (𝑘 ↑ (𝑁‘ 1 )) = (𝐾 ↑ (𝑁‘ 1 )))
18		2fveq3 6839	. . . . 5 ⊢ (𝑘 = 𝐾 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝐾)))
19	18	fveq1d 6836	. . . 4 ⊢ (𝑘 = 𝐾 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝐾))‘𝑍))
20	17, 19	oveq12d 7381	. . 3 ⊢ (𝑘 = 𝐾 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))
21	16, 20	eqeq12d 2756	. 2 ⊢ (𝑘 = 𝐾 → ((𝐶‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ↔ (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍))))
22		oveq2 7371	. . . . 5 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = (𝐵 ↑m ∅))
23		vieta.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
24	23	fvexi 6848	. . . . . 6 ⊢ 𝐵 ∈ V
25		mapdm0 8786	. . . . . 6 ⊢ (𝐵 ∈ V → (𝐵 ↑m ∅) = {∅})
26	24, 25	ax-mp 5	. . . . 5 ⊢ (𝐵 ↑m ∅) = {∅}
27	22, 26	eqtrdi 2791	. . . 4 ⊢ (𝑗 = ∅ → (𝐵 ↑m 𝑗) = {∅})
28		fveq2 6834	. . . . . . 7 ⊢ (𝑗 = ∅ → (♯‘𝑗) = (♯‘∅))
29	28	oveq2d 7379	. . . . . 6 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = (0...(♯‘∅)))
30		hash0 14327	. . . . . . . 8 ⊢ (♯‘∅) = 0
31	30	oveq2i 7374	. . . . . . 7 ⊢ (0...(♯‘∅)) = (0...0)
32		fz0sn 13579	. . . . . . 7 ⊢ (0...0) = {0}
33	31, 32	eqtri 2763	. . . . . 6 ⊢ (0...(♯‘∅)) = {0}
34	29, 33	eqtrdi 2791	. . . . 5 ⊢ (𝑗 = ∅ → (0...(♯‘𝑗)) = {0})
35		mpteq1 5168	. . . . . . . . . . 11 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
36		mpt0 6634	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ∅ ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅
37	35, 36	eqtrdi 2791	. . . . . . . . . 10 ⊢ (𝑗 = ∅ → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = ∅)
38	37	oveq2d 7379	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg ∅))
39		eqid 2740	. . . . . . . . . 10 ⊢ (0g‘𝑀) = (0g‘𝑀)
40	39	gsum0 18650	. . . . . . . . 9 ⊢ (𝑀 Σg ∅) = (0g‘𝑀)
41	38, 40	eqtrdi 2791	. . . . . . . 8 ⊢ (𝑗 = ∅ → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (0g‘𝑀))
42	41	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = ∅ → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(0g‘𝑀)))
43	28	oveq1d 7378	. . . . . . . 8 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = ((♯‘∅) − 𝑘))
44	30	oveq1i 7373	. . . . . . . 8 ⊢ ((♯‘∅) − 𝑘) = (0 − 𝑘)
45	43, 44	eqtrdi 2791	. . . . . . 7 ⊢ (𝑗 = ∅ → ((♯‘𝑗) − 𝑘) = (0 − 𝑘))
46	42, 45	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = ∅ → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(0g‘𝑀))‘(0 − 𝑘)))
47		oveq1 7370	. . . . . . . . 9 ⊢ (𝑗 = ∅ → (𝑗 eval 𝑅) = (∅ eval 𝑅))
48		oveq1 7370	. . . . . . . . . 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 7379	. . . . . 6 ⊢ (𝑗 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
53	46, 52	eqeq12d 2756	. . . . 5 ⊢ (𝑗 = ∅ → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
54	34, 53	raleqbidv 3314	. . . 4 ⊢ (𝑗 = ∅ → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
55	27, 54	raleqbidv 3314	. . 3 ⊢ (𝑗 = ∅ → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧))))
56		oveq2 7371	. . . 4 ⊢ (𝑗 = 𝑖 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝑖))
57		fveq2 6834	. . . . . 6 ⊢ (𝑗 = 𝑖 → (♯‘𝑗) = (♯‘𝑖))
58	57	oveq2d 7379	. . . . 5 ⊢ (𝑗 = 𝑖 → (0...(♯‘𝑗)) = (0...(♯‘𝑖)))
59		mpteq1 5168	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
60	59	oveq2d 7379	. . . . . . . 8 ⊢ (𝑗 = 𝑖 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
61	60	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
62	57	oveq1d 7378	. . . . . . 7 ⊢ (𝑗 = 𝑖 → ((♯‘𝑗) − 𝑘) = ((♯‘𝑖) − 𝑘))
63	61, 62	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
64		oveq1 7370	. . . . . . . . 9 ⊢ (𝑗 = 𝑖 → (𝑗 eval 𝑅) = (𝑖 eval 𝑅))
65		oveq1 7370	. . . . . . . . . 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 7379	. . . . . 6 ⊢ (𝑗 = 𝑖 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
70	63, 69	eqeq12d 2756	. . . . 5 ⊢ (𝑗 = 𝑖 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
71	58, 70	raleqbidv 3314	. . . 4 ⊢ (𝑗 = 𝑖 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
72	56, 71	raleqbidv 3314	. . 3 ⊢ (𝑗 = 𝑖 → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))))
73		oveq2 7371	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝐵 ↑m 𝑗) = (𝐵 ↑m (𝑖 ∪ {𝑚})))
74		fveq2 6834	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (♯‘𝑗) = (♯‘(𝑖 ∪ {𝑚})))
75	74	oveq2d 7379	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (0...(♯‘𝑗)) = (0...(♯‘(𝑖 ∪ {𝑚}))))
76		mpteq1 5168	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
77	76	oveq2d 7379	. . . . . . . 8 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
78	77	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
79	74	oveq1d 7378	. . . . . . 7 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((♯‘𝑗) − 𝑘) = ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))
80	78, 79	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))
81		oveq1 7370	. . . . . . . . 9 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (𝑗 eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅))
82		oveq1 7370	. . . . . . . . . 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 7379	. . . . . 6 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
87	80, 86	eqeq12d 2756	. . . . 5 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
88	75, 87	raleqbidv 3314	. . . 4 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
89	73, 88	raleqbidv 3314	. . 3 ⊢ (𝑗 = (𝑖 ∪ {𝑚}) → (∀𝑧 ∈ (𝐵 ↑m 𝑗)∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
90		oveq2 7371	. . . 4 ⊢ (𝑗 = 𝐼 → (𝐵 ↑m 𝑗) = (𝐵 ↑m 𝐼))
91		fveq2 6834	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = (♯‘𝐼))
92		vieta.h	. . . . . . 7 ⊢ 𝐻 = (♯‘𝐼)
93	91, 92	eqtr4di 2793	. . . . . 6 ⊢ (𝑗 = 𝐼 → (♯‘𝑗) = 𝐻)
94	93	oveq2d 7379	. . . . 5 ⊢ (𝑗 = 𝐼 → (0...(♯‘𝑗)) = (0...𝐻))
95		mpteq1 5168	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))
96	95	oveq2d 7379	. . . . . . . 8 ⊢ (𝑗 = 𝐼 → (𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))
97	96	fveq2d 6838	. . . . . . 7 ⊢ (𝑗 = 𝐼 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))))
98	93	oveq1d 7378	. . . . . . 7 ⊢ (𝑗 = 𝐼 → ((♯‘𝑗) − 𝑘) = (𝐻 − 𝑘))
99	97, 98	fveq12d 6841	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)))
100		oveq1 7370	. . . . . . . . . 10 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = (𝐼 eval 𝑅))
101		vieta.q	. . . . . . . . . 10 ⊢ 𝑄 = (𝐼 eval 𝑅)
102	100, 101	eqtr4di 2793	. . . . . . . . 9 ⊢ (𝑗 = 𝐼 → (𝑗 eval 𝑅) = 𝑄)
103		oveq1 7370	. . . . . . . . . . 11 ⊢ (𝑗 = 𝐼 → (𝑗eSymPoly𝑅) = (𝐼eSymPoly𝑅))
104		vieta.e	. . . . . . . . . . 11 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
105	103, 104	eqtr4di 2793	. . . . . . . . . 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 7379	. . . . . 6 ⊢ (𝑗 = 𝐼 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
110	99, 109	eqeq12d 2756	. . . . 5 ⊢ (𝑗 = 𝐼 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
111	94, 110	raleqbidv 3314	. . . 4 ⊢ (𝑗 = 𝐼 → (∀𝑘 ∈ (0...(♯‘𝑗))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑗 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑗) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑗 eval 𝑅)‘((𝑗eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧))))
112	90, 111	raleqbidv 3314	. . 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 20707	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ Ring)
117	23, 114, 116	ringidcld 20245	. . . . . 6 ⊢ (𝜑 → 1 ∈ 𝐵)
118	23, 113, 114, 116, 117	ringlidmd 20251	. . . . 5 ⊢ (𝜑 → ( 1 · 1 ) = 1 )
119		vieta.n	. . . . . . . 8 ⊢ 𝑁 = (invg‘𝑅)
120	116	ringgrpd 20221	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Grp)
121	23, 119, 120, 117	grpinvcld 18962	. . . . . . 7 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
122		eqid 2740	. . . . . . . . 9 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
123	122, 23	mgpbas 20124	. . . . . . . 8 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
124	122, 114	ringidval 20162	. . . . . . . 8 ⊢ 1 = (0g‘(mulGrp‘𝑅))
125		vieta.p	. . . . . . . 8 ⊢ ↑ = (.g‘(mulGrp‘𝑅))
126	123, 124, 125	mulg0 19048	. . . . . . 7 ⊢ ((𝑁‘ 1 ) ∈ 𝐵 → (0 ↑ (𝑁‘ 1 )) = 1 )
127	121, 126	syl 17	. . . . . 6 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) = 1 )
128		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (ℤRHom‘𝑅) = (ℤRHom‘𝑅)
129	128, 114	zrh1 21494	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → ((ℤRHom‘𝑅)‘1) = 1 )
130	116, 129	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((ℤRHom‘𝑅)‘1) = 1 )
131	130	sneqd 4574	. . . . . . . . . . . 12 ⊢ (𝜑 → {((ℤRHom‘𝑅)‘1)} = { 1 })
132	131	xpeq2d 5655	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = ({∅} × { 1 }))
133		0ex 5236	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
134	133	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ∈ V)
135	114	fvexi 6848	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
136	135	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ V)
137		xpsng 7088	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ 1 ∈ V) → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
138	134, 136, 137	syl2anc 590	. . . . . . . . . . 11 ⊢ (𝜑 → ({∅} × { 1 }) = {⟨∅, 1 ⟩})
139		0xp 5724	. . . . . . . . . . . . . . . 16 ⊢ (∅ × {0}) = ∅
140	139	eqcomi 2749	. . . . . . . . . . . . . . 15 ⊢ ∅ = (∅ × {0})
141	140	eqeq2i 2753	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ∅ ↔ 𝑓 = (∅ × {0}))
142	141	bilani 505	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 = ∅) → 𝑓 = (∅ × {0}))
143	142	iftrued 4469	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 = ∅) → if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅)) = 1 )
144	143, 134, 136	fmptsnd 7120	. . . . . . . . . . 11 ⊢ (𝜑 → {⟨∅, 1 ⟩} = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
145	132, 138, 144	3eqtrd 2779	. . . . . . . . . 10 ⊢ (𝜑 → ({∅} × {((ℤRHom‘𝑅)‘1)}) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
146		elsni 4579	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ {∅} → ℎ = ∅)
147		nn0ex 12441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ0 ∈ V
148		mapdm0 8786	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ0 ∈ V → (ℕ0 ↑m ∅) = {∅})
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℕ0 ↑m ∅) = {∅}
150	146, 149	eleq2s 2858	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ℎ = ∅)
151	150	cnveqd 5824	. . . . . . . . . . . . . . . . . 18 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → ◡ℎ = ◡∅)
152	151	imaeq1d 6018	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = (◡∅ “ ℕ))
153		cnv0 6097	. . . . . . . . . . . . . . . . . . 19 ⊢ ◡∅ = ∅
154	153	imaeq1i 6016	. . . . . . . . . . . . . . . . . 18 ⊢ (◡∅ “ ℕ) = (∅ “ ℕ)
155		0ima 6037	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ “ ℕ) = ∅
156	154, 155	eqtri 2763	. . . . . . . . . . . . . . . . 17 ⊢ (◡∅ “ ℕ) = ∅
157	152, 156	eqtrdi 2791	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) = ∅)
158		0fi 8986	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ Fin
159	157, 158	eqeltrdi 2848	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ (ℕ0 ↑m ∅) → (◡ℎ “ ℕ) ∈ Fin)
160	159	rabeqc 3404	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin} = (ℕ0 ↑m ∅)
161	160, 149	eqtr2i 2764	. . . . . . . . . . . . 13 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
162		eqid 2740	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
163	162	psrbasfsupp 33702	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ (◡ℎ “ ℕ) ∈ Fin}
164	161, 163	eqtr4i 2766	. . . . . . . . . . . 12 ⊢ {∅} = {ℎ ∈ (ℕ0 ↑m ∅) ∣ ℎ finSupp 0}
165		0nn0 12450	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ0
166	165	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ0)
167	164, 134, 115, 166	esplyfval 33754	. . . . . . . . . . 11 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))))
168		fveqeq2 6843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = ∅ → ((♯‘𝑐) = 0 ↔ (♯‘∅) = 0))
169		0elpw 5291	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ 𝒫 ∅
170	169	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∅ ∈ 𝒫 ∅)
171	30	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (♯‘∅) = 0)
172		hasheq0 14323	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ 𝒫 ∅ → ((♯‘𝑐) = 0 ↔ 𝑐 = ∅))
173	172	biimpa 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ∈ 𝒫 ∅ ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
174	173	adantll 720	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ 𝒫 ∅) ∧ (♯‘𝑐) = 0) → 𝑐 = ∅)
175	168, 170, 171, 174	rabeqsnd 4608	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0} = {∅})
176	175	imaeq2d 6019	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = ((𝟭‘∅) “ {∅}))
177		pw0 4750	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝒫 ∅ = {∅}
178	177	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝒫 ∅ = {∅})
179		indf1o 32950	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ V → (𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅))
180		f1of 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝟭‘∅):𝒫 ∅–1-1-onto→({0, 1} ↑m ∅) → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
181	134, 179, 180	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝟭‘∅):𝒫 ∅⟶({0, 1} ↑m ∅))
182	178, 181	feq2dd 6648	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝟭‘∅):{∅}⟶({0, 1} ↑m ∅))
183	182	ffnd 6663	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝟭‘∅) Fn {∅})
184	133	snid 4601	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ {∅}
185	184	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∅ ∈ {∅})
186	183, 185	fnimasnd 7316	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝟭‘∅) “ {∅}) = {((𝟭‘∅)‘∅)})
187		ssidd 3945	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∅ ⊆ ∅)
188		indf 12163	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ V ∧ ∅ ⊆ ∅) → ((𝟭‘∅)‘∅):∅⟶{0, 1})
189	134, 187, 188	syl2anc 590	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝟭‘∅)‘∅):∅⟶{0, 1})
190		f0bi 6717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝟭‘∅)‘∅):∅⟶{0, 1} ↔ ((𝟭‘∅)‘∅) = ∅)
191	189, 190	sylib 219	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝟭‘∅)‘∅) = ∅)
192	191	sneqd 4574	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {((𝟭‘∅)‘∅)} = {∅})
193	176, 186, 192	3eqtrd 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}) = {∅})
194	193	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ((𝟭‘{∅})‘{∅}))
195		p0ex 5320	. . . . . . . . . . . . . 14 ⊢ {∅} ∈ V
196		indconst1 12170	. . . . . . . . . . . . . 14 ⊢ ({∅} ∈ V → ((𝟭‘{∅})‘{∅}) = ({∅} × {1}))
197	195, 196	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((𝟭‘{∅})‘{∅}) = ({∅} × {1})
198	194, 197	eqtrdi 2791	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0})) = ({∅} × {1}))
199	198	coeq2d 5811	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ((𝟭‘{∅})‘((𝟭‘∅) “ {𝑐 ∈ 𝒫 ∅ ∣ (♯‘𝑐) = 0}))) = ((ℤRHom‘𝑅) ∘ ({∅} × {1})))
200	128	zrhrhm 21493	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅))
201		zringbas 21435	. . . . . . . . . . . . . . 15 ⊢ ℤ = (Base‘ℤring)
202	201, 23	rhmf 20462	. . . . . . . . . . . . . 14 ⊢ ((ℤRHom‘𝑅) ∈ (ℤring RingHom 𝑅) → (ℤRHom‘𝑅):ℤ⟶𝐵)
203	116, 200, 202	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤRHom‘𝑅):ℤ⟶𝐵)
204	203	ffnd 6663	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤRHom‘𝑅) Fn ℤ)
205		1zzd 12556	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℤ)
206		fcoconst 7083	. . . . . . . . . . . 12 ⊢ (((ℤRHom‘𝑅) Fn ℤ ∧ 1 ∈ ℤ) → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
207	204, 205, 206	syl2anc 590	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℤRHom‘𝑅) ∘ ({∅} × {1})) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
208	167, 199, 207	3eqtrd 2779	. . . . . . . . . 10 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ({∅} × {((ℤRHom‘𝑅)‘1)}))
209		eqid 2740	. . . . . . . . . . 11 ⊢ (∅ mPoly 𝑅) = (∅ mPoly 𝑅)
210		eqid 2740	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
211		eqid 2740	. . . . . . . . . . 11 ⊢ (algSc‘(∅ mPoly 𝑅)) = (algSc‘(∅ mPoly 𝑅))
212	209, 161, 210, 23, 211, 134, 116, 117	mplascl 22047	. . . . . . . . . 10 ⊢ (𝜑 → ((algSc‘(∅ mPoly 𝑅))‘ 1 ) = (𝑓 ∈ {∅} ↦ if(𝑓 = (∅ × {0}), 1 , (0g‘𝑅))))
213	145, 208, 212	3eqtr4d 2785	. . . . . . . . 9 ⊢ (𝜑 → ((∅eSymPoly𝑅)‘0) = ((algSc‘(∅ mPoly 𝑅))‘ 1 ))
214	213	fveq2d 6838	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)) = ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )))
215	214	fveq1d 6836	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅))
216		eqid 2740	. . . . . . . . 9 ⊢ (∅ eval 𝑅) = (∅ eval 𝑅)
217	184, 149	eleqtrri 2839	. . . . . . . . . 10 ⊢ ∅ ∈ (ℕ0 ↑m ∅)
218	217	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ∅ ∈ (ℕ0 ↑m ∅))
219	115	idomcringd 20706	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ CRing)
220	216, 209, 23, 211, 218, 219, 117	evlsca 22089	. . . . . . . 8 ⊢ (𝜑 → ((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 )) = ((𝐵 ↑m ∅) × { 1 }))
221	220	fveq1d 6836	. . . . . . 7 ⊢ (𝜑 → (((∅ eval 𝑅)‘((algSc‘(∅ mPoly 𝑅))‘ 1 ))‘∅) = (((𝐵 ↑m ∅) × { 1 })‘∅))
222	184, 26	eleqtrri 2839	. . . . . . . 8 ⊢ ∅ ∈ (𝐵 ↑m ∅)
223	135	fvconst2 7155	. . . . . . . 8 ⊢ (∅ ∈ (𝐵 ↑m ∅) → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
224	222, 223	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (((𝐵 ↑m ∅) × { 1 })‘∅) = 1 )
225	215, 221, 224	3eqtrd 2779	. . . . . 6 ⊢ (𝜑 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅) = 1 )
226	127, 225	oveq12d 7381	. . . . 5 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)) = ( 1 · 1 ))
227		iftrue 4467	. . . . . 6 ⊢ (𝑙 = 0 → if(𝑙 = 0, 1 , (0g‘𝑅)) = 1 )
228		vieta.w	. . . . . . . 8 ⊢ 𝑊 = (Poly1‘𝑅)
229		vieta.m	. . . . . . . . . 10 ⊢ 𝑀 = (mulGrp‘𝑊)
230		eqid 2740	. . . . . . . . . 10 ⊢ (1r‘𝑊) = (1r‘𝑊)
231	229, 230	ringidval 20162	. . . . . . . . 9 ⊢ (1r‘𝑊) = (0g‘𝑀)
232	231	eqcomi 2749	. . . . . . . 8 ⊢ (0g‘𝑀) = (1r‘𝑊)
233	228, 232, 210, 114	coe1id 22286	. . . . . . 7 ⊢ (𝑅 ∈ Ring → (coe1‘(0g‘𝑀)) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, 1 , (0g‘𝑅))))
234	116, 233	syl 17	. . . . . 6 ⊢ (𝜑 → (coe1‘(0g‘𝑀)) = (𝑙 ∈ ℕ0 ↦ if(𝑙 = 0, 1 , (0g‘𝑅))))
235	227, 234, 166, 136	fvmptd4 6967	. . . . 5 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = 1 )
236	118, 226, 235	3eqtr4rd 2786	. . . 4 ⊢ (𝜑 → ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
237		fveq2 6834	. . . . . . . . 9 ⊢ (𝑧 = ∅ → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))
238	237	oveq2d 7379	. . . . . . . 8 ⊢ (𝑧 = ∅ → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)))
239	238	eqeq2d 2751	. . . . . . 7 ⊢ (𝑧 = ∅ → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
240	239	ralbidv 3163	. . . . . 6 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅))))
241		c0ex 11136	. . . . . . 7 ⊢ 0 ∈ V
242		oveq2 7371	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (0 − 𝑘) = (0 − 0))
243		0m0e0 12294	. . . . . . . . . 10 ⊢ (0 − 0) = 0
244	242, 243	eqtrdi 2791	. . . . . . . . 9 ⊢ (𝑘 = 0 → (0 − 𝑘) = 0)
245	244	fveq2d 6838	. . . . . . . 8 ⊢ (𝑘 = 0 → ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((coe1‘(0g‘𝑀))‘0))
246		oveq1 7370	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑘 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
247		2fveq3 6839	. . . . . . . . . 10 ⊢ (𝑘 = 0 → ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘)) = ((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0)))
248	247	fveq1d 6836	. . . . . . . . 9 ⊢ (𝑘 = 0 → (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅) = (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))
249	246, 248	oveq12d 7381	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
250	245, 249	eqeq12d 2756	. . . . . . 7 ⊢ (𝑘 = 0 → (((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))))
251	241, 250	ralsn 4620	. . . . . 6 ⊢ (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘∅)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
252	240, 251	bitrdi 288	. . . . 5 ⊢ (𝑧 = ∅ → (∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅))))
253	133, 252	ralsn 4620	. . . 4 ⊢ (∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(0g‘𝑀))‘0) = ((0 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘0))‘∅)))
254	236, 253	sylibr 235	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ {∅}∀𝑘 ∈ {0} ((coe1‘(0g‘𝑀))‘(0 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((∅ eval 𝑅)‘((∅eSymPoly𝑅)‘𝑘))‘𝑧)))
255		nfv 1921	. . . . . . 7 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
256		nfra1 3264	. . . . . . 7 ⊢ Ⅎ𝑧∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
257	255, 256	nfan 1906	. . . . . 6 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
258		nfv 1921	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))
259		nfra2w 3276	. . . . . . . . 9 ⊢ Ⅎ𝑘∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))
260	258, 259	nfan 1906	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)))
261		nfv 1921	. . . . . . . 8 ⊢ Ⅎ𝑘 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))
262	260, 261	nfan 1906	. . . . . . 7 ⊢ Ⅎ𝑘((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
263		vieta.3	. . . . . . . . 9 ⊢ − = (-g‘𝑊)
264		eqid 2740	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) eval 𝑅) = ((𝑖 ∪ {𝑚}) eval 𝑅)
265		eqid 2740	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚})eSymPoly𝑅) = ((𝑖 ∪ {𝑚})eSymPoly𝑅)
266		vieta.x	. . . . . . . . 9 ⊢ 𝑋 = (var1‘𝑅)
267		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
268		eqid 2740	. . . . . . . . 9 ⊢ (♯‘(𝑖 ∪ {𝑚})) = (♯‘(𝑖 ∪ {𝑚}))
269		vieta.i	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ Fin)
270	269	ad5antr 740	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝐼 ∈ Fin)
271		simp-5r 791	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ⊆ 𝐼)
272	270, 271	ssfid 9176	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑖 ∈ Fin)
273		snfi 8987	. . . . . . . . . . 11 ⊢ {𝑚} ∈ Fin
274	273	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → {𝑚} ∈ Fin)
275	272, 274	unfid 9103	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
276	115	ad5antr 740	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑅 ∈ IDomn)
277	24	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝐵 ∈ V)
278		simplr 774	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚})))
279	275, 277, 278	elmaprd 32779	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑧:(𝑖 ∪ {𝑚})⟶𝐵)
280		2fveq3 6839	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑧‘𝑜)))
281	280	oveq2d 7379	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑧‘𝑜))))
282	281	cbvmptv 5183	. . . . . . . . . 10 ⊢ (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜))))
283	282	oveq2i 7374	. . . . . . . . 9 ⊢ (𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑜 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑜)))))
284		fznn0sub2 13587	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
285	284	adantl 482	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − 𝑘) ∈ (0...(♯‘(𝑖 ∪ {𝑚}))))
286		ssun2 4115	. . . . . . . . . . 11 ⊢ {𝑚} ⊆ (𝑖 ∪ {𝑚})
287		vsnid 4602	. . . . . . . . . . 11 ⊢ 𝑚 ∈ {𝑚}
288	286, 287	sselii 3919	. . . . . . . . . 10 ⊢ 𝑚 ∈ (𝑖 ∪ {𝑚})
289	288	a1i 11	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑚 ∈ (𝑖 ∪ {𝑚}))
290		eqid 2740	. . . . . . . . 9 ⊢ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = ((𝑖 ∪ {𝑚}) ∖ {𝑚})
291		fveq1 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑦 → (𝑧‘𝑛) = (𝑦‘𝑛))
292	291	fveq2d 6838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑦 → (𝐴‘(𝑧‘𝑛)) = (𝐴‘(𝑦‘𝑛)))
293	292	oveq2d 7379	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑦 → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑛))))
294	293	mpteq2dv 5173	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 𝑦 → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))
295	294	oveq2d 7379	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑦 → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))
296	295	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))))
297	296	fveq1d 6836	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)))
298		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑦 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))
299	298	oveq2d 7379	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
300	297, 299	eqeq12d 2756	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
301	300	ralbidv 3163	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦))))
302	301	cbvralvw 3218	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)))
303		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑚 ∈ (𝐼 ∖ 𝑖))
304	303	eldifbd 3903	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ¬ 𝑚 ∈ 𝑖)
305		disjsn 4650	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∩ {𝑚}) = ∅ ↔ ¬ 𝑚 ∈ 𝑖)
306	304, 305	sylibr 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∩ {𝑚}) = ∅)
307		undif5 4419	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∩ {𝑚}) = ∅ → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
308	306, 307	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) = 𝑖)
309	308	eqcomd 2746	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 = ((𝑖 ∪ {𝑚}) ∖ {𝑚}))
310	309	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝐵 ↑m 𝑖) = (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚})))
311		oveq2 7371	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → ((♯‘𝑖) − 𝑘) = ((♯‘𝑖) − 𝑙))
312	311	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)))
313		oveq1 7370	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
314		2fveq3 6839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑙 → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘)) = ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)))
315	314	fveq1d 6836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑙 → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦) = (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))
316	313, 315	oveq12d 7381	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
317	312, 316	eqeq12d 2756	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑙 → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦))))
318	317	cbvralvw 3218	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)))
319	309	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (♯‘𝑖) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
320	319	oveq2d 7379	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (0...(♯‘𝑖)) = (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))))
321		2fveq3 6839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑜 → (𝐴‘(𝑦‘𝑛)) = (𝐴‘(𝑦‘𝑜)))
322	321	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑜 → (𝑋 − (𝐴‘(𝑦‘𝑛))) = (𝑋 − (𝐴‘(𝑦‘𝑜))))
323	322	cbvmptv 5183	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))
324	309	mpteq1d 5169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑜 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
325	323, 324	eqtrid 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))) = (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))
326	325	oveq2d 7379	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))
327	326	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛)))))) = (coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜)))))))
328	319	oveq1d 7378	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((♯‘𝑖) − 𝑙) = ((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙))
329	327, 328	fveq12d 6841	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)))
330	309	oveq1d 7378	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅))
331	309	oveq1d 7378	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅))
332	331	fveq1d 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖eSymPoly𝑅)‘𝑙) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))
333	330, 332	fveq12d 6841	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙)) = ((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙)))
334	333	fveq1d 6836	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦) = (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))
335	334	oveq2d 7379	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
336	329, 335	eqeq12d 2756	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
337	320, 336	raleqbidv 3314	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑙 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑙))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
338	318, 337	bitrid 284	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
339	310, 338	raleqbidv 3314	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑦 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑦‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑦)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
340	302, 339	bitrid 284	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦))))
341	340	biimpa 477	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
342	341	ad2antrr 732	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ∀𝑦 ∈ (𝐵 ↑m ((𝑖 ∪ {𝑚}) ∖ {𝑚}))∀𝑙 ∈ (0...(♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))((coe1‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑦‘𝑜))))))‘((♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) − 𝑙)) = ((𝑙 ↑ (𝑁‘ 1 )) · (((((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)‘((((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)‘𝑙))‘𝑦)))
343		eqid 2740	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚}) eval 𝑅)
344		eqid 2740	. . . . . . . . . 10 ⊢ (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅) = (((𝑖 ∪ {𝑚}) ∖ {𝑚})eSymPoly𝑅)
345		eqid 2740	. . . . . . . . . 10 ⊢ (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚}))
346		difssd 4074	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ⊆ (𝑖 ∪ {𝑚}))
347	275, 346	ssfid 9176	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ∈ Fin)
348	279, 346	fssresd 6701	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚})):((𝑖 ∪ {𝑚}) ∖ {𝑚})⟶𝐵)
349		eqid 2740	. . . . . . . . . 10 ⊢ (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜))))) = (𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))
350		eqid 2740	. . . . . . . . . 10 ⊢ (deg1‘𝑅) = (deg1‘𝑅)
351	228, 23, 263, 229, 343, 344, 119, 114, 113, 266, 267, 125, 345, 347, 276, 348, 349, 350	vietadeg1 33769	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((deg1‘𝑅)‘(𝑀 Σg (𝑜 ∈ ((𝑖 ∪ {𝑚}) ∖ {𝑚}) ↦ (𝑋 − (𝐴‘((𝑧 ↾ ((𝑖 ∪ {𝑚}) ∖ {𝑚}))‘𝑜)))))) = (♯‘((𝑖 ∪ {𝑚}) ∖ {𝑚})))
352	228, 23, 263, 229, 264, 265, 119, 114, 113, 266, 267, 125, 268, 275, 276, 279, 283, 285, 289, 290, 342, 351	vietalem 33770	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)))
353	269	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝐼 ∈ Fin)
354		simplr 774	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ⊆ 𝐼)
355	353, 354	ssfid 9176	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → 𝑖 ∈ Fin)
356	273	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → {𝑚} ∈ Fin)
357	355, 356	unfid 9103	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (𝑖 ∪ {𝑚}) ∈ Fin)
358	357	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (𝑖 ∪ {𝑚}) ∈ Fin)
359		hashcl 14316	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∪ {𝑚}) ∈ Fin → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
360	358, 359	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℕ0)
361	360	nn0cnd 12498	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (♯‘(𝑖 ∪ {𝑚})) ∈ ℂ)
362		elfznn0 13572	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚}))) → 𝑘 ∈ ℕ0)
363	362	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℕ0)
364	363	nn0cnd 12498	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → 𝑘 ∈ ℂ)
365	361, 364	nncand 11508	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = 𝑘)
366	365	oveq1d 7378	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
367	365	fveq2d 6838	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))) = (((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))
368	367	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)))) = (((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘)))
369	368	fveq1d 6836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧) = ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))
370	366, 369	oveq12d 7381	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
371	370	ad4ant14 758	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘((♯‘(𝑖 ∪ {𝑚})) − ((♯‘(𝑖 ∪ {𝑚})) − 𝑘))))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
372	352, 371	eqtrd 2775	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) ∧ 𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))) → ((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
373	262, 372	ralrimia 3239	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) ∧ 𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))) → ∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
374	257, 373	ralrimia 3239	. . . . 5 ⊢ ((((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) ∧ ∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧))) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧)))
375	374	ex 413	. . . 4 ⊢ (((𝜑 ∧ 𝑖 ⊆ 𝐼) ∧ 𝑚 ∈ (𝐼 ∖ 𝑖)) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
376	375	anasss 467	. . 3 ⊢ ((𝜑 ∧ (𝑖 ⊆ 𝐼 ∧ 𝑚 ∈ (𝐼 ∖ 𝑖))) → (∀𝑧 ∈ (𝐵 ↑m 𝑖)∀𝑘 ∈ (0...(♯‘𝑖))((coe1‘(𝑀 Σg (𝑛 ∈ 𝑖 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝑖) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝑖 eval 𝑅)‘((𝑖eSymPoly𝑅)‘𝑘))‘𝑧)) → ∀𝑧 ∈ (𝐵 ↑m (𝑖 ∪ {𝑚}))∀𝑘 ∈ (0...(♯‘(𝑖 ∪ {𝑚})))((coe1‘(𝑀 Σg (𝑛 ∈ (𝑖 ∪ {𝑚}) ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘(𝑖 ∪ {𝑚})) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝑖 ∪ {𝑚}) eval 𝑅)‘(((𝑖 ∪ {𝑚})eSymPoly𝑅)‘𝑘))‘𝑧))))
377	55, 72, 89, 112, 254, 376, 269	findcard2d 9098	. 2 ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑m 𝐼)∀𝑘 ∈ (0...𝐻)((coe1‘(𝑀 Σg (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘(𝐻 − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑧)))
378	24	a1i 11	. . 3 ⊢ (𝜑 → 𝐵 ∈ V)
379		vieta.z	. . 3 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
380	378, 269, 379	elmapdd 8785	. 2 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m 𝐼))
381		vieta.k	. 2 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
382	14, 21, 377, 380, 381	rspc2dv 3582	1 ⊢ (𝜑 → (𝐶‘(𝐻 − 𝐾)) = ((𝐾 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐾))‘𝑍)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3054  {crab 3392  Vcvv 3432   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889   ⊆ wss 3890  ∅c0 4268  ifcif 4461  𝒫 cpw 4536  {csn 4562  {cpr 4564  ⟨cop 4568   class class class wbr 5079   ↦ cmpt 5160   × cxp 5623  ^◡ccnv 5624   ↾ cres 5627   “ cima 5628   ∘ ccom 5629   Fn wfn 6487  ⟶wf 6488  –1-1-onto→wf1o 6491  ‘cfv 6492  (class class class)co 7363   ↑_m cmap 8770  Fincfn 8890   finSupp cfsupp 9271  0cc0 11036  1c1 11037   − cmin 11375  𝟭cind 12157  ℕcn 12172  ℕ₀cn0 12435  ℤcz 12522  ...cfz 13459  ♯chash 14290  Basecbs 17177  ._rcmulr 17219  0_gc0g 17400   Σ_g cgsu 17401  inv_gcminusg 18908  -_gcsg 18909  ._gcmg 19041  mulGrpcmgp 20119  1_rcur 20160  Ringcrg 20212   RingHom crh 20447  IDomncidom 20672  ℤ_ringczring 21428  ℤRHomczrh 21481  algSccascl 21834   mPoly cmpl 21888   eval cevl 22056  var₁cv1 22168  Poly₁cpl1 22169  coe₁cco1 22170  deg₁cdg1 26044  eSymPolycesply 33747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-inf2 9560  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113  ax-pre-sup 11114  ax-addf 11115  ax-mulf 11116

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-iin 4931  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-of 7627  df-ofr 7628  df-om 7814  df-1st 7938  df-2nd 7939  df-supp 8108  df-tpos 8173  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-2o 8403  df-oadd 8406  df-er 8640  df-map 8772  df-pm 8773  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9272  df-sup 9352  df-oi 9422  df-dju 9823  df-card 9861  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-div 11806  df-ind 12158  df-nn 12173  df-2 12242  df-3 12243  df-4 12244  df-5 12245  df-6 12246  df-7 12247  df-8 12248  df-9 12249  df-n0 12436  df-xnn0 12509  df-z 12523  df-dec 12643  df-uz 12787  df-rp 12941  df-fz 13460  df-fzo 13607  df-seq 13962  df-exp 14022  df-fac 14234  df-bc 14263  df-hash 14291  df-cj 15059  df-re 15060  df-im 15061  df-sqrt 15195  df-abs 15196  df-clim 15448  df-sum 15647  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-plusg 17231  df-mulr 17232  df-starv 17233  df-sca 17234  df-vsca 17235  df-ip 17236  df-tset 17237  df-ple 17238  df-ds 17240  df-unif 17241  df-hom 17242  df-cco 17243  df-0g 17402  df-gsum 17403  df-prds 17408  df-pws 17410  df-mre 17546  df-mrc 17547  df-acs 17549  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-mhm 18749  df-submnd 18750  df-grp 18910  df-minusg 18911  df-sbg 18912  df-mulg 19042  df-subg 19097  df-ghm 19186  df-cntz 19290  df-cmn 19755  df-abl 19756  df-mgp 20120  df-rng 20132  df-ur 20161  df-srg 20166  df-ring 20214  df-cring 20215  df-oppr 20315  df-dvdsr 20335  df-unit 20336  df-invr 20366  df-rhm 20450  df-nzr 20492  df-subrng 20525  df-subrg 20549  df-rlreg 20673  df-domn 20674  df-idom 20675  df-lmod 20859  df-lss 20929  df-lsp 20969  df-cnfld 21355  df-zring 21429  df-zrh 21485  df-assa 21835  df-asp 21836  df-ascl 21837  df-psr 21891  df-mvr 21892  df-mpl 21893  df-opsr 21895  df-evls 22057  df-evl 22058  df-psr1 22172  df-vr1 22173  df-ply1 22174  df-coe1 22175  df-mdeg 26045  df-deg1 26046  df-extv 33721  df-esply 33749

This theorem is referenced by: (None)