vietalem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > vietalem		Structured version Visualization version GIF version

Theorem vietalem 33723

Description: Lemma for vieta 33724: induction step. (Contributed by Thierry Arnoux, 15-Feb-2026.)

**Hypotheses**
Ref	Expression
vieta.w	⊢ 𝑊 = (Poly₁‘𝑅)
vieta.b	⊢ 𝐵 = (Base‘𝑅)
vieta.3	⊢ − = (-_g‘𝑊)
vieta.m	⊢ 𝑀 = (mulGrp‘𝑊)
vieta.q	⊢ 𝑄 = (𝐼 eval 𝑅)
vieta.e	⊢ 𝐸 = (𝐼eSymPoly𝑅)
vieta.n	⊢ 𝑁 = (inv_g‘𝑅)
vieta.1	⊢ 1 = (1_r‘𝑅)
vieta.t	⊢ · = (._r‘𝑅)
vieta.x	⊢ 𝑋 = (var₁‘𝑅)
vieta.a	⊢ 𝐴 = (algSc‘𝑊)
vieta.p	⊢ ↑ = (._g‘(mulGrp‘𝑅))
vieta.h	⊢ 𝐻 = (♯‘𝐼)
vieta.i	⊢ (𝜑 → 𝐼 ∈ Fin)
vieta.r	⊢ (𝜑 → 𝑅 ∈ IDomn)
vieta.z	⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
vieta.f	⊢ 𝐹 = (𝑀 Σ_g (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
vieta.k	⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
vietalem.y	⊢ (𝜑 → 𝑌 ∈ 𝐼)
vietalem.j	⊢ 𝐽 = (𝐼 ∖ {𝑌})
vietalem.2	⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑_m 𝐽)∀𝑘 ∈ (0...(♯‘𝐽))((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)))
vietalem.3	⊢ (𝜑 → ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (♯‘𝐽))

**Assertion**
Ref	Expression
vietalem	⊢ (𝜑 → ((coe₁‘𝐹)‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))

Distinct variable groups: − ,𝑘,𝑛,𝑧 1 ,𝑘,𝑧 ↑ ,𝑘,𝑧 · ,𝑘,𝑧 𝐴,𝑘,𝑛,𝑧 𝐵,𝑘,𝑧 𝑘,𝐸,𝑧 𝑘,𝐻,𝑧 𝑘,𝐼,𝑛,𝑧 𝑘,𝐾 𝑘,𝑀,𝑧 𝑘,𝑁,𝑧 𝑄,𝑘,𝑧 𝑅,𝑘,𝑧 𝑘,𝑋,𝑛,𝑧 𝑘,𝑍,𝑛,𝑧 𝜑,𝑘,𝑧 1 ,𝑛 ↑ ,𝑛 · ,𝑛 𝑛,𝐸 𝑛,𝐻 𝑘,𝐽,𝑛,𝑧 𝑛,𝑀 𝑛,𝑁 𝑄,𝑛 𝑅,𝑛 𝑘,𝑊,𝑛 𝑘,𝑌,𝑛 𝜑,𝑛 Allowed substitution hints: 𝐵(𝑛) 𝐹(𝑧,𝑘,𝑛) 𝐾(𝑧,𝑛) 𝑊(𝑧) 𝑌(𝑧)

Proof of Theorem vietalem Dummy variables 𝑖 𝑙 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vieta.f	. . . . . . 7 ⊢ 𝐹 = (𝑀 Σ_g (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
2	1	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑀 Σ_g (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
3		vietalem.j	. . . . . . . . . 10 ⊢ 𝐽 = (𝐼 ∖ {𝑌})
4	3	uneq1i 4104	. . . . . . . . 9 ⊢ (𝐽 ∪ {𝑌}) = ((𝐼 ∖ {𝑌}) ∪ {𝑌})
5		vietalem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ 𝐼)
6	5	snssd 4730	. . . . . . . . . 10 ⊢ (𝜑 → {𝑌} ⊆ 𝐼)
7		undifr 4423	. . . . . . . . . 10 ⊢ ({𝑌} ⊆ 𝐼 ↔ ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
8	6, 7	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
9	4, 8	eqtr2id 2784	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (𝐽 ∪ {𝑌}))
10	9	mpteq1d 5175	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))) = (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
11	10	oveq2d 7383	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
12		vieta.m	. . . . . . . 8 ⊢ 𝑀 = (mulGrp‘𝑊)
13		eqid 2736	. . . . . . . 8 ⊢ (Base‘𝑊) = (Base‘𝑊)
14	12, 13	mgpbas 20126	. . . . . . 7 ⊢ (Base‘𝑊) = (Base‘𝑀)
15		eqid 2736	. . . . . . . 8 ⊢ (._r‘𝑊) = (._r‘𝑊)
16	12, 15	mgpplusg 20125	. . . . . . 7 ⊢ (._r‘𝑊) = (+_g‘𝑀)
17		vieta.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ IDomn)
18	17	idomcringd 20704	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CRing)
19		vieta.w	. . . . . . . . 9 ⊢ 𝑊 = (Poly₁‘𝑅)
20	19	ply1crng 22162	. . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑊 ∈ CRing)
21	12	crngmgp 20222	. . . . . . . 8 ⊢ (𝑊 ∈ CRing → 𝑀 ∈ CMnd)
22	18, 20, 21	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ CMnd)
23		vieta.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
24		diffi 9109	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (𝐼 ∖ {𝑌}) ∈ Fin)
25	23, 24	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐼 ∖ {𝑌}) ∈ Fin)
26	3, 25	eqeltrid 2840	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Fin)
27		vieta.3	. . . . . . . 8 ⊢ − = (-_g‘𝑊)
28	18, 20	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ CRing)
29	28	crngringd 20227	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Ring)
30	29	ringgrpd 20223	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Grp)
31	30	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑊 ∈ Grp)
32	17	idomringd 20705	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Ring)
33		vieta.x	. . . . . . . . . . 11 ⊢ 𝑋 = (var₁‘𝑅)
34	33, 19, 13	vr1cl 22181	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑊))
35	32, 34	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑊))
36	35	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑋 ∈ (Base‘𝑊))
37		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
38		eqid 2736	. . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
39		eqid 2736	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
40	19	ply1assa 22163	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → 𝑊 ∈ AssAlg)
41	18, 40	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ AssAlg)
42	41	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑊 ∈ AssAlg)
43		vieta.z	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
44	43	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑍:𝐼⟶𝐵)
45		difss 4076	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∖ {𝑌}) ⊆ 𝐼
46	3, 45	eqsstri 3968	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝐼
47	46	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
48	47	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑛 ∈ 𝐼)
49	44, 48	ffvelcdmd 7037	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑍‘𝑛) ∈ 𝐵)
50		vieta.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑅)
51	19	ply1sca 22216	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑊))
52	18, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑊))
53	52	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑊)))
54	50, 53	eqtrid 2783	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊)))
55	54	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝐵 = (Base‘(Scalar‘𝑊)))
56	49, 55	eleqtrd 2838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑍‘𝑛) ∈ (Base‘(Scalar‘𝑊)))
57	37, 38, 39, 42, 56	asclelbas 21863	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝐴‘(𝑍‘𝑛)) ∈ (Base‘𝑊))
58	13, 27, 31, 36, 57	grpsubcld 33101	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑋 − (𝐴‘(𝑍‘𝑛))) ∈ (Base‘𝑊))
59		neldifsnd 4738	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝐼 ∖ {𝑌}))
60	3	eleq2i 2828	. . . . . . . 8 ⊢ (𝑌 ∈ 𝐽 ↔ 𝑌 ∈ (𝐼 ∖ {𝑌}))
61	59, 60	sylnibr 329	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐽)
62	54, 43	feq3dd 6655	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍:𝐼⟶(Base‘(Scalar‘𝑊)))
63	62, 5	ffvelcdmd 7037	. . . . . . . . 9 ⊢ (𝜑 → (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)))
64	37, 38, 39, 41, 63	asclelbas 21863	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(𝑍‘𝑌)) ∈ (Base‘𝑊))
65	13, 27, 30, 35, 64	grpsubcld 33101	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝐴‘(𝑍‘𝑌))) ∈ (Base‘𝑊))
66		2fveq3 6845	. . . . . . . 8 ⊢ (𝑛 = 𝑌 → (𝐴‘(𝑍‘𝑛)) = (𝐴‘(𝑍‘𝑌)))
67	66	oveq2d 7383	. . . . . . 7 ⊢ (𝑛 = 𝑌 → (𝑋 − (𝐴‘(𝑍‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑌))))
68	14, 16, 22, 26, 58, 5, 61, 65, 67	gsumunsn 19935	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
69	2, 11, 68	3eqtrd 2775	. . . . 5 ⊢ (𝜑 → 𝐹 = ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
70		eqid 2736	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
71		eqid 2736	. . . . . . . . 9 ⊢ (._g‘𝑀) = (._g‘𝑀)
72		eqid 2736	. . . . . . . . 9 ⊢ (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
73		eqid 2736	. . . . . . . . 9 ⊢ ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
74		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑛 ∈ 𝐽)
75	74	fvresd 6860	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → ((𝑍 ↾ 𝐽)‘𝑛) = (𝑍‘𝑛))
76	75	fveq2d 6844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)) = (𝐴‘(𝑍‘𝑛)))
77	76	oveq2d 7383	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
78	77	mpteq2dva 5178	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))) = (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
79	78	oveq2d 7383	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
80	58	ralrimiva 3129	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝐽 (𝑋 − (𝐴‘(𝑍‘𝑛))) ∈ (Base‘𝑊))
81	14, 22, 26, 80	gsummptcl 19942	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) ∈ (Base‘𝑊))
82	79, 81	eqeltrd 2836	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘𝑊))
83	19, 33, 13, 70, 12, 71, 72, 73, 32, 82	ply1coedeg 33649	. . . . . . . 8 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
84		vietalem.3	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (♯‘𝐽))
85	84	oveq2d 7383	. . . . . . . . . 10 ⊢ (𝜑 → (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) = (0...(♯‘𝐽)))
86	85	mpteq1d 5175	. . . . . . . . 9 ⊢ (𝜑 → (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))
87	86	oveq2d 7383	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
88	83, 79, 87	3eqtr3d 2779	. . . . . . 7 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
89	29	ringcmnd 20265	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ CMnd)
90		hashcl 14318	. . . . . . . . 9 ⊢ (𝐽 ∈ Fin → (♯‘𝐽) ∈ ℕ₀)
91	26, 90	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐽) ∈ ℕ₀)
92	19	ply1lmod 22215	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑊 ∈ LMod)
93	32, 92	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ LMod)
94	93	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑊 ∈ LMod)
95	82	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘𝑊))
96	52	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Poly₁‘𝑅) = (Poly₁‘(Scalar‘𝑊)))
97	19, 96	eqtrid 2783	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 = (Poly₁‘(Scalar‘𝑊)))
98	97	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑊) = (Base‘(Poly₁‘(Scalar‘𝑊))))
99	98	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (Base‘𝑊) = (Base‘(Poly₁‘(Scalar‘𝑊))))
100	95, 99	eleqtrd 2838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘(Poly₁‘(Scalar‘𝑊))))
101		fz0ssnn0 13576	. . . . . . . . . . 11 ⊢ (0...(♯‘𝐽)) ⊆ ℕ₀
102		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ (0...(♯‘𝐽)))
103	101, 102	sselid 3919	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ ℕ₀)
104		eqid 2736	. . . . . . . . . . 11 ⊢ (Base‘(Poly₁‘(Scalar‘𝑊))) = (Base‘(Poly₁‘(Scalar‘𝑊)))
105		eqid 2736	. . . . . . . . . . 11 ⊢ (Poly₁‘(Scalar‘𝑊)) = (Poly₁‘(Scalar‘𝑊))
106	72, 104, 105, 39	coe1fvalcl 22176	. . . . . . . . . 10 ⊢ (((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘(Poly₁‘(Scalar‘𝑊))) ∧ 𝑙 ∈ ℕ₀) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) ∈ (Base‘(Scalar‘𝑊)))
107	100, 103, 106	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) ∈ (Base‘(Scalar‘𝑊)))
108	22	cmnmndd 19779	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ Mnd)
109	108	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
110	32	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
111	110, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
112	14, 71, 109, 103, 111	mulgnn0cld 19071	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑙(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
113	13, 38, 70, 39, 94, 107, 112	lmodvscld 20874	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
114		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑙 = ((♯‘𝐽) − 𝑘))
115	114	fveq2d 6844	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) = ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)))
116		oveq1 7374	. . . . . . . . . 10 ⊢ (𝑙 = ((♯‘𝐽) − 𝑘) → (𝑙(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
117	116	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (𝑙(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
118	115, 117	oveq12d 7385	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) = (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
119	13, 89, 91, 113, 118	gsummptrev 33117	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
120		fveq1 6839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑧‘𝑛) = ((𝑍 ↾ 𝐽)‘𝑛))
121	120	fveq2d 6844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝐴‘(𝑧‘𝑛)) = (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))
122	121	oveq2d 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))
123	122	mpteq2dv 5179	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))
124	123	oveq2d 7383	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
125	124	fveq2d 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))))
126	125	fveq1d 6842	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)))
127		fveq2 6840	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
128	127	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
129	126, 128	eqeq12d 2752	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
130	129	ralbidv 3160	. . . . . . . . . . . . 13 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (∀𝑘 ∈ (0...(♯‘𝐽))((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ∀𝑘 ∈ (0...(♯‘𝐽))((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
131		vietalem.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 ↑_m 𝐽)∀𝑘 ∈ (0...(♯‘𝐽))((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)))
132	50	fvexi 6854	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
133	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ V)
134	43, 47	fssresd 6707	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 ↾ 𝐽):𝐽⟶𝐵)
135	133, 26, 134	elmapdd 8788	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
136	130, 131, 135	rspcdva 3565	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐽))((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
137	136	r19.21bi 3229	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
138	137	oveq1d 7382	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
139	138	mpteq2dva 5178	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))) = (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
140	139	oveq2d 7383	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
141		vieta.t	. . . . . . . . . . 11 ⊢ · = (._r‘𝑅)
142		eqid 2736	. . . . . . . . . . . . 13 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
143	142, 50	mgpbas 20126	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
144		vieta.p	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘(mulGrp‘𝑅))
145	142	ringmgp 20220	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
146	110, 145	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
147		fznn0sub2 13589	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑙) ∈ (0...(♯‘𝐽)))
148	147	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑙) ∈ (0...(♯‘𝐽)))
149	101, 148	sselid 3919	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑙) ∈ ℕ₀)
150		vieta.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (inv_g‘𝑅)
151	32	ringgrpd 20223	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Grp)
152		vieta.1	. . . . . . . . . . . . . . 15 ⊢ 1 = (1_r‘𝑅)
153	50, 152, 32	ringidcld 20247	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ 𝐵)
154	50, 150, 151, 153	grpinvcld 18964	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
155	154	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
156	143, 144, 146, 149, 155	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) ∈ 𝐵)
157		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝐽 eval 𝑅) = (𝐽 eval 𝑅)
158		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝐽 mPoly 𝑅) = (𝐽 mPoly 𝑅)
159		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘(𝐽 mPoly 𝑅)) = (Base‘(𝐽 mPoly 𝑅))
160	26	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
161	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
162		eqid 2736	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}
163	162, 160, 110, 149, 159	esplympl 33711	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)) ∈ (Base‘(𝐽 mPoly 𝑅)))
164	135	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
165	157, 158, 159, 50, 160, 161, 163, 164	evlcl 22080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
166	50, 141, 110, 156, 165	ringcld 20241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
167	19, 13, 50, 70, 110, 166, 112	ply1vscl 22349	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
168	91	nn0cnd 12500	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘𝐽) ∈ ℂ)
169	168	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (♯‘𝐽) ∈ ℂ)
170		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ (0...(♯‘𝐽)))
171	101, 170	sselid 3919	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ ℕ₀)
172	171	nn0cnd 12500	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ ℂ)
173	169, 172	subcld 11505	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑘) ∈ ℂ)
174	114, 173	eqeltrd 2836	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑙 ∈ ℂ)
175	169, 174	subcld 11505	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑙) ∈ ℂ)
176	169, 174	nncand 11510	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = 𝑙)
177	176, 114	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = ((♯‘𝐽) − 𝑘))
178	169, 175, 172, 177	subcand 11546	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑙) = 𝑘)
179	178	oveq1d 7382	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
180	178	fveq2d 6844	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)) = ((𝐽eSymPoly𝑅)‘𝑘))
181	180	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙))) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)))
182	181	fveq1d 6842	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
183	179, 182	oveq12d 7385	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
184	183, 117	oveq12d 7385	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
185	13, 89, 91, 167, 184	gsummptrev 33117	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
186	140, 185	eqtr4d 2774	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
187	88, 119, 186	3eqtrd 2775	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
188	187	oveq1d 7382	. . . . 5 ⊢ (𝜑 → ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
189		eqid 2736	. . . . . . 7 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
190	32	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
191	190, 145	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
192		elfznn0 13574	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...(♯‘𝐽)) → 𝑖 ∈ ℕ₀)
193	192	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑖 ∈ ℕ₀)
194	154	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
195	143, 144, 191, 193, 194	mulgnn0cld 19071	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑖 ↑ (𝑁‘ 1 )) ∈ 𝐵)
196	26	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
197	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
198	162, 196, 190, 193, 159	esplympl 33711	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑖) ∈ (Base‘(𝐽 mPoly 𝑅)))
199	135	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
200	157, 158, 159, 50, 196, 197, 198, 199	evlcl 22080	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
201	50, 141, 190, 195, 200	ringcld 20241	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
202	108	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
203		fznn0sub2 13589	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑖) ∈ (0...(♯‘𝐽)))
204	203	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑖) ∈ (0...(♯‘𝐽)))
205	101, 204	sselid 3919	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑖) ∈ ℕ₀)
206	35	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
207	14, 71, 202, 205, 206	mulgnn0cld 19071	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
208	19, 13, 50, 70, 190, 201, 207	ply1vscl 22349	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
209		oveq1 7374	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
210		2fveq3 6845	. . . . . . . . . 10 ⊢ (𝑖 = 0 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)))
211	210	fveq1d 6842	. . . . . . . . 9 ⊢ (𝑖 = 0 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))
212	209, 211	oveq12d 7385	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))))
213		oveq2 7375	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − 0))
214	213	oveq1d 7382	. . . . . . . 8 ⊢ (𝑖 = 0 → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − 0)(._g‘𝑀)𝑋))
215	212, 214	oveq12d 7385	. . . . . . 7 ⊢ (𝑖 = 0 → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋)))
216		oveq1 7374	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → (𝑖 ↑ (𝑁‘ 1 )) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
217		2fveq3 6845	. . . . . . . . . 10 ⊢ (𝑖 = (♯‘𝐽) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽))))
218	217	fveq1d 6842	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))
219	216, 218	oveq12d 7385	. . . . . . . 8 ⊢ (𝑖 = (♯‘𝐽) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))
220		oveq2 7375	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − (♯‘𝐽)))
221	220	oveq1d 7382	. . . . . . . 8 ⊢ (𝑖 = (♯‘𝐽) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))
222	219, 221	oveq12d 7385	. . . . . . 7 ⊢ (𝑖 = (♯‘𝐽) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)))
223		oveq1 7374	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
224		2fveq3 6845	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)))
225	224	fveq1d 6842	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
226	223, 225	oveq12d 7385	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
227		oveq2 7375	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − 𝑘))
228	227	oveq1d 7382	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
229	226, 228	oveq12d 7385	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
230		oveq1 7374	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ↑ (𝑁‘ 1 )) = ((𝑘 + 1) ↑ (𝑁‘ 1 )))
231		2fveq3 6845	. . . . . . . . . 10 ⊢ (𝑖 = (𝑘 + 1) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1))))
232	231	fveq1d 6842	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))
233	230, 232	oveq12d 7385	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
234		oveq2 7375	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − (𝑘 + 1)))
235	234	oveq1d 7382	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))
236	233, 235	oveq12d 7385	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)))
237		eqid 2736	. . . . . . . . 9 ⊢ (inv_g‘𝑊) = (inv_g‘𝑊)
238	32, 145	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
239		0nn0 12452	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ₀
240	239	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ₀)
241	143, 144, 238, 240, 154	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) ∈ 𝐵)
242	152, 153	eqeltrrid 2841	. . . . . . . . . . 11 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝐵)
243	50, 141, 32, 241, 242	ringcld 20241	. . . . . . . . . 10 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)) ∈ 𝐵)
244		vieta.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (♯‘𝐼)
245		hashcl 14318	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ₀)
246	23, 245	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐼) ∈ ℕ₀)
247	244, 246	eqeltrid 2840	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℕ₀)
248	14, 71, 108, 247, 35	mulgnn0cld 19071	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
249	19, 13, 50, 70, 32, 243, 248	ply1vscl 22349	. . . . . . . . 9 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
250	143, 144, 238, 247, 154	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) ∈ 𝐵)
251		vieta.q	. . . . . . . . . . . 12 ⊢ 𝑄 = (𝐼 eval 𝑅)
252		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝐼 mPoly 𝑅) = (𝐼 mPoly 𝑅)
253		eqid 2736	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPoly 𝑅)) = (Base‘(𝐼 mPoly 𝑅))
254		vieta.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
255	254	fveq1i 6841	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐻) = ((𝐼eSymPoly𝑅)‘𝐻)
256		eqid 2736	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
257	256, 23, 32, 247, 253	esplympl 33711	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐻) ∈ (Base‘(𝐼 mPoly 𝑅)))
258	255, 257	eqeltrid 2840	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝐻) ∈ (Base‘(𝐼 mPoly 𝑅)))
259	133, 23, 43	elmapdd 8788	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑_m 𝐼))
260	251, 252, 253, 50, 23, 18, 258, 259	evlcl 22080	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘(𝐸‘𝐻))‘𝑍) ∈ 𝐵)
261	50, 141, 32, 250, 260	ringcld 20241	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) ∈ 𝐵)
262	14, 71, 108, 240, 35	mulgnn0cld 19071	. . . . . . . . . 10 ⊢ (𝜑 → (0(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
263	19, 13, 50, 70, 32, 261, 262	ply1vscl 22349	. . . . . . . . 9 ⊢ (𝜑 → (((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
264	13, 189, 27, 237, 30, 249, 263	grpsubinv 18988	. . . . . . . 8 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) − ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))) = ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))))
265	162, 26, 32, 240, 159	esplympl 33711	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘0) ∈ (Base‘(𝐽 mPoly 𝑅)))
266	157, 158, 159, 50, 26, 18, 265, 135	evlcl 22080	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
267	50, 141, 32, 241, 266	ringcld 20241	. . . . . . . . . . . 12 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
268	267, 54	eleqtrd 2838	. . . . . . . . . . 11 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
269	168	subid1d 11494	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − 0) = (♯‘𝐽))
270	269, 91	eqeltrd 2836	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐽) − 0) ∈ ℕ₀)
271	14, 71, 108, 270, 35	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝐽) − 0)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
272	13, 38, 39, 70, 15, 41, 268, 271, 35	assaassd 33615	. . . . . . . . . 10 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) = (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
273		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘(𝐽 mPoly 𝑅)) = (1_r‘(𝐽 mPoly 𝑅))
274	26, 32, 273	esplyfval0 33708	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘0) = (1_r‘(𝐽 mPoly 𝑅)))
275	274	fveq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)) = ((𝐽 eval 𝑅)‘(1_r‘(𝐽 mPoly 𝑅))))
276		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (algSc‘(𝐽 mPoly 𝑅)) = (algSc‘(𝐽 mPoly 𝑅))
277		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
278	158, 276, 277, 273, 26, 32	mplascl1 22004	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)) = (1_r‘(𝐽 mPoly 𝑅)))
279	278	fveq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅))) = ((𝐽 eval 𝑅)‘(1_r‘(𝐽 mPoly 𝑅))))
280	275, 279	eqtr4d 2774	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)) = ((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅))))
281	280	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)))‘(𝑍 ↾ 𝐽)))
282	157, 158, 50, 276, 26, 18, 242, 134	evlscaval 33684	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)))‘(𝑍 ↾ 𝐽)) = (1_r‘𝑅))
283	281, 282	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) = (1_r‘𝑅))
284	283	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) = ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)))
285	14, 71, 16	mulgnn0p1 19061	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ Mnd ∧ (♯‘𝐽) ∈ ℕ₀ ∧ 𝑋 ∈ (Base‘𝑊)) → (((♯‘𝐽) + 1)(._g‘𝑀)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
286	108, 91, 35, 285	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) + 1)(._g‘𝑀)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
287		hashdifsn 14376	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼) → (♯‘(𝐼 ∖ {𝑌})) = ((♯‘𝐼) − 1))
288	23, 5, 287	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐼 ∖ {𝑌})) = ((♯‘𝐼) − 1))
289	3	fveq2i 6843	. . . . . . . . . . . . . . . 16 ⊢ (♯‘𝐽) = (♯‘(𝐼 ∖ {𝑌}))
290	244	oveq1i 7377	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 − 1) = ((♯‘𝐼) − 1)
291	288, 289, 290	3eqtr4g 2796	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐽) = (𝐻 − 1))
292	291	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((♯‘𝐽) + 1) = ((𝐻 − 1) + 1))
293	247	nn0cnd 12500	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ ℂ)
294		1cnd 11139	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
295	293, 294	npcand 11509	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐻 − 1) + 1) = 𝐻)
296	292, 295	eqtr2d 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 = ((♯‘𝐽) + 1))
297	296	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻(._g‘𝑀)𝑋) = (((♯‘𝐽) + 1)(._g‘𝑀)𝑋))
298	269	oveq1d 7382	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐽) − 0)(._g‘𝑀)𝑋) = ((♯‘𝐽)(._g‘𝑀)𝑋))
299	298	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
300	286, 297, 299	3eqtr4rd 2782	. . . . . . . . . . 11 ⊢ (𝜑 → ((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋) = (𝐻(._g‘𝑀)𝑋))
301	284, 300	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))
302	272, 301	eqtr2d 2772	. . . . . . . . 9 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) = ((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋))
303	52	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝑅) = (._r‘(Scalar‘𝑊)))
304	141, 303	eqtrid 2783	. . . . . . . . . . . . 13 ⊢ (𝜑 → · = (._r‘(Scalar‘𝑊)))
305	304	oveqd 7384	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
306	305	oveq1d 7382	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)))
307	43, 5	ffvelcdmd 7037	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑌) ∈ 𝐵)
308	143, 144, 238, 91, 154	mulgnn0cld 19071	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝐽) ↑ (𝑁‘ 1 )) ∈ 𝐵)
309	162, 26, 32, 91, 159	esplympl 33711	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘(♯‘𝐽)) ∈ (Base‘(𝐽 mPoly 𝑅)))
310	157, 158, 159, 50, 26, 18, 309, 135	evlcl 22080	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
311	50, 141, 18, 307, 308, 310	crng12d 20239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
312	296	oveq1d 7382	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) = (((♯‘𝐽) + 1) ↑ (𝑁‘ 1 )))
313	152, 150, 144, 32, 91	ringm1expp1 33295	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((♯‘𝐽) + 1) ↑ (𝑁‘ 1 )) = (𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 ))))
314	312, 313	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) = (𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 ))))
315	314	fveq2d 6844	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) = (𝑁‘(𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 )))))
316	50, 150, 151, 308	grpinvinvd 33100	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁‘(𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 )))) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
317	315, 316	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
318		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
319		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝐽eSymPoly𝑅) = (𝐽eSymPoly𝑅)
320		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (♯‘𝐽) = (♯‘𝐽)
321	50, 318, 141, 251, 157, 254, 319, 244, 320, 3, 23, 18, 5, 43	esplyfvn 33721	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘(𝐸‘𝐻))‘𝑍) = ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))
322	317, 321	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
323	311, 322	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
324	50, 141, 150, 32, 250, 260	ringmneg1 20285	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) = (𝑁‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
325	52	fveq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (inv_g‘𝑅) = (inv_g‘(Scalar‘𝑊)))
326	150, 325	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 = (inv_g‘(Scalar‘𝑊)))
327	326	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))) = ((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
328	323, 324, 327	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
329	168	subidd 11493	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − (♯‘𝐽)) = 0)
330	329	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋) = (0(._g‘𝑀)𝑋))
331	328, 330	oveq12d 7385	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
332	50, 141, 32, 308, 310	ringcld 20241	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
333	332, 54	eleqtrd 2838	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
334	329, 240	eqeltrd 2836	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − (♯‘𝐽)) ∈ ℕ₀)
335	14, 71, 108, 334, 35	mulgnn0cld 19071	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
336		eqid 2736	. . . . . . . . . . . . 13 ⊢ (._r‘(Scalar‘𝑊)) = (._r‘(Scalar‘𝑊))
337	13, 38, 70, 39, 336	lmodvsass 20882	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LMod ∧ ((𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)) ∧ (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))) → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
338	93, 63, 333, 335, 337	syl13anc 1375	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
339	306, 331, 338	3eqtr3d 2779	. . . . . . . . . 10 ⊢ (𝜑 → (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
340		eqid 2736	. . . . . . . . . . 11 ⊢ (inv_g‘(Scalar‘𝑊)) = (inv_g‘(Scalar‘𝑊))
341	261, 54	eleqtrd 2838	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) ∈ (Base‘(Scalar‘𝑊)))
342	13, 38, 70, 237, 39, 340, 93, 262, 341	lmodvsneg 20901	. . . . . . . . . 10 ⊢ (𝜑 → ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
343	19, 13, 50, 70, 32, 332, 335	ply1vscl 22349	. . . . . . . . . . 11 ⊢ (𝜑 → ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
344	37, 38, 39, 13, 15, 70	asclmul2 21867	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ AssAlg ∧ (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) ∈ (Base‘𝑊)) → (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
345	41, 63, 343, 344	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
346	339, 342, 345	3eqtr4d 2781	. . . . . . . . 9 ⊢ (𝜑 → ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))))
347	302, 346	oveq12d 7385	. . . . . . . 8 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) − ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))) = (((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) − (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌)))))
348	264, 347	eqtr3d 2773	. . . . . . 7 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) − (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌)))))
349	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Ring)
350	349, 145	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
351		fzossfz 13633	. . . . . . . . . . . . . . . 16 ⊢ (0..^(♯‘𝐽)) ⊆ (0...(♯‘𝐽))
352		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ (0..^(♯‘𝐽)))
353	351, 352	sselid 3919	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ (0...(♯‘𝐽)))
354	101, 353	sselid 3919	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ ℕ₀)
355		peano2nn0 12477	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
356	354, 355	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ ℕ₀)
357	154	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
358	143, 144, 350, 356, 357	mulgnn0cld 19071	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 + 1) ↑ (𝑁‘ 1 )) ∈ 𝐵)
359	26	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐽 ∈ Fin)
360	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ CRing)
361	162, 359, 349, 356, 159	esplympl 33711	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘(𝑘 + 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
362	135	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
363	157, 158, 159, 50, 359, 360, 361, 362	evlcl 22080	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
364	43	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑍:𝐼⟶𝐵)
365	5	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑌 ∈ 𝐼)
366	364, 365	ffvelcdmd 7037	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍‘𝑌) ∈ 𝐵)
367	162, 359, 349, 354, 159	esplympl 33711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐽 mPoly 𝑅)))
368	157, 158, 159, 50, 359, 360, 367, 362	evlcl 22080	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
369	50, 141, 349, 366, 368	ringcld 20241	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
370	50, 318, 141, 349, 358, 363, 369	ringdid 20244	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
371	23	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐼 ∈ Fin)
372	254	fveq1i 6841	. . . . . . . . . . . . . 14 ⊢ (𝐸‘(𝑘 + 1)) = ((𝐼eSymPoly𝑅)‘(𝑘 + 1))
373	141, 371, 360, 365, 3, 319, 353, 162, 372, 50, 251, 157, 318, 364	esplyindfv 33720	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍) = (((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
374	32	ringabld 20264	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ Abel)
375	374	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Abel)
376	50, 318, 375, 369, 363	ablcomd 33106	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
377	373, 376	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
378	377	oveq2d 7383	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
379		eqid 2736	. . . . . . . . . . . 12 ⊢ (-_g‘𝑅) = (-_g‘𝑅)
380	151	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Grp)
381	50, 141, 349, 358, 363	ringcld 20241	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
382	50, 141, 349, 358, 369	ringcld 20241	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) ∈ 𝐵)
383	50, 318, 379, 150, 380, 381, 382	grpsubinv 18988	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘𝑅)(𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
384	370, 378, 383	3eqtr4d 2781	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘𝑅)(𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))))
385	52	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝜑 → (-_g‘𝑅) = (-_g‘(Scalar‘𝑊)))
386	385	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (-_g‘𝑅) = (-_g‘(Scalar‘𝑊)))
387		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
388	238	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (mulGrp‘𝑅) ∈ Mnd)
389		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
390	154	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑁‘ 1 ) ∈ 𝐵)
391	143, 144, 388, 389, 390	mulgnn0cld 19071	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
392	354, 391	syldan 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
393	50, 141, 349, 392, 368, 366	ringassd 20238	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌))))
394	152, 150, 144, 349, 354	ringm1expp1 33295	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 + 1) ↑ (𝑁‘ 1 )) = (𝑁‘(𝑘 ↑ (𝑁‘ 1 ))))
395	394	fveq2d 6844	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) = (𝑁‘(𝑁‘(𝑘 ↑ (𝑁‘ 1 )))))
396	50, 150, 380, 392	grpinvinvd 33100	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘(𝑁‘(𝑘 ↑ (𝑁‘ 1 )))) = (𝑘 ↑ (𝑁‘ 1 )))
397	395, 396	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) = (𝑘 ↑ (𝑁‘ 1 )))
398	50, 141, 360, 366, 368	crngcomd 20236	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌)))
399	397, 398	oveq12d 7385	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌))))
400	50, 141, 150, 349, 358, 369	ringmneg1 20285	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = (𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
401	393, 399, 400	3eqtr2rd 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)))
402	386, 387, 401	oveq123d 7388	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘𝑅)(𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))))
403	384, 402	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))))
404	403	oveq1d 7382	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
405		eqid 2736	. . . . . . . . 9 ⊢ (-_g‘(Scalar‘𝑊)) = (-_g‘(Scalar‘𝑊))
406	349, 92	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑊 ∈ LMod)
407	54	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐵 = (Base‘(Scalar‘𝑊)))
408	381, 407	eleqtrd 2838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
409	50, 141, 349, 392, 368	ringcld 20241	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
410	50, 141, 349, 409, 366	ringcld 20241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) ∈ 𝐵)
411	410, 407	eleqtrd 2838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) ∈ (Base‘(Scalar‘𝑊)))
412	108	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑀 ∈ Mnd)
413		fz0ssnn0 13576	. . . . . . . . . . 11 ⊢ (0...𝐻) ⊆ ℕ₀
414		fzossfz 13633	. . . . . . . . . . . 12 ⊢ (0..^𝐻) ⊆ (0...𝐻)
415		fzssp1 13521	. . . . . . . . . . . . . . . 16 ⊢ (1...(♯‘𝐽)) ⊆ (1...((♯‘𝐽) + 1))
416	296	oveq2d 7383	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝐻) = (1...((♯‘𝐽) + 1)))
417	415, 416	sseqtrrid 3965	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ (1...𝐻))
418	417	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (1...(♯‘𝐽)) ⊆ (1...𝐻))
419	359, 90	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) ∈ ℕ₀)
420		fz0add1fz1 13690	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐽) ∈ ℕ₀ ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...(♯‘𝐽)))
421	419, 352, 420	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...(♯‘𝐽)))
422	418, 421	sseldd 3922	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...𝐻))
423		ubmelfzo 13685	. . . . . . . . . . . . 13 ⊢ ((𝑘 + 1) ∈ (1...𝐻) → (𝐻 − (𝑘 + 1)) ∈ (0..^𝐻))
424	422, 423	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ (0..^𝐻))
425	414, 424	sselid 3919	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ (0...𝐻))
426	413, 425	sselid 3919	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ ℕ₀)
427	349, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
428	14, 71, 412, 426, 427	mulgnn0cld 19071	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
429	13, 70, 38, 39, 27, 405, 406, 408, 411, 428	lmodsubdir 20915	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) − ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))))
430	296	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐻 = ((♯‘𝐽) + 1))
431	430	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = (((♯‘𝐽) + 1) − (𝑘 + 1)))
432	168	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) ∈ ℂ)
433		1cnd 11139	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 1 ∈ ℂ)
434	356	nn0cnd 12500	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ ℂ)
435	432, 433, 434	addsubd 11526	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) + 1) − (𝑘 + 1)) = (((♯‘𝐽) − (𝑘 + 1)) + 1))
436	431, 435	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = (((♯‘𝐽) − (𝑘 + 1)) + 1))
437	436	oveq1d 7382	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋))
438		fzofzp1 13719	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^(♯‘𝐽)) → (𝑘 + 1) ∈ (0...(♯‘𝐽)))
439	438	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (0...(♯‘𝐽)))
440		fznn0sub2 13589	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 + 1) ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − (𝑘 + 1)) ∈ (0...(♯‘𝐽)))
441	439, 440	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − (𝑘 + 1)) ∈ (0...(♯‘𝐽)))
442	101, 441	sselid 3919	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − (𝑘 + 1)) ∈ ℕ₀)
443	14, 71, 16	mulgnn0p1 19061	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ Mnd ∧ ((♯‘𝐽) − (𝑘 + 1)) ∈ ℕ₀ ∧ 𝑋 ∈ (Base‘𝑊)) → ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
444	412, 442, 427, 443	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
445	437, 444	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
446	445	oveq2d 7383	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
447	360, 40	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑊 ∈ AssAlg)
448	14, 71, 412, 442, 427	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
449	13, 38, 39, 70, 15, 447, 408, 448, 427	assaassd 33615	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
450	446, 449	eqtr4d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋))
451	63	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)))
452	409, 407	eleqtrd 2838	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
453		fznn0sub2 13589	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
454	353, 453	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
455	101, 454	sselid 3919	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ ℕ₀)
456	14, 71, 412, 455, 427	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
457	13, 38, 70, 39, 336	lmodvsass 20882	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LMod ∧ ((𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)) ∧ (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))) → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
458	406, 451, 452, 456, 457	syl13anc 1375	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
459	50, 141, 360, 409, 366	crngcomd 20236	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
460	304	oveqd 7384	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
461	460	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
462	459, 461	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
463	291	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) = (𝐻 − 1))
464	463	oveq1d 7382	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) = ((𝐻 − 1) − 𝑘))
465	293	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐻 ∈ ℂ)
466	354	nn0cnd 12500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ ℂ)
467	465, 466, 433	sub32d 11537	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − 𝑘) − 1) = ((𝐻 − 1) − 𝑘))
468	465, 466, 433	subsub4d 11536	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − 𝑘) − 1) = (𝐻 − (𝑘 + 1)))
469	464, 467, 468	3eqtr2rd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = ((♯‘𝐽) − 𝑘))
470	469	oveq1d 7382	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
471	462, 470	oveq12d 7385	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
472	19, 13, 50, 70, 349, 409, 456	ply1vscl 22349	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
473	37, 38, 39, 13, 15, 70	asclmul2 21867	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ AssAlg ∧ (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊)) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
474	447, 451, 472, 473	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
475	458, 471, 474	3eqtr4d 2781	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))))
476	450, 475	oveq12d 7385	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) − ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))) = ((((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) − ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌)))))
477	404, 429, 476	3eqtrd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = ((((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) − ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌)))))
478	13, 189, 27, 15, 29, 35, 64, 91, 208, 215, 222, 229, 236, 348, 477	gsummulsubdishift2s 33132	. . . . . 6 ⊢ (𝜑 → ((𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = ((𝑊 Σ_g (𝑘 ∈ (0..^(♯‘𝐽)) ↦ ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))))
479	32	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
480	479, 145	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
481	101	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐽)) ⊆ ℕ₀)
482	481	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑘 ∈ ℕ₀)
483	154	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
484	143, 144, 480, 482, 483	mulgnn0cld 19071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
485	26	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
486	18	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
487	162, 485, 479, 482, 159	esplympl 33711	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐽 mPoly 𝑅)))
488	135	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
489	157, 158, 159, 50, 485, 486, 487, 488	evlcl 22080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
490	50, 141, 479, 484, 489	ringcld 20241	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
491	108	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
492	453	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
493	101, 492	sselid 3919	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ ℕ₀)
494	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
495	14, 71, 491, 493, 494	mulgnn0cld 19071	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
496	19, 13, 50, 70, 479, 490, 495	ply1vscl 22349	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
497		oveq1 7374	. . . . . . . . . . 11 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → (𝑘 ↑ (𝑁‘ 1 )) = (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )))
498		2fveq3 6845	. . . . . . . . . . . 12 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙))))
499	498	fveq1d 6842	. . . . . . . . . . 11 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))
500	497, 499	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))))
501	500	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))))
502		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑘 = ((♯‘𝐽) − 𝑙))
503	502	oveq2d 7383	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − 𝑘) = ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)))
504	168	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (♯‘𝐽) ∈ ℂ)
505	103	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑙 ∈ ℕ₀)
506	505	nn0cnd 12500	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑙 ∈ ℂ)
507	504, 506	nncand 11510	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = 𝑙)
508	503, 507	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − 𝑘) = 𝑙)
509	508	oveq1d 7382	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) = (𝑙(._g‘𝑀)𝑋))
510	501, 509	oveq12d 7385	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))
511	13, 89, 91, 496, 510	gsummptrev 33117	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
512	511	oveq1d 7382	. . . . . 6 ⊢ (𝜑 → ((𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
513	32	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑅 ∈ Ring)
514	513, 145	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
515		fz1ssfz0 13577	. . . . . . . . . . . . . . 15 ⊢ (1...(♯‘𝐽)) ⊆ (0...(♯‘𝐽))
516	515, 101	sstri 3931	. . . . . . . . . . . . . 14 ⊢ (1...(♯‘𝐽)) ⊆ ℕ₀
517	516	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ ℕ₀)
518	517	sselda 3921	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑙 ∈ ℕ₀)
519	154	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
520	143, 144, 514, 518, 519	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
521	23	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝐼 ∈ Fin)
522	18	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑅 ∈ CRing)
523	254	fveq1i 6841	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝑙) = ((𝐼eSymPoly𝑅)‘𝑙)
524	256, 521, 513, 518, 253	esplympl 33711	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
525	523, 524	eqeltrid 2840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
526	259	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
527	251, 252, 253, 50, 521, 522, 525, 526	evlcl 22080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
528	50, 141, 513, 520, 527	ringcld 20241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
529	108	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑀 ∈ Mnd)
530		fzssp1 13521	. . . . . . . . . . . . . . . 16 ⊢ (0...(♯‘𝐽)) ⊆ (0...((♯‘𝐽) + 1))
531	296	oveq2d 7383	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0...𝐻) = (0...((♯‘𝐽) + 1)))
532	530, 531	sseqtrrid 3965	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0...(♯‘𝐽)) ⊆ (0...𝐻))
533	515, 532	sstrid 3933	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ (0...𝐻))
534	533	sselda 3921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑙 ∈ (0...𝐻))
535		fznn0sub2 13589	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ (0...𝐻) → (𝐻 − 𝑙) ∈ (0...𝐻))
536	534, 535	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ (0...𝐻))
537	413, 536	sselid 3919	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ ℕ₀)
538	513, 34	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
539	14, 71, 529, 537, 538	mulgnn0cld 19071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
540	19, 13, 50, 70, 513, 528, 539	ply1vscl 22349	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
541		oveq1 7374	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → (𝑙 ↑ (𝑁‘ 1 )) = ((𝑘 + 1) ↑ (𝑁‘ 1 )))
542		2fveq3 6845	. . . . . . . . . . . . 13 ⊢ (𝑙 = (𝑘 + 1) → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘(𝑘 + 1))))
543	542	fveq1d 6842	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))
544	541, 543	oveq12d 7385	. . . . . . . . . . 11 ⊢ (𝑙 = (𝑘 + 1) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)))
545		oveq2 7375	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → (𝐻 − 𝑙) = (𝐻 − (𝑘 + 1)))
546	545	oveq1d 7382	. . . . . . . . . . 11 ⊢ (𝑙 = (𝑘 + 1) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))
547	544, 546	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝑙 = (𝑘 + 1) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
548	547	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) ∧ 𝑙 = (𝑘 + 1)) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
549	13, 89, 91, 540, 548	gsummptp1 33118	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0..^(♯‘𝐽)) ↦ ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
550	549	oveq1d 7382	. . . . . . 7 ⊢ (𝜑 → ((𝑊 Σ_g (𝑘 ∈ (0..^(♯‘𝐽)) ↦ ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))))
551		oveq1 7374	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
552		2fveq3 6845	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝑙)))
553	552	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝑙))‘𝑍))
554	551, 553	oveq12d 7385	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)))
555		oveq2 7375	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → (𝐻 − 𝑘) = (𝐻 − 𝑙))
556	555	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) = ((𝐻 − 𝑙)(._g‘𝑀)𝑋))
557	554, 556	oveq12d 7385	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) = (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
558	557	cbvmptv 5189	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
559	558	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
560	559	oveq2d 7383	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
561		nn0uz 12826	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
562	247, 561	eleqtrdi 2846	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ (ℤ_≥‘0))
563	32	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑅 ∈ Ring)
564	563, 145	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (mulGrp‘𝑅) ∈ Mnd)
565	413	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝐻) ⊆ ℕ₀)
566	565	sselda 3921	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑙 ∈ ℕ₀)
567	154	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝑁‘ 1 ) ∈ 𝐵)
568	143, 144, 564, 566, 567	mulgnn0cld 19071	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
569	23	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝐼 ∈ Fin)
570	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑅 ∈ CRing)
571	256, 569, 563, 566, 253	esplympl 33711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
572	523, 571	eqeltrid 2840	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
573	259	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
574	251, 252, 253, 50, 569, 570, 572, 573	evlcl 22080	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
575	50, 141, 563, 568, 574	ringcld 20241	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
576	108	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑀 ∈ Mnd)
577		fznn0sub 13510	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ (0...𝐻) → (𝐻 − 𝑙) ∈ ℕ₀)
578	577	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐻 − 𝑙) ∈ ℕ₀)
579	563, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑋 ∈ (Base‘𝑊))
580	14, 71, 576, 578, 579	mulgnn0cld 19071	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
581	19, 13, 50, 70, 563, 575, 580	ply1vscl 22349	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
582		oveq1 7374	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → (𝑙 ↑ (𝑁‘ 1 )) = (𝐻 ↑ (𝑁‘ 1 )))
583		2fveq3 6845	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝐻 → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘𝐻)))
584	583	fveq1d 6842	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘𝐻))‘𝑍))
585	582, 584	oveq12d 7385	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐻 → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
586	585	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
587		oveq2 7375	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → (𝐻 − 𝑙) = (𝐻 − 𝐻))
588	293	subidd 11493	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻 − 𝐻) = 0)
589	587, 588	sylan9eqr 2793	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → (𝐻 − 𝑙) = 0)
590	589	oveq1d 7382	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = (0(._g‘𝑀)𝑋))
591	586, 590	oveq12d 7385	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = (((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
592	13, 189, 89, 562, 581, 591	gsummptfzsplitra 33119	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))))
593	91	nn0zd 12549	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐽) ∈ ℤ)
594		fzval3 13689	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐽) ∈ ℤ → (0...(♯‘𝐽)) = (0..^((♯‘𝐽) + 1)))
595	593, 594	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...(♯‘𝐽)) = (0..^((♯‘𝐽) + 1)))
596	296	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝐻) = (0..^((♯‘𝐽) + 1)))
597	595, 596	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...(♯‘𝐽)) = (0..^𝐻))
598	597	mpteq1d 5175	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
599	598	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
600	91, 561	eleqtrdi 2846	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐽) ∈ (ℤ_≥‘0))
601	143, 144, 146, 103, 155	mulgnn0cld 19071	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
602	23	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝐼 ∈ Fin)
603	256, 602, 110, 103, 253	esplympl 33711	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
604	523, 603	eqeltrid 2840	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
605	259	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
606	251, 252, 253, 50, 602, 161, 604, 605	evlcl 22080	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
607	50, 141, 110, 601, 606	ringcld 20241	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
608	532	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ (0...𝐻))
609	608, 535	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ (0...𝐻))
610	413, 609	sselid 3919	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ ℕ₀)
611	14, 71, 109, 610, 111	mulgnn0cld 19071	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
612	19, 13, 50, 70, 110, 607, 611	ply1vscl 22349	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
613		oveq1 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 0 → (𝑙 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
614	613	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝑙 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
615		2fveq3 6845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 0 → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘0)))
616	615	fveq1d 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 0 → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘0))‘𝑍))
617	616	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘0))‘𝑍))
618		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1_r‘(𝐼 mPoly 𝑅)) = (1_r‘(𝐼 mPoly 𝑅))
619	23, 32, 618	esplyfval0 33708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘0) = (1_r‘(𝐼 mPoly 𝑅)))
620	254	fveq1i 6841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐸‘0) = ((𝐼eSymPoly𝑅)‘0)
621	620	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘0) = ((𝐼eSymPoly𝑅)‘0))
622		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (algSc‘(𝐼 mPoly 𝑅)) = (algSc‘(𝐼 mPoly 𝑅))
623	252, 622, 277, 618, 23, 32	mplascl1 22004	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)) = (1_r‘(𝐼 mPoly 𝑅)))
624	619, 621, 623	3eqtr4d 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸‘0) = ((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))
625	624	fveq2d 6844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑄‘(𝐸‘0)) = (𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅))))
626	625	fveq1d 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘(𝐸‘0))‘𝑍) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍))
627	626	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘0))‘𝑍) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍))
628	251, 252, 50, 622, 23, 18, 242, 43	evlscaval 33684	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍) = (1_r‘𝑅))
629	628	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍) = (1_r‘𝑅))
630	617, 627, 629	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = (1_r‘𝑅))
631	614, 630	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)))
632		oveq2 7375	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 0 → (𝐻 − 𝑙) = (𝐻 − 0))
633	632	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 𝑙) = (𝐻 − 0))
634	293	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 = 0) → 𝐻 ∈ ℂ)
635	634	subid1d 11494	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 0) = 𝐻)
636	633, 635	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 𝑙) = 𝐻)
637	636	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = (𝐻(._g‘𝑀)𝑋))
638	631, 637	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 = 0) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))
639	13, 189, 89, 600, 612, 638	gsummptfzsplitla 33120	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))))
640		0p1e1 12298	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 1) = 1
641	640	oveq1i 7377	. . . . . . . . . . . . . . . 16 ⊢ ((0 + 1)...(♯‘𝐽)) = (1...(♯‘𝐽))
642	641	mpteq1i 5176	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))) = (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
643	642	oveq2i 7378	. . . . . . . . . . . . . 14 ⊢ (𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
644	643	oveq2i 7378	. . . . . . . . . . . . 13 ⊢ ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))) = ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
645	644	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))) = ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))))
646	29	ringabld 20264	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ Abel)
647		fzfid 13935	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐽)) ∈ Fin)
648	540	ralrimiva 3129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑙 ∈ (1...(♯‘𝐽))(((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
649	13, 89, 647, 648	gsummptcl 19942	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) ∈ (Base‘𝑊))
650	13, 189, 646, 249, 649	ablcomd 33106	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))))
651	639, 645, 650	3eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))))
652	599, 651	eqtr3d 2773	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))))
653	652	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → ((𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))))
654	592, 653	eqtr2d 2772	. . . . . . . 8 ⊢ (𝜑 → (((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
655	13, 189, 30, 649, 249, 263	grpassd 18921	. . . . . . . 8 ⊢ (𝜑 → (((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))))
656	560, 654, 655	3eqtr2rd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))))
657	32	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑅 ∈ Ring)
658	657, 145	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (mulGrp‘𝑅) ∈ Mnd)
659	565	sselda 3921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑘 ∈ ℕ₀)
660	154	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝑁‘ 1 ) ∈ 𝐵)
661	143, 144, 658, 659, 660	mulgnn0cld 19071	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
662	23	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝐼 ∈ Fin)
663	18	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑅 ∈ CRing)
664	254	fveq1i 6841	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑘) = ((𝐼eSymPoly𝑅)‘𝑘)
665	256, 662, 657, 659, 253	esplympl 33711	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐼 mPoly 𝑅)))
666	664, 665	eqeltrid 2840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐸‘𝑘) ∈ (Base‘(𝐼 mPoly 𝑅)))
667	259	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
668	251, 252, 253, 50, 662, 663, 666, 667	evlcl 22080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘𝑘))‘𝑍) ∈ 𝐵)
669	50, 141, 657, 661, 668	ringcld 20241	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ∈ 𝐵)
670	108	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑀 ∈ Mnd)
671		fznn0sub2 13589	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝐻) → (𝐻 − 𝑘) ∈ (0...𝐻))
672	671	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐻 − 𝑘) ∈ (0...𝐻))
673	413, 672	sselid 3919	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐻 − 𝑘) ∈ ℕ₀)
674	35	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑋 ∈ (Base‘𝑊))
675	14, 71, 670, 673, 674	mulgnn0cld 19071	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
676	19, 13, 50, 70, 657, 669, 675	ply1vscl 22349	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
677		oveq1 7374	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐻 − 𝑙) → (𝑘 ↑ (𝑁‘ 1 )) = ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )))
678		2fveq3 6845	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐻 − 𝑙) → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘(𝐻 − 𝑙))))
679	678	fveq1d 6842	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐻 − 𝑙) → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))
680	677, 679	oveq12d 7385	. . . . . . . . . 10 ⊢ (𝑘 = (𝐻 − 𝑙) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)))
681	680	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)))
682		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑘 = (𝐻 − 𝑙))
683	682	oveq2d 7383	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − 𝑘) = (𝐻 − (𝐻 − 𝑙)))
684	293	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝐻 ∈ ℂ)
685	566	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑙 ∈ ℕ₀)
686	685	nn0cnd 12500	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑙 ∈ ℂ)
687	684, 686	nncand 11510	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − (𝐻 − 𝑙)) = 𝑙)
688	683, 687	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − 𝑘) = 𝑙)
689	688	oveq1d 7382	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) = (𝑙(._g‘𝑀)𝑋))
690	681, 689	oveq12d 7385	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) = ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))
691	13, 89, 247, 676, 690	gsummptrev 33117	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
692	550, 656, 691	3eqtrd 2775	. . . . . 6 ⊢ (𝜑 → ((𝑊 Σ_g (𝑘 ∈ (0..^(♯‘𝐽)) ↦ ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
693	478, 512, 692	3eqtr3d 2779	. . . . 5 ⊢ (𝜑 → ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
694	69, 188, 693	3eqtrd 2775	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
695	694	fveq2d 6844	. . 3 ⊢ (𝜑 → (coe₁‘𝐹) = (coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))))
696	695	fveq1d 6842	. 2 ⊢ (𝜑 → ((coe₁‘𝐹)‘𝐾) = ((coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))‘𝐾))
697	12	fveq2i 6843	. . 3 ⊢ (._g‘𝑀) = (._g‘(mulGrp‘𝑊))
698	143, 144, 564, 578, 567	mulgnn0cld 19071	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) ∈ 𝐵)
699	254	fveq1i 6841	. . . . . . 7 ⊢ (𝐸‘(𝐻 − 𝑙)) = ((𝐼eSymPoly𝑅)‘(𝐻 − 𝑙))
700	256, 569, 563, 578, 253	esplympl 33711	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘(𝐻 − 𝑙)) ∈ (Base‘(𝐼 mPoly 𝑅)))
701	699, 700	eqeltrid 2840	. . . . . 6 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐸‘(𝐻 − 𝑙)) ∈ (Base‘(𝐼 mPoly 𝑅)))
702	251, 252, 253, 50, 569, 570, 701, 573	evlcl 22080	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍) ∈ 𝐵)
703	50, 141, 563, 698, 702	ringcld 20241	. . . 4 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) ∈ 𝐵)
704	703	ralrimiva 3129	. . 3 ⊢ (𝜑 → ∀𝑙 ∈ (0...𝐻)(((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) ∈ 𝐵)
705		vieta.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
706		oveq2 7375	. . . . 5 ⊢ (𝑙 = 𝐾 → (𝐻 − 𝑙) = (𝐻 − 𝐾))
707	706	oveq1d 7382	. . . 4 ⊢ (𝑙 = 𝐾 → ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) = ((𝐻 − 𝐾) ↑ (𝑁‘ 1 )))
708	706	fveq2d 6844	. . . . . 6 ⊢ (𝑙 = 𝐾 → (𝐸‘(𝐻 − 𝑙)) = (𝐸‘(𝐻 − 𝐾)))
709	708	fveq2d 6844	. . . . 5 ⊢ (𝑙 = 𝐾 → (𝑄‘(𝐸‘(𝐻 − 𝑙))) = (𝑄‘(𝐸‘(𝐻 − 𝐾))))
710	709	fveq1d 6842	. . . 4 ⊢ (𝑙 = 𝐾 → ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍) = ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍))
711	707, 710	oveq12d 7385	. . 3 ⊢ (𝑙 = 𝐾 → (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))
712	19, 13, 33, 697, 32, 50, 70, 247, 704, 705, 711	gsummoncoe1fz 33658	. 2 ⊢ (𝜑 → ((coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))
713	696, 712	eqtrd 2771	1 ⊢ (𝜑 → ((coe₁‘𝐹)‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3051 {crab 3389 Vcvv 3429 ∖ cdif 3886 ∪ cun 3887 ⊆ wss 3889 {csn 4567 class class class wbr 5085 ↦ cmpt 5166 ↾ cres 5633 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 ↑_m cmap 8773 Fincfn 8893 finSupp cfsupp 9274 ℂcc 11036 0cc0 11038 1c1 11039 + caddc 11041 − cmin 11377 ℕ₀cn0 12437 ℤcz 12524 ℤ_≥cuz 12788 ...cfz 13461 ..^cfzo 13608 ♯chash 14292 Basecbs 17179 +_gcplusg 17220 ._rcmulr 17221 Scalarcsca 17223 ·_𝑠 cvsca 17224 Σ_g cgsu 17403 Mndcmnd 18702 Grpcgrp 18909 inv_gcminusg 18910 -_gcsg 18911 ._gcmg 19043 CMndccmn 19755 Abelcabl 19756 mulGrpcmgp 20121 1_rcur 20162 Ringcrg 20214 CRingccrg 20215 IDomncidom 20670 LModclmod 20855 AssAlgcasa 21830 algSccascl 21832 mPoly cmpl 21886 eval cevl 22051 var₁cv1 22139 Poly₁cpl1 22140 coe₁cco1 22141 deg₁cdg1 26019 eSymPolycesply 33700

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 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-ofr 7632 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-oadd 8409 df-er 8643 df-map 8775 df-pm 8776 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-sup 9355 df-oi 9425 df-dju 9825 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-ind 12160 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-xnn0 12511 df-z 12525 df-dec 12645 df-uz 12789 df-rp 12943 df-fz 13462 df-fzo 13609 df-seq 13964 df-fac 14236 df-bc 14265 df-hash 14293 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-0g 17404 df-gsum 17405 df-prds 17410 df-pws 17412 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-mhm 18751 df-submnd 18752 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-ghm 19188 df-cntz 19292 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-srg 20168 df-ring 20216 df-cring 20217 df-rhm 20452 df-subrng 20523 df-subrg 20547 df-idom 20673 df-lmod 20857 df-lss 20927 df-lsp 20967 df-cnfld 21353 df-zring 21427 df-zrh 21483 df-assa 21833 df-asp 21834 df-ascl 21835 df-psr 21889 df-mvr 21890 df-mpl 21891 df-opsr 21893 df-evls 22052 df-evl 22053 df-psr1 22143 df-vr1 22144 df-ply1 22145 df-coe1 22146 df-mdeg 26020 df-deg1 26021 df-extv 33674 df-esply 33702

This theorem is referenced by: vieta 33724

W3C validator