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 33992

Description: Lemma for vieta 33993: 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 4118	. . . . . . . . 9 ⊢ (𝐽 ∪ {𝑌}) = ((𝐼 ∖ {𝑌}) ∪ {𝑌})
5		vietalem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ 𝐼)
6	5	snssd 4754	. . . . . . . . . 10 ⊢ (𝜑 → {𝑌} ⊆ 𝐼)
7		undifr 4446	. . . . . . . . . 10 ⊢ ({𝑌} ⊆ 𝐼 ↔ ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
8	6, 7	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
9	4, 8	eqtr2id 2813	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (𝐽 ∪ {𝑌}))
10	9	mpteq1d 5203	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))) = (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
11	10	oveq2d 7432	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
12		vieta.m	. . . . . . . 8 ⊢ 𝑀 = (mulGrp‘𝑊)
13		eqid 2765	. . . . . . . 8 ⊢ (Base‘𝑊) = (Base‘𝑊)
14	12, 13	mgpbas 20244	. . . . . . 7 ⊢ (Base‘𝑊) = (Base‘𝑀)
15		eqid 2765	. . . . . . . 8 ⊢ (._r‘𝑊) = (._r‘𝑊)
16	12, 15	mgpplusg 20243	. . . . . . 7 ⊢ (._r‘𝑊) = (+_g‘𝑀)
17		vieta.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ IDomn)
18	17	idomcringd 20854	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CRing)
19		vieta.w	. . . . . . . . 9 ⊢ 𝑊 = (Poly₁‘𝑅)
20	19	ply1crng 22387	. . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑊 ∈ CRing)
21	12	crngmgp 20346	. . . . . . . 8 ⊢ (𝑊 ∈ CRing → 𝑀 ∈ CMnd)
22	18, 20, 21	3syl 19	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ CMnd)
23		vieta.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
24		diffi 9162	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (𝐼 ∖ {𝑌}) ∈ Fin)
25	23, 24	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝐼 ∖ {𝑌}) ∈ Fin)
26	3, 25	eqeltrid 2869	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Fin)
27		vieta.3	. . . . . . . 8 ⊢ − = (-_g‘𝑊)
28	18, 20	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ CRing)
29	28	crngringd 20351	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Ring)
30	29	ringgrpd 20347	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Grp)
31	30	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑊 ∈ Grp)
32	17	idomringd 20855	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Ring)
33		vieta.x	. . . . . . . . . . 11 ⊢ 𝑋 = (var₁‘𝑅)
34	33, 19, 13	vr1cl 22406	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑊))
35	32, 34	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑊))
36	35	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑋 ∈ (Base‘𝑊))
37		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
38		eqid 2765	. . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
39		eqid 2765	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
40	19	ply1assa 22388	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → 𝑊 ∈ AssAlg)
41	18, 40	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ AssAlg)
42	41	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑊 ∈ AssAlg)
43		vieta.z	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
44	43	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑍:𝐼⟶𝐵)
45		difss 4090	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∖ {𝑌}) ⊆ 𝐼
46	3, 45	eqsstri 3984	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝐼
47	46	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
48	47	sselda 3938	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑛 ∈ 𝐼)
49	44, 48	ffvelcdmd 7084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑍‘𝑛) ∈ 𝐵)
50		vieta.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑅)
51	19	ply1sca 22441	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑊))
52	18, 51	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑊))
53	52	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑊)))
54	50, 53	eqtrid 2812	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊)))
55	54	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝐵 = (Base‘(Scalar‘𝑊)))
56	49, 55	eleqtrd 2867	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑍‘𝑛) ∈ (Base‘(Scalar‘𝑊)))
57	37, 38, 39, 42, 56	asclelbas 22062	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝐴‘(𝑍‘𝑛)) ∈ (Base‘𝑊))
58	13, 27, 31, 36, 57	grpsubcld 33384	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑋 − (𝐴‘(𝑍‘𝑛))) ∈ (Base‘𝑊))
59		neldifsnd 4763	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝐼 ∖ {𝑌}))
60	3	eleq2i 2857	. . . . . . . 8 ⊢ (𝑌 ∈ 𝐽 ↔ 𝑌 ∈ (𝐼 ∖ {𝑌}))
61	59, 60	sylnibr 332	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐽)
62	54, 43	feq3dd 6696	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍:𝐼⟶(Base‘(Scalar‘𝑊)))
63	62, 5	ffvelcdmd 7084	. . . . . . . . 9 ⊢ (𝜑 → (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)))
64	37, 38, 39, 41, 63	asclelbas 22062	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(𝑍‘𝑌)) ∈ (Base‘𝑊))
65	13, 27, 30, 35, 64	grpsubcld 33384	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝐴‘(𝑍‘𝑌))) ∈ (Base‘𝑊))
66		2fveq3 6890	. . . . . . . 8 ⊢ (𝑛 = 𝑌 → (𝐴‘(𝑍‘𝑛)) = (𝐴‘(𝑍‘𝑌)))
67	66	oveq2d 7432	. . . . . . 7 ⊢ (𝑛 = 𝑌 → (𝑋 − (𝐴‘(𝑍‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑌))))
68	14, 16, 22, 26, 58, 5, 61, 65, 67	gsumunsn 20053	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
69	2, 11, 68	3eqtrd 2804	. . . . 5 ⊢ (𝜑 → 𝐹 = ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
70		eqid 2765	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
71		eqid 2765	. . . . . . . . 9 ⊢ (._g‘𝑀) = (._g‘𝑀)
72		eqid 2765	. . . . . . . . 9 ⊢ (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
73		eqid 2765	. . . . . . . . 9 ⊢ ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
74		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑛 ∈ 𝐽)
75	74	fvresd 6905	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → ((𝑍 ↾ 𝐽)‘𝑛) = (𝑍‘𝑛))
76	75	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)) = (𝐴‘(𝑍‘𝑛)))
77	76	oveq2d 7432	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
78	77	mpteq2dva 5206	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))) = (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
79	78	oveq2d 7432	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
80	58	ralrimiva 3159	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝐽 (𝑋 − (𝐴‘(𝑍‘𝑛))) ∈ (Base‘𝑊))
81	14, 22, 26, 80	gsummptcl 20060	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) ∈ (Base‘𝑊))
82	79, 81	eqeltrd 2865	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘𝑊))
83	19, 33, 13, 70, 12, 71, 72, 73, 32, 82	ply1coedeg 33902	. . . . . . . 8 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
84		vietalem.3	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (♯‘𝐽))
85	84	oveq2d 7432	. . . . . . . . . 10 ⊢ (𝜑 → (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) = (0...(♯‘𝐽)))
86	85	mpteq1d 5203	. . . . . . . . 9 ⊢ (𝜑 → (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))
87	86	oveq2d 7432	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
88	83, 79, 87	3eqtr3d 2808	. . . . . . 7 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
89	29	ringcmnd 20391	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ CMnd)
90		hashcl 14405	. . . . . . . . 9 ⊢ (𝐽 ∈ Fin → (♯‘𝐽) ∈ ℕ₀)
91	26, 90	syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐽) ∈ ℕ₀)
92	19	ply1lmod 22440	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑊 ∈ LMod)
93	32, 92	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ LMod)
94	93	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑊 ∈ LMod)
95	82	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘𝑊))
96	52	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Poly₁‘𝑅) = (Poly₁‘(Scalar‘𝑊)))
97	19, 96	eqtrid 2812	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 = (Poly₁‘(Scalar‘𝑊)))
98	97	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑊) = (Base‘(Poly₁‘(Scalar‘𝑊))))
99	98	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (Base‘𝑊) = (Base‘(Poly₁‘(Scalar‘𝑊))))
100	95, 99	eleqtrd 2867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘(Poly₁‘(Scalar‘𝑊))))
101		fz0ssnn0 13662	. . . . . . . . . . 11 ⊢ (0...(♯‘𝐽)) ⊆ ℕ₀
102		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ (0...(♯‘𝐽)))
103	101, 102	sselid 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ ℕ₀)
104		eqid 2765	. . . . . . . . . . 11 ⊢ (Base‘(Poly₁‘(Scalar‘𝑊))) = (Base‘(Poly₁‘(Scalar‘𝑊)))
105		eqid 2765	. . . . . . . . . . 11 ⊢ (Poly₁‘(Scalar‘𝑊)) = (Poly₁‘(Scalar‘𝑊))
106	72, 104, 105, 39	coe1fvalcl 22401	. . . . . . . . . 10 ⊢ (((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘(Poly₁‘(Scalar‘𝑊))) ∧ 𝑙 ∈ ℕ₀) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) ∈ (Base‘(Scalar‘𝑊)))
107	100, 103, 106	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) ∈ (Base‘(Scalar‘𝑊)))
108	22	cmnmndd 19897	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ Mnd)
109	108	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
110	32	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
111	110, 34	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
112	14, 71, 109, 103, 111	mulgnn0cld 19184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑙(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
113	13, 38, 70, 39, 94, 107, 112	lmodvscld 21029	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
114		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑙 = ((♯‘𝐽) − 𝑘))
115	114	fveq2d 6889	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) = ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)))
116		oveq1 7423	. . . . . . . . . 10 ⊢ (𝑙 = ((♯‘𝐽) − 𝑘) → (𝑙(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
117	116	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (𝑙(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
118	115, 117	oveq12d 7434	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) = (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
119	13, 89, 91, 113, 118	gsummptrev 33399	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
120		fveq1 6884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑧‘𝑛) = ((𝑍 ↾ 𝐽)‘𝑛))
121	120	fveq2d 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝐴‘(𝑧‘𝑛)) = (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))
122	121	oveq2d 7432	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))
123	122	mpteq2dv 5207	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))
124	123	oveq2d 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
125	124	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))))
126	125	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)))
127		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
128	127	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
129	126, 128	eqeq12d 2781	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
130	129	ralbidv 3190	. . . . . . . . . . . . 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 6899	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
133	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ V)
134	43, 47	fssresd 6749	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 ↾ 𝐽):𝐽⟶𝐵)
135	133, 26, 134	elmapdd 8840	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
136	130, 131, 135	rspcdva 3584	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐽))((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
137	136	r19.21bi 3259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
138	137	oveq1d 7431	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
139	138	mpteq2dva 5206	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))) = (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
140	139	oveq2d 7432	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
141		vieta.t	. . . . . . . . . . 11 ⊢ · = (._r‘𝑅)
142		eqid 2765	. . . . . . . . . . . . 13 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
143	142, 50	mgpbas 20244	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
144		vieta.p	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘(mulGrp‘𝑅))
145	142	ringmgp 20344	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
146	110, 145	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
147		fznn0sub2 13675	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑙) ∈ (0...(♯‘𝐽)))
148	147	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑙) ∈ (0...(♯‘𝐽)))
149	101, 148	sselid 3936	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑙) ∈ ℕ₀)
150		vieta.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (inv_g‘𝑅)
151	32	ringgrpd 20347	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Grp)
152		vieta.1	. . . . . . . . . . . . . . 15 ⊢ 1 = (1_r‘𝑅)
153	50, 152, 32	ringidcld 20373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ 𝐵)
154	50, 150, 151, 153	grpinvcld 19078	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
155	154	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
156	143, 144, 146, 149, 155	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) ∈ 𝐵)
157		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝐽 eval 𝑅) = (𝐽 eval 𝑅)
158		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝐽 mPoly 𝑅) = (𝐽 mPoly 𝑅)
159		eqid 2765	. . . . . . . . . . . 12 ⊢ (Base‘(𝐽 mPoly 𝑅)) = (Base‘(𝐽 mPoly 𝑅))
160	26	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
161	18	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
162		eqid 2765	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}
163	162, 160, 110, 149, 159	esplympl 33980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)) ∈ (Base‘(𝐽 mPoly 𝑅)))
164	135	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
165	157, 158, 159, 50, 160, 161, 163, 164	evlcl 22282	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
166	50, 141, 110, 156, 165	ringcld 20362	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
167	19, 13, 50, 70, 110, 166, 112	ply1vscl 22570	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
168	91	nn0cnd 12578	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘𝐽) ∈ ℂ)
169	168	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (♯‘𝐽) ∈ ℂ)
170		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ (0...(♯‘𝐽)))
171	101, 170	sselid 3936	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ ℕ₀)
172	171	nn0cnd 12578	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ ℂ)
173	169, 172	subcld 11580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑘) ∈ ℂ)
174	114, 173	eqeltrd 2865	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑙 ∈ ℂ)
175	169, 174	subcld 11580	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑙) ∈ ℂ)
176	169, 174	nncand 11585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = 𝑙)
177	176, 114	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = ((♯‘𝐽) − 𝑘))
178	169, 175, 172, 177	subcand 11621	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑙) = 𝑘)
179	178	oveq1d 7431	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
180	178	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)) = ((𝐽eSymPoly𝑅)‘𝑘))
181	180	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙))) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)))
182	181	fveq1d 6887	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
183	179, 182	oveq12d 7434	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
184	183, 117	oveq12d 7434	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
185	13, 89, 91, 167, 184	gsummptrev 33399	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
186	140, 185	eqtr4d 2803	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
187	88, 119, 186	3eqtrd 2804	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
188	187	oveq1d 7431	. . . . 5 ⊢ (𝜑 → ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
189		eqid 2765	. . . . . . 7 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
190	32	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
191	190, 145	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
192		elfznn0 13660	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...(♯‘𝐽)) → 𝑖 ∈ ℕ₀)
193	192	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑖 ∈ ℕ₀)
194	154	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
195	143, 144, 191, 193, 194	mulgnn0cld 19184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑖 ↑ (𝑁‘ 1 )) ∈ 𝐵)
196	26	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
197	18	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
198	162, 196, 190, 193, 159	esplympl 33980	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑖) ∈ (Base‘(𝐽 mPoly 𝑅)))
199	135	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
200	157, 158, 159, 50, 196, 197, 198, 199	evlcl 22282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
201	50, 141, 190, 195, 200	ringcld 20362	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
202	108	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
203		fznn0sub2 13675	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑖) ∈ (0...(♯‘𝐽)))
204	203	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑖) ∈ (0...(♯‘𝐽)))
205	101, 204	sselid 3936	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑖) ∈ ℕ₀)
206	35	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
207	14, 71, 202, 205, 206	mulgnn0cld 19184	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
208	19, 13, 50, 70, 190, 201, 207	ply1vscl 22570	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
209		oveq1 7423	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
210		2fveq3 6890	. . . . . . . . . 10 ⊢ (𝑖 = 0 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)))
211	210	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑖 = 0 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))
212	209, 211	oveq12d 7434	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))))
213		oveq2 7424	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − 0))
214	213	oveq1d 7431	. . . . . . . 8 ⊢ (𝑖 = 0 → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − 0)(._g‘𝑀)𝑋))
215	212, 214	oveq12d 7434	. . . . . . 7 ⊢ (𝑖 = 0 → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋)))
216		oveq1 7423	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → (𝑖 ↑ (𝑁‘ 1 )) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
217		2fveq3 6890	. . . . . . . . . 10 ⊢ (𝑖 = (♯‘𝐽) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽))))
218	217	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))
219	216, 218	oveq12d 7434	. . . . . . . 8 ⊢ (𝑖 = (♯‘𝐽) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))
220		oveq2 7424	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − (♯‘𝐽)))
221	220	oveq1d 7431	. . . . . . . 8 ⊢ (𝑖 = (♯‘𝐽) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))
222	219, 221	oveq12d 7434	. . . . . . 7 ⊢ (𝑖 = (♯‘𝐽) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)))
223		oveq1 7423	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
224		2fveq3 6890	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)))
225	224	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
226	223, 225	oveq12d 7434	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
227		oveq2 7424	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − 𝑘))
228	227	oveq1d 7431	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
229	226, 228	oveq12d 7434	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
230		oveq1 7423	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ↑ (𝑁‘ 1 )) = ((𝑘 + 1) ↑ (𝑁‘ 1 )))
231		2fveq3 6890	. . . . . . . . . 10 ⊢ (𝑖 = (𝑘 + 1) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1))))
232	231	fveq1d 6887	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))
233	230, 232	oveq12d 7434	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
234		oveq2 7424	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − (𝑘 + 1)))
235	234	oveq1d 7431	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))
236	233, 235	oveq12d 7434	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)))
237		eqid 2765	. . . . . . . . 9 ⊢ (inv_g‘𝑊) = (inv_g‘𝑊)
238	32, 145	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
239		0nn0 12530	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ₀
240	239	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ₀)
241	143, 144, 238, 240, 154	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) ∈ 𝐵)
242	152, 153	eqeltrrid 2870	. . . . . . . . . . 11 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝐵)
243	50, 141, 32, 241, 242	ringcld 20362	. . . . . . . . . 10 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)) ∈ 𝐵)
244		vieta.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (♯‘𝐼)
245		hashcl 14405	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ₀)
246	23, 245	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐼) ∈ ℕ₀)
247	244, 246	eqeltrid 2869	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℕ₀)
248	14, 71, 108, 247, 35	mulgnn0cld 19184	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
249	19, 13, 50, 70, 32, 243, 248	ply1vscl 22570	. . . . . . . . 9 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
250	143, 144, 238, 247, 154	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) ∈ 𝐵)
251		vieta.q	. . . . . . . . . . . 12 ⊢ 𝑄 = (𝐼 eval 𝑅)
252		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝐼 mPoly 𝑅) = (𝐼 mPoly 𝑅)
253		eqid 2765	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPoly 𝑅)) = (Base‘(𝐼 mPoly 𝑅))
254		vieta.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
255	254	fveq1i 6886	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐻) = ((𝐼eSymPoly𝑅)‘𝐻)
256		eqid 2765	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
257	256, 23, 32, 247, 253	esplympl 33980	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐻) ∈ (Base‘(𝐼 mPoly 𝑅)))
258	255, 257	eqeltrid 2869	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝐻) ∈ (Base‘(𝐼 mPoly 𝑅)))
259	133, 23, 43	elmapdd 8840	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑_m 𝐼))
260	251, 252, 253, 50, 23, 18, 258, 259	evlcl 22282	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘(𝐸‘𝐻))‘𝑍) ∈ 𝐵)
261	50, 141, 32, 250, 260	ringcld 20362	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) ∈ 𝐵)
262	14, 71, 108, 240, 35	mulgnn0cld 19184	. . . . . . . . . 10 ⊢ (𝜑 → (0(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
263	19, 13, 50, 70, 32, 261, 262	ply1vscl 22570	. . . . . . . . 9 ⊢ (𝜑 → (((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
264	13, 189, 27, 237, 30, 249, 263	grpsubinv 19101	. . . . . . . 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 33980	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘0) ∈ (Base‘(𝐽 mPoly 𝑅)))
266	157, 158, 159, 50, 26, 18, 265, 135	evlcl 22282	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
267	50, 141, 32, 241, 266	ringcld 20362	. . . . . . . . . . . 12 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
268	267, 54	eleqtrd 2867	. . . . . . . . . . 11 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
269	168	subid1d 11569	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − 0) = (♯‘𝐽))
270	269, 91	eqeltrd 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐽) − 0) ∈ ℕ₀)
271	14, 71, 108, 270, 35	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝐽) − 0)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
272	13, 38, 39, 70, 15, 41, 268, 271, 35	assaassd 33868	. . . . . . . . . 10 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) = (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
273		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘(𝐽 mPoly 𝑅)) = (1_r‘(𝐽 mPoly 𝑅))
274	26, 32, 273	esplyfval0 33977	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘0) = (1_r‘(𝐽 mPoly 𝑅)))
275	274	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)) = ((𝐽 eval 𝑅)‘(1_r‘(𝐽 mPoly 𝑅))))
276		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (algSc‘(𝐽 mPoly 𝑅)) = (algSc‘(𝐽 mPoly 𝑅))
277		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
278	158, 276, 277, 273, 26, 32	mplascl1 22205	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)) = (1_r‘(𝐽 mPoly 𝑅)))
279	278	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅))) = ((𝐽 eval 𝑅)‘(1_r‘(𝐽 mPoly 𝑅))))
280	275, 279	eqtr4d 2803	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)) = ((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅))))
281	280	fveq1d 6887	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)))‘(𝑍 ↾ 𝐽)))
282	157, 158, 50, 276, 26, 18, 242, 134	evlscaval 33953	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)))‘(𝑍 ↾ 𝐽)) = (1_r‘𝑅))
283	281, 282	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) = (1_r‘𝑅))
284	283	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) = ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)))
285	14, 71, 16	mulgnn0p1 19174	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ Mnd ∧ (♯‘𝐽) ∈ ℕ₀ ∧ 𝑋 ∈ (Base‘𝑊)) → (((♯‘𝐽) + 1)(._g‘𝑀)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
286	108, 91, 35, 285	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) + 1)(._g‘𝑀)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
287		hashdifsn 14464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼) → (♯‘(𝐼 ∖ {𝑌})) = ((♯‘𝐼) − 1))
288	23, 5, 287	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐼 ∖ {𝑌})) = ((♯‘𝐼) − 1))
289	3	fveq2i 6888	. . . . . . . . . . . . . . . 16 ⊢ (♯‘𝐽) = (♯‘(𝐼 ∖ {𝑌}))
290	244	oveq1i 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 − 1) = ((♯‘𝐼) − 1)
291	288, 289, 290	3eqtr4g 2825	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐽) = (𝐻 − 1))
292	291	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((♯‘𝐽) + 1) = ((𝐻 − 1) + 1))
293	247	nn0cnd 12578	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ ℂ)
294		1cnd 11213	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
295	293, 294	npcand 11584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐻 − 1) + 1) = 𝐻)
296	292, 295	eqtr2d 2801	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 = ((♯‘𝐽) + 1))
297	296	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻(._g‘𝑀)𝑋) = (((♯‘𝐽) + 1)(._g‘𝑀)𝑋))
298	269	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐽) − 0)(._g‘𝑀)𝑋) = ((♯‘𝐽)(._g‘𝑀)𝑋))
299	298	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
300	286, 297, 299	3eqtr4rd 2811	. . . . . . . . . . 11 ⊢ (𝜑 → ((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋) = (𝐻(._g‘𝑀)𝑋))
301	284, 300	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))
302	272, 301	eqtr2d 2801	. . . . . . . . 9 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) = ((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋))
303	52	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝑅) = (._r‘(Scalar‘𝑊)))
304	141, 303	eqtrid 2812	. . . . . . . . . . . . 13 ⊢ (𝜑 → · = (._r‘(Scalar‘𝑊)))
305	304	oveqd 7433	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
306	305	oveq1d 7431	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)))
307	43, 5	ffvelcdmd 7084	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑌) ∈ 𝐵)
308	143, 144, 238, 91, 154	mulgnn0cld 19184	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝐽) ↑ (𝑁‘ 1 )) ∈ 𝐵)
309	162, 26, 32, 91, 159	esplympl 33980	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘(♯‘𝐽)) ∈ (Base‘(𝐽 mPoly 𝑅)))
310	157, 158, 159, 50, 26, 18, 309, 135	evlcl 22282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
311	50, 141, 18, 307, 308, 310	crng12d 20364	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
312	296	oveq1d 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) = (((♯‘𝐽) + 1) ↑ (𝑁‘ 1 )))
313	152, 150, 144, 32, 91	ringm1expp1 33576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((♯‘𝐽) + 1) ↑ (𝑁‘ 1 )) = (𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 ))))
314	312, 313	eqtrd 2800	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) = (𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 ))))
315	314	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) = (𝑁‘(𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 )))))
316	50, 150, 151, 308	grpinvinvd 33383	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁‘(𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 )))) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
317	315, 316	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
318		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
319		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝐽eSymPoly𝑅) = (𝐽eSymPoly𝑅)
320		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (♯‘𝐽) = (♯‘𝐽)
321	50, 318, 141, 251, 157, 254, 319, 244, 320, 3, 23, 18, 5, 43	esplyfvn 33990	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘(𝐸‘𝐻))‘𝑍) = ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))
322	317, 321	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
323	311, 322	eqtr4d 2803	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
324	50, 141, 150, 32, 250, 260	ringmneg1 20412	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) = (𝑁‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
325	52	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (inv_g‘𝑅) = (inv_g‘(Scalar‘𝑊)))
326	150, 325	eqtrid 2812	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 = (inv_g‘(Scalar‘𝑊)))
327	326	fveq1d 6887	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))) = ((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
328	323, 324, 327	3eqtrd 2804	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
329	168	subidd 11568	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − (♯‘𝐽)) = 0)
330	329	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋) = (0(._g‘𝑀)𝑋))
331	328, 330	oveq12d 7434	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
332	50, 141, 32, 308, 310	ringcld 20362	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
333	332, 54	eleqtrd 2867	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
334	329, 240	eqeltrd 2865	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − (♯‘𝐽)) ∈ ℕ₀)
335	14, 71, 108, 334, 35	mulgnn0cld 19184	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
336		eqid 2765	. . . . . . . . . . . . 13 ⊢ (._r‘(Scalar‘𝑊)) = (._r‘(Scalar‘𝑊))
337	13, 38, 70, 39, 336	lmodvsass 21037	. . . . . . . . . . . 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 1399	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
339	306, 331, 338	3eqtr3d 2808	. . . . . . . . . 10 ⊢ (𝜑 → (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
340		eqid 2765	. . . . . . . . . . 11 ⊢ (inv_g‘(Scalar‘𝑊)) = (inv_g‘(Scalar‘𝑊))
341	261, 54	eleqtrd 2867	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) ∈ (Base‘(Scalar‘𝑊)))
342	13, 38, 70, 237, 39, 340, 93, 262, 341	lmodvsneg 21056	. . . . . . . . . 10 ⊢ (𝜑 → ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
343	19, 13, 50, 70, 32, 332, 335	ply1vscl 22570	. . . . . . . . . . 11 ⊢ (𝜑 → ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
344	37, 38, 39, 13, 15, 70	asclmul2 22066	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ AssAlg ∧ (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) ∈ (Base‘𝑊)) → (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
345	41, 63, 343, 344	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
346	339, 342, 345	3eqtr4d 2810	. . . . . . . . 9 ⊢ (𝜑 → ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))))
347	302, 346	oveq12d 7434	. . . . . . . 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 2802	. . . . . . 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 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Ring)
350	349, 145	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
351		fzossfz 13719	. . . . . . . . . . . . . . . 16 ⊢ (0..^(♯‘𝐽)) ⊆ (0...(♯‘𝐽))
352		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ (0..^(♯‘𝐽)))
353	351, 352	sselid 3936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ (0...(♯‘𝐽)))
354	101, 353	sselid 3936	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ ℕ₀)
355		peano2nn0 12555	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
356	354, 355	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ ℕ₀)
357	154	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
358	143, 144, 350, 356, 357	mulgnn0cld 19184	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 + 1) ↑ (𝑁‘ 1 )) ∈ 𝐵)
359	26	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐽 ∈ Fin)
360	18	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ CRing)
361	162, 359, 349, 356, 159	esplympl 33980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘(𝑘 + 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
362	135	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
363	157, 158, 159, 50, 359, 360, 361, 362	evlcl 22282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
364	43	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑍:𝐼⟶𝐵)
365	5	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑌 ∈ 𝐼)
366	364, 365	ffvelcdmd 7084	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍‘𝑌) ∈ 𝐵)
367	162, 359, 349, 354, 159	esplympl 33980	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐽 mPoly 𝑅)))
368	157, 158, 159, 50, 359, 360, 367, 362	evlcl 22282	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
369	50, 141, 349, 366, 368	ringcld 20362	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
370	50, 318, 141, 349, 358, 363, 369	ringdid 20369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
371	23	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐼 ∈ Fin)
372	254	fveq1i 6886	. . . . . . . . . . . . . 14 ⊢ (𝐸‘(𝑘 + 1)) = ((𝐼eSymPoly𝑅)‘(𝑘 + 1))
373	141, 371, 360, 365, 3, 319, 353, 162, 372, 50, 251, 157, 318, 364	esplyindfv 33989	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍) = (((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
374	32	ringabld 20390	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ Abel)
375	374	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Abel)
376	50, 318, 375, 369, 363	ablcomd 33388	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
377	373, 376	eqtrd 2800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
378	377	oveq2d 7432	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
379		eqid 2765	. . . . . . . . . . . 12 ⊢ (-_g‘𝑅) = (-_g‘𝑅)
380	151	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Grp)
381	50, 141, 349, 358, 363	ringcld 20362	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
382	50, 141, 349, 358, 369	ringcld 20362	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) ∈ 𝐵)
383	50, 318, 379, 150, 380, 381, 382	grpsubinv 19101	. . . . . . . . . . 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 2810	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘𝑅)(𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))))
385	52	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝜑 → (-_g‘𝑅) = (-_g‘(Scalar‘𝑊)))
386	385	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (-_g‘𝑅) = (-_g‘(Scalar‘𝑊)))
387		eqidd 2766	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
388	238	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (mulGrp‘𝑅) ∈ Mnd)
389		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
390	154	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑁‘ 1 ) ∈ 𝐵)
391	143, 144, 388, 389, 390	mulgnn0cld 19184	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
392	354, 391	syldan 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
393	50, 141, 349, 392, 368, 366	ringassd 20363	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌))))
394	152, 150, 144, 349, 354	ringm1expp1 33576	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 + 1) ↑ (𝑁‘ 1 )) = (𝑁‘(𝑘 ↑ (𝑁‘ 1 ))))
395	394	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) = (𝑁‘(𝑁‘(𝑘 ↑ (𝑁‘ 1 )))))
396	50, 150, 380, 392	grpinvinvd 33383	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘(𝑁‘(𝑘 ↑ (𝑁‘ 1 )))) = (𝑘 ↑ (𝑁‘ 1 )))
397	395, 396	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) = (𝑘 ↑ (𝑁‘ 1 )))
398	50, 141, 360, 366, 368	crngcomd 20360	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌)))
399	397, 398	oveq12d 7434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌))))
400	50, 141, 150, 349, 358, 369	ringmneg1 20412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = (𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
401	393, 399, 400	3eqtr2rd 2807	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)))
402	386, 387, 401	oveq123d 7437	. . . . . . . . . 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 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))))
404	403	oveq1d 7431	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
405		eqid 2765	. . . . . . . . 9 ⊢ (-_g‘(Scalar‘𝑊)) = (-_g‘(Scalar‘𝑊))
406	349, 92	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑊 ∈ LMod)
407	54	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐵 = (Base‘(Scalar‘𝑊)))
408	381, 407	eleqtrd 2867	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
409	50, 141, 349, 392, 368	ringcld 20362	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
410	50, 141, 349, 409, 366	ringcld 20362	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) ∈ 𝐵)
411	410, 407	eleqtrd 2867	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) ∈ (Base‘(Scalar‘𝑊)))
412	108	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑀 ∈ Mnd)
413		fz0ssnn0 13662	. . . . . . . . . . 11 ⊢ (0...𝐻) ⊆ ℕ₀
414		fzossfz 13719	. . . . . . . . . . . 12 ⊢ (0..^𝐻) ⊆ (0...𝐻)
415		fzssp1 13607	. . . . . . . . . . . . . . . 16 ⊢ (1...(♯‘𝐽)) ⊆ (1...((♯‘𝐽) + 1))
416	296	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝐻) = (1...((♯‘𝐽) + 1)))
417	415, 416	sseqtrrid 3981	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ (1...𝐻))
418	417	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (1...(♯‘𝐽)) ⊆ (1...𝐻))
419	359, 90	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) ∈ ℕ₀)
420		fz0add1fz1 13776	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐽) ∈ ℕ₀ ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...(♯‘𝐽)))
421	419, 352, 420	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...(♯‘𝐽)))
422	418, 421	sseldd 3939	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...𝐻))
423		ubmelfzo 13771	. . . . . . . . . . . . 13 ⊢ ((𝑘 + 1) ∈ (1...𝐻) → (𝐻 − (𝑘 + 1)) ∈ (0..^𝐻))
424	422, 423	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ (0..^𝐻))
425	414, 424	sselid 3936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ (0...𝐻))
426	413, 425	sselid 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ ℕ₀)
427	349, 34	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
428	14, 71, 412, 426, 427	mulgnn0cld 19184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
429	13, 70, 38, 39, 27, 405, 406, 408, 411, 428	lmodsubdir 21070	. . . . . . . 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 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐻 = ((♯‘𝐽) + 1))
431	430	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = (((♯‘𝐽) + 1) − (𝑘 + 1)))
432	168	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) ∈ ℂ)
433		1cnd 11213	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 1 ∈ ℂ)
434	356	nn0cnd 12578	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ ℂ)
435	432, 433, 434	addsubd 11601	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) + 1) − (𝑘 + 1)) = (((♯‘𝐽) − (𝑘 + 1)) + 1))
436	431, 435	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = (((♯‘𝐽) − (𝑘 + 1)) + 1))
437	436	oveq1d 7431	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋))
438		fzofzp1 13805	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^(♯‘𝐽)) → (𝑘 + 1) ∈ (0...(♯‘𝐽)))
439	438	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (0...(♯‘𝐽)))
440		fznn0sub2 13675	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 + 1) ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − (𝑘 + 1)) ∈ (0...(♯‘𝐽)))
441	439, 440	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − (𝑘 + 1)) ∈ (0...(♯‘𝐽)))
442	101, 441	sselid 3936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − (𝑘 + 1)) ∈ ℕ₀)
443	14, 71, 16	mulgnn0p1 19174	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ Mnd ∧ ((♯‘𝐽) − (𝑘 + 1)) ∈ ℕ₀ ∧ 𝑋 ∈ (Base‘𝑊)) → ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
444	412, 442, 427, 443	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
445	437, 444	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
446	445	oveq2d 7432	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
447	360, 40	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑊 ∈ AssAlg)
448	14, 71, 412, 442, 427	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
449	13, 38, 39, 70, 15, 447, 408, 448, 427	assaassd 33868	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
450	446, 449	eqtr4d 2803	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋))
451	63	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)))
452	409, 407	eleqtrd 2867	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
453		fznn0sub2 13675	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
454	353, 453	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
455	101, 454	sselid 3936	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ ℕ₀)
456	14, 71, 412, 455, 427	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
457	13, 38, 70, 39, 336	lmodvsass 21037	. . . . . . . . . . 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 1399	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
459	50, 141, 360, 409, 366	crngcomd 20360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
460	304	oveqd 7433	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
461	460	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
462	459, 461	eqtrd 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
463	291	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) = (𝐻 − 1))
464	463	oveq1d 7431	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) = ((𝐻 − 1) − 𝑘))
465	293	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐻 ∈ ℂ)
466	354	nn0cnd 12578	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ ℂ)
467	465, 466, 433	sub32d 11612	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − 𝑘) − 1) = ((𝐻 − 1) − 𝑘))
468	465, 466, 433	subsub4d 11611	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − 𝑘) − 1) = (𝐻 − (𝑘 + 1)))
469	464, 467, 468	3eqtr2rd 2807	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = ((♯‘𝐽) − 𝑘))
470	469	oveq1d 7431	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
471	462, 470	oveq12d 7434	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
472	19, 13, 50, 70, 349, 409, 456	ply1vscl 22570	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
473	37, 38, 39, 13, 15, 70	asclmul2 22066	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ AssAlg ∧ (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊)) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
474	447, 451, 472, 473	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
475	458, 471, 474	3eqtr4d 2810	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))))
476	450, 475	oveq12d 7434	. . . . . . . 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 2804	. . . . . . 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 33414	. . . . . 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 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
480	479, 145	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
481	101	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐽)) ⊆ ℕ₀)
482	481	sselda 3938	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑘 ∈ ℕ₀)
483	154	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
484	143, 144, 480, 482, 483	mulgnn0cld 19184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
485	26	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
486	18	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
487	162, 485, 479, 482, 159	esplympl 33980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐽 mPoly 𝑅)))
488	135	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
489	157, 158, 159, 50, 485, 486, 487, 488	evlcl 22282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
490	50, 141, 479, 484, 489	ringcld 20362	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
491	108	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
492	453	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
493	101, 492	sselid 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ ℕ₀)
494	35	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
495	14, 71, 491, 493, 494	mulgnn0cld 19184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
496	19, 13, 50, 70, 479, 490, 495	ply1vscl 22570	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
497		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → (𝑘 ↑ (𝑁‘ 1 )) = (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )))
498		2fveq3 6890	. . . . . . . . . . . 12 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙))))
499	498	fveq1d 6887	. . . . . . . . . . 11 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))
500	497, 499	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))))
501	500	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))))
502		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑘 = ((♯‘𝐽) − 𝑙))
503	502	oveq2d 7432	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − 𝑘) = ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)))
504	168	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (♯‘𝐽) ∈ ℂ)
505	103	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑙 ∈ ℕ₀)
506	505	nn0cnd 12578	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑙 ∈ ℂ)
507	504, 506	nncand 11585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = 𝑙)
508	503, 507	eqtrd 2800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − 𝑘) = 𝑙)
509	508	oveq1d 7431	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) = (𝑙(._g‘𝑀)𝑋))
510	501, 509	oveq12d 7434	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))
511	13, 89, 91, 496, 510	gsummptrev 33399	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
512	511	oveq1d 7431	. . . . . 6 ⊢ (𝜑 → ((𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
513	32	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑅 ∈ Ring)
514	513, 145	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
515		fz1ssfz0 13663	. . . . . . . . . . . . . . 15 ⊢ (1...(♯‘𝐽)) ⊆ (0...(♯‘𝐽))
516	515, 101	sstri 3947	. . . . . . . . . . . . . 14 ⊢ (1...(♯‘𝐽)) ⊆ ℕ₀
517	516	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ ℕ₀)
518	517	sselda 3938	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑙 ∈ ℕ₀)
519	154	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
520	143, 144, 514, 518, 519	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
521	23	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝐼 ∈ Fin)
522	18	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑅 ∈ CRing)
523	254	fveq1i 6886	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝑙) = ((𝐼eSymPoly𝑅)‘𝑙)
524	256, 521, 513, 518, 253	esplympl 33980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
525	523, 524	eqeltrid 2869	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
526	259	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
527	251, 252, 253, 50, 521, 522, 525, 526	evlcl 22282	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
528	50, 141, 513, 520, 527	ringcld 20362	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
529	108	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑀 ∈ Mnd)
530		fzssp1 13607	. . . . . . . . . . . . . . . 16 ⊢ (0...(♯‘𝐽)) ⊆ (0...((♯‘𝐽) + 1))
531	296	oveq2d 7432	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0...𝐻) = (0...((♯‘𝐽) + 1)))
532	530, 531	sseqtrrid 3981	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0...(♯‘𝐽)) ⊆ (0...𝐻))
533	515, 532	sstrid 3949	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ (0...𝐻))
534	533	sselda 3938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑙 ∈ (0...𝐻))
535		fznn0sub2 13675	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ (0...𝐻) → (𝐻 − 𝑙) ∈ (0...𝐻))
536	534, 535	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ (0...𝐻))
537	413, 536	sselid 3936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ ℕ₀)
538	513, 34	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
539	14, 71, 529, 537, 538	mulgnn0cld 19184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
540	19, 13, 50, 70, 513, 528, 539	ply1vscl 22570	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
541		oveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → (𝑙 ↑ (𝑁‘ 1 )) = ((𝑘 + 1) ↑ (𝑁‘ 1 )))
542		2fveq3 6890	. . . . . . . . . . . . 13 ⊢ (𝑙 = (𝑘 + 1) → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘(𝑘 + 1))))
543	542	fveq1d 6887	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))
544	541, 543	oveq12d 7434	. . . . . . . . . . 11 ⊢ (𝑙 = (𝑘 + 1) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)))
545		oveq2 7424	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → (𝐻 − 𝑙) = (𝐻 − (𝑘 + 1)))
546	545	oveq1d 7431	. . . . . . . . . . 11 ⊢ (𝑙 = (𝑘 + 1) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))
547	544, 546	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝑙 = (𝑘 + 1) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
548	547	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) ∧ 𝑙 = (𝑘 + 1)) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
549	13, 89, 91, 540, 548	gsummptp1 33400	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0..^(♯‘𝐽)) ↦ ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
550	549	oveq1d 7431	. . . . . . 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 7423	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
552		2fveq3 6890	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝑙)))
553	552	fveq1d 6887	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝑙))‘𝑍))
554	551, 553	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)))
555		oveq2 7424	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → (𝐻 − 𝑘) = (𝐻 − 𝑙))
556	555	oveq1d 7431	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) = ((𝐻 − 𝑙)(._g‘𝑀)𝑋))
557	554, 556	oveq12d 7434	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) = (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
558	557	cbvmptv 5217	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
559	558	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
560	559	oveq2d 7432	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
561		nn0uz 12911	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
562	247, 561	eleqtrdi 2875	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ (ℤ_≥‘0))
563	32	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑅 ∈ Ring)
564	563, 145	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (mulGrp‘𝑅) ∈ Mnd)
565	413	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝐻) ⊆ ℕ₀)
566	565	sselda 3938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑙 ∈ ℕ₀)
567	154	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝑁‘ 1 ) ∈ 𝐵)
568	143, 144, 564, 566, 567	mulgnn0cld 19184	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
569	23	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝐼 ∈ Fin)
570	18	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑅 ∈ CRing)
571	256, 569, 563, 566, 253	esplympl 33980	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
572	523, 571	eqeltrid 2869	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
573	259	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
574	251, 252, 253, 50, 569, 570, 572, 573	evlcl 22282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
575	50, 141, 563, 568, 574	ringcld 20362	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
576	108	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑀 ∈ Mnd)
577		fznn0sub 13596	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ (0...𝐻) → (𝐻 − 𝑙) ∈ ℕ₀)
578	577	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐻 − 𝑙) ∈ ℕ₀)
579	563, 34	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑋 ∈ (Base‘𝑊))
580	14, 71, 576, 578, 579	mulgnn0cld 19184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
581	19, 13, 50, 70, 563, 575, 580	ply1vscl 22570	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
582		oveq1 7423	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → (𝑙 ↑ (𝑁‘ 1 )) = (𝐻 ↑ (𝑁‘ 1 )))
583		2fveq3 6890	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝐻 → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘𝐻)))
584	583	fveq1d 6887	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘𝐻))‘𝑍))
585	582, 584	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐻 → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
586	585	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
587		oveq2 7424	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → (𝐻 − 𝑙) = (𝐻 − 𝐻))
588	293	subidd 11568	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻 − 𝐻) = 0)
589	587, 588	sylan9eqr 2822	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → (𝐻 − 𝑙) = 0)
590	589	oveq1d 7431	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = (0(._g‘𝑀)𝑋))
591	586, 590	oveq12d 7434	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = (((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
592	13, 189, 89, 562, 581, 591	gsummptfzsplitra 33401	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))))
593	91	nn0zd 12627	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐽) ∈ ℤ)
594		fzval3 13775	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐽) ∈ ℤ → (0...(♯‘𝐽)) = (0..^((♯‘𝐽) + 1)))
595	593, 594	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...(♯‘𝐽)) = (0..^((♯‘𝐽) + 1)))
596	296	oveq2d 7432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝐻) = (0..^((♯‘𝐽) + 1)))
597	595, 596	eqtr4d 2803	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...(♯‘𝐽)) = (0..^𝐻))
598	597	mpteq1d 5203	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
599	598	oveq2d 7432	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
600	91, 561	eleqtrdi 2875	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐽) ∈ (ℤ_≥‘0))
601	143, 144, 146, 103, 155	mulgnn0cld 19184	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
602	23	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝐼 ∈ Fin)
603	256, 602, 110, 103, 253	esplympl 33980	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
604	523, 603	eqeltrid 2869	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
605	259	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
606	251, 252, 253, 50, 602, 161, 604, 605	evlcl 22282	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
607	50, 141, 110, 601, 606	ringcld 20362	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
608	532	sselda 3938	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ (0...𝐻))
609	608, 535	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ (0...𝐻))
610	413, 609	sselid 3936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ ℕ₀)
611	14, 71, 109, 610, 111	mulgnn0cld 19184	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
612	19, 13, 50, 70, 110, 607, 611	ply1vscl 22570	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
613		oveq1 7423	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 0 → (𝑙 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
614	613	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝑙 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
615		2fveq3 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 0 → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘0)))
616	615	fveq1d 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 0 → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘0))‘𝑍))
617	616	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘0))‘𝑍))
618		eqid 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1_r‘(𝐼 mPoly 𝑅)) = (1_r‘(𝐼 mPoly 𝑅))
619	23, 32, 618	esplyfval0 33977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘0) = (1_r‘(𝐼 mPoly 𝑅)))
620	254	fveq1i 6886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐸‘0) = ((𝐼eSymPoly𝑅)‘0)
621	620	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘0) = ((𝐼eSymPoly𝑅)‘0))
622		eqid 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (algSc‘(𝐼 mPoly 𝑅)) = (algSc‘(𝐼 mPoly 𝑅))
623	252, 622, 277, 618, 23, 32	mplascl1 22205	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)) = (1_r‘(𝐼 mPoly 𝑅)))
624	619, 621, 623	3eqtr4d 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸‘0) = ((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))
625	624	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑄‘(𝐸‘0)) = (𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅))))
626	625	fveq1d 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘(𝐸‘0))‘𝑍) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍))
627	626	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘0))‘𝑍) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍))
628	251, 252, 50, 622, 23, 18, 242, 43	evlscaval 33953	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍) = (1_r‘𝑅))
629	628	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍) = (1_r‘𝑅))
630	617, 627, 629	3eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = (1_r‘𝑅))
631	614, 630	oveq12d 7434	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)))
632		oveq2 7424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 0 → (𝐻 − 𝑙) = (𝐻 − 0))
633	632	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 𝑙) = (𝐻 − 0))
634	293	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 = 0) → 𝐻 ∈ ℂ)
635	634	subid1d 11569	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 0) = 𝐻)
636	633, 635	eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 𝑙) = 𝐻)
637	636	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = (𝐻(._g‘𝑀)𝑋))
638	631, 637	oveq12d 7434	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 = 0) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))
639	13, 189, 89, 600, 612, 638	gsummptfzsplitla 33402	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))))
640		0p1e1 12372	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 1) = 1
641	640	oveq1i 7426	. . . . . . . . . . . . . . . 16 ⊢ ((0 + 1)...(♯‘𝐽)) = (1...(♯‘𝐽))
642	641	mpteq1i 5204	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))) = (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
643	642	oveq2i 7427	. . . . . . . . . . . . . 14 ⊢ (𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
644	643	oveq2i 7427	. . . . . . . . . . . . 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 20390	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ Abel)
647		fzfid 14022	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐽)) ∈ Fin)
648	540	ralrimiva 3159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑙 ∈ (1...(♯‘𝐽))(((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
649	13, 89, 647, 648	gsummptcl 20060	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) ∈ (Base‘𝑊))
650	13, 189, 646, 249, 649	ablcomd 33388	. . . . . . . . . . . 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 2804	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))))
652	599, 651	eqtr3d 2802	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))))
653	652	oveq1d 7431	. . . . . . . . 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 2801	. . . . . . . 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 19035	. . . . . . . 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 2807	. . . . . . 7 ⊢ (𝜑 → ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))))
657	32	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑅 ∈ Ring)
658	657, 145	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (mulGrp‘𝑅) ∈ Mnd)
659	565	sselda 3938	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑘 ∈ ℕ₀)
660	154	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝑁‘ 1 ) ∈ 𝐵)
661	143, 144, 658, 659, 660	mulgnn0cld 19184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
662	23	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝐼 ∈ Fin)
663	18	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑅 ∈ CRing)
664	254	fveq1i 6886	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑘) = ((𝐼eSymPoly𝑅)‘𝑘)
665	256, 662, 657, 659, 253	esplympl 33980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐼 mPoly 𝑅)))
666	664, 665	eqeltrid 2869	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐸‘𝑘) ∈ (Base‘(𝐼 mPoly 𝑅)))
667	259	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
668	251, 252, 253, 50, 662, 663, 666, 667	evlcl 22282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘𝑘))‘𝑍) ∈ 𝐵)
669	50, 141, 657, 661, 668	ringcld 20362	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ∈ 𝐵)
670	108	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑀 ∈ Mnd)
671		fznn0sub2 13675	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝐻) → (𝐻 − 𝑘) ∈ (0...𝐻))
672	671	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐻 − 𝑘) ∈ (0...𝐻))
673	413, 672	sselid 3936	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐻 − 𝑘) ∈ ℕ₀)
674	35	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑋 ∈ (Base‘𝑊))
675	14, 71, 670, 673, 674	mulgnn0cld 19184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
676	19, 13, 50, 70, 657, 669, 675	ply1vscl 22570	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
677		oveq1 7423	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐻 − 𝑙) → (𝑘 ↑ (𝑁‘ 1 )) = ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )))
678		2fveq3 6890	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐻 − 𝑙) → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘(𝐻 − 𝑙))))
679	678	fveq1d 6887	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐻 − 𝑙) → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))
680	677, 679	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝑘 = (𝐻 − 𝑙) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)))
681	680	adantl 487	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)))
682		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑘 = (𝐻 − 𝑙))
683	682	oveq2d 7432	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − 𝑘) = (𝐻 − (𝐻 − 𝑙)))
684	293	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝐻 ∈ ℂ)
685	566	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑙 ∈ ℕ₀)
686	685	nn0cnd 12578	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑙 ∈ ℂ)
687	684, 686	nncand 11585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − (𝐻 − 𝑙)) = 𝑙)
688	683, 687	eqtrd 2800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − 𝑘) = 𝑙)
689	688	oveq1d 7431	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) = (𝑙(._g‘𝑀)𝑋))
690	681, 689	oveq12d 7434	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) = ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))
691	13, 89, 247, 676, 690	gsummptrev 33399	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
692	550, 656, 691	3eqtrd 2804	. . . . . 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 2808	. . . . 5 ⊢ (𝜑 → ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
694	69, 188, 693	3eqtrd 2804	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
695	694	fveq2d 6889	. . 3 ⊢ (𝜑 → (coe₁‘𝐹) = (coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))))
696	695	fveq1d 6887	. 2 ⊢ (𝜑 → ((coe₁‘𝐹)‘𝐾) = ((coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))‘𝐾))
697	12	fveq2i 6888	. . 3 ⊢ (._g‘𝑀) = (._g‘(mulGrp‘𝑊))
698	143, 144, 564, 578, 567	mulgnn0cld 19184	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) ∈ 𝐵)
699	254	fveq1i 6886	. . . . . . 7 ⊢ (𝐸‘(𝐻 − 𝑙)) = ((𝐼eSymPoly𝑅)‘(𝐻 − 𝑙))
700	256, 569, 563, 578, 253	esplympl 33980	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘(𝐻 − 𝑙)) ∈ (Base‘(𝐼 mPoly 𝑅)))
701	699, 700	eqeltrid 2869	. . . . . 6 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐸‘(𝐻 − 𝑙)) ∈ (Base‘(𝐼 mPoly 𝑅)))
702	251, 252, 253, 50, 569, 570, 701, 573	evlcl 22282	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍) ∈ 𝐵)
703	50, 141, 563, 698, 702	ringcld 20362	. . . 4 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) ∈ 𝐵)
704	703	ralrimiva 3159	. . 3 ⊢ (𝜑 → ∀𝑙 ∈ (0...𝐻)(((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) ∈ 𝐵)
705		vieta.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
706		oveq2 7424	. . . . 5 ⊢ (𝑙 = 𝐾 → (𝐻 − 𝑙) = (𝐻 − 𝐾))
707	706	oveq1d 7431	. . . 4 ⊢ (𝑙 = 𝐾 → ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) = ((𝐻 − 𝐾) ↑ (𝑁‘ 1 )))
708	706	fveq2d 6889	. . . . . 6 ⊢ (𝑙 = 𝐾 → (𝐸‘(𝐻 − 𝑙)) = (𝐸‘(𝐻 − 𝐾)))
709	708	fveq2d 6889	. . . . 5 ⊢ (𝑙 = 𝐾 → (𝑄‘(𝐸‘(𝐻 − 𝑙))) = (𝑄‘(𝐸‘(𝐻 − 𝐾))))
710	709	fveq1d 6887	. . . 4 ⊢ (𝑙 = 𝐾 → ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍) = ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍))
711	707, 710	oveq12d 7434	. . 3 ⊢ (𝑙 = 𝐾 → (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))
712	19, 13, 33, 697, 32, 50, 70, 247, 704, 705, 711	gsummoncoe1fz 33911	. 2 ⊢ (𝜑 → ((coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))
713	696, 712	eqtrd 2800	1 ⊢ (𝜑 → ((coe₁‘𝐹)‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ∀wral 3081 {crab 3418 Vcvv 3457 ∖ cdif 3903 ∪ cun 3904 ⊆ wss 3906 {csn 4591 class class class wbr 5111 ↦ cmpt 5194 ↾ cres 5665 ⟶wf 6536 ‘cfv 6540 (class class class)co 7416 ↑_m cmap 8826 Fincfn 8945 finSupp cfsupp 9324 ℂcc 11109 0cc0 11111 1c1 11112 + caddc 11114 − cmin 11452 ℕ₀cn0 12515 ℤcz 12602 ℤ_≥cuz 12873 ...cfz 13546 ..^cfzo 13694 ♯chash 14379 Basecbs 17286 +_gcplusg 17327 ._rcmulr 17328 Scalarcsca 17330 ·_𝑠 cvsca 17331 Σ_g cgsu 17510 Mndcmnd 18813 Grpcgrp 19023 inv_gcminusg 19024 -_gcsg 19025 ._gcmg 19156 CMndccmn 19873 Abelcabl 19874 mulGrpcmgp 20239 1_rcur 20286 Ringcrg 20338 CRingccrg 20339 IDomncidom 20821 LModclmod 21010 AssAlgcasa 22029 algSccascl 22031 mPoly cmpl 22085 eval cevl 22253 var₁cv1 22365 Poly₁cpl1 22366 coe₁cco1 22367 deg₁cdg1 26240 eSymPolycesply 33969

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-pre-sup 11189 ax-addf 11190 ax-mulf 11191

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7680 df-ofr 7681 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8159 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-oadd 8459 df-er 8696 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9325 df-sup 9405 df-oi 9475 df-dju 9899 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-div 11883 df-ind 12230 df-nn 12245 df-2 12314 df-3 12315 df-4 12316 df-5 12317 df-6 12318 df-7 12319 df-8 12320 df-9 12321 df-n0 12516 df-xnn0 12589 df-z 12603 df-dec 12723 df-uz 12874 df-rp 13028 df-fz 13547 df-fzo 13695 df-seq 14051 df-fac 14323 df-bc 14352 df-hash 14380 df-struct 17224 df-sets 17241 df-slot 17259 df-ndx 17271 df-base 17287 df-ress 17308 df-plusg 17340 df-mulr 17341 df-starv 17342 df-sca 17343 df-vsca 17344 df-ip 17345 df-tset 17346 df-ple 17347 df-ds 17349 df-unif 17350 df-hom 17351 df-cco 17352 df-0g 17511 df-gsum 17512 df-prds 17517 df-pws 17519 df-mre 17655 df-mrc 17656 df-acs 17658 df-mgm 18715 df-sgrp 18798 df-mnd 18814 df-mhm 18864 df-submnd 18865 df-grp 19026 df-minusg 19027 df-sbg 19028 df-mulg 19157 df-subg 19212 df-ghm 19307 df-cntz 19410 df-cmn 19875 df-abl 19876 df-mgp 20240 df-rng 20254 df-ur 20287 df-srg 20292 df-ring 20340 df-cring 20341 df-rhm 20579 df-subrng 20674 df-subrg 20698 df-idom 20824 df-lmod 21012 df-lss 21082 df-lsp 21122 df-cnfld 21552 df-zring 21626 df-zrh 21682 df-assa 22032 df-asp 22033 df-ascl 22034 df-psr 22088 df-mvr 22089 df-mpl 22090 df-opsr 22092 df-evls 22254 df-evl 22255 df-psr1 22369 df-vr1 22370 df-ply1 22371 df-coe1 22372 df-mdeg 26241 df-deg1 26242 df-extv 33943 df-esply 33971

This theorem is used by: vieta 33993

W3C validator