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 33836

Description: Lemma for vieta 33837: 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 4115	. . . . . . . . 9 ⊢ (𝐽 ∪ {𝑌}) = ((𝐼 ∖ {𝑌}) ∪ {𝑌})
5		vietalem.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ 𝐼)
6	5	snssd 4742	. . . . . . . . . 10 ⊢ (𝜑 → {𝑌} ⊆ 𝐼)
7		undifr 4434	. . . . . . . . . 10 ⊢ ({𝑌} ⊆ 𝐼 ↔ ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
8	6, 7	sylib 220	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼 ∖ {𝑌}) ∪ {𝑌}) = 𝐼)
9	4, 8	eqtr2id 2809	. . . . . . . 8 ⊢ (𝜑 → 𝐼 = (𝐽 ∪ {𝑌}))
10	9	mpteq1d 5187	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))) = (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
11	10	oveq2d 7406	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐼 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
12		vieta.m	. . . . . . . 8 ⊢ 𝑀 = (mulGrp‘𝑊)
13		eqid 2761	. . . . . . . 8 ⊢ (Base‘𝑊) = (Base‘𝑊)
14	12, 13	mgpbas 20181	. . . . . . 7 ⊢ (Base‘𝑊) = (Base‘𝑀)
15		eqid 2761	. . . . . . . 8 ⊢ (._r‘𝑊) = (._r‘𝑊)
16	12, 15	mgpplusg 20180	. . . . . . 7 ⊢ (._r‘𝑊) = (+_g‘𝑀)
17		vieta.r	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ IDomn)
18	17	idomcringd 20763	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CRing)
19		vieta.w	. . . . . . . . 9 ⊢ 𝑊 = (Poly₁‘𝑅)
20	19	ply1crng 22247	. . . . . . . 8 ⊢ (𝑅 ∈ CRing → 𝑊 ∈ CRing)
21	12	crngmgp 20277	. . . . . . . 8 ⊢ (𝑊 ∈ CRing → 𝑀 ∈ CMnd)
22	18, 20, 21	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ CMnd)
23		vieta.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ Fin)
24		diffi 9136	. . . . . . . . 9 ⊢ (𝐼 ∈ Fin → (𝐼 ∖ {𝑌}) ∈ Fin)
25	23, 24	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐼 ∖ {𝑌}) ∈ Fin)
26	3, 25	eqeltrid 2865	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Fin)
27		vieta.3	. . . . . . . 8 ⊢ − = (-_g‘𝑊)
28	18, 20	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ CRing)
29	28	crngringd 20282	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ Ring)
30	29	ringgrpd 20278	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Grp)
31	30	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑊 ∈ Grp)
32	17	idomringd 20764	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Ring)
33		vieta.x	. . . . . . . . . . 11 ⊢ 𝑋 = (var₁‘𝑅)
34	33, 19, 13	vr1cl 22266	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑊))
35	32, 34	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑊))
36	35	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑋 ∈ (Base‘𝑊))
37		vieta.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑊)
38		eqid 2761	. . . . . . . . 9 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
39		eqid 2761	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
40	19	ply1assa 22248	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → 𝑊 ∈ AssAlg)
41	18, 40	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ AssAlg)
42	41	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑊 ∈ AssAlg)
43		vieta.z	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍:𝐼⟶𝐵)
44	43	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑍:𝐼⟶𝐵)
45		difss 4087	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∖ {𝑌}) ⊆ 𝐼
46	3, 45	eqsstri 3980	. . . . . . . . . . . . 13 ⊢ 𝐽 ⊆ 𝐼
47	46	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
48	47	sselda 3934	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑛 ∈ 𝐼)
49	44, 48	ffvelcdmd 7060	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑍‘𝑛) ∈ 𝐵)
50		vieta.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑅)
51	19	ply1sca 22301	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑊))
52	18, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑊))
53	52	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑊)))
54	50, 53	eqtrid 2808	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = (Base‘(Scalar‘𝑊)))
55	54	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝐵 = (Base‘(Scalar‘𝑊)))
56	49, 55	eleqtrd 2863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑍‘𝑛) ∈ (Base‘(Scalar‘𝑊)))
57	37, 38, 39, 42, 56	asclelbas 21922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝐴‘(𝑍‘𝑛)) ∈ (Base‘𝑊))
58	13, 27, 31, 36, 57	grpsubcld 33180	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑋 − (𝐴‘(𝑍‘𝑛))) ∈ (Base‘𝑊))
59		neldifsnd 4750	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝐼 ∖ {𝑌}))
60	3	eleq2i 2853	. . . . . . . 8 ⊢ (𝑌 ∈ 𝐽 ↔ 𝑌 ∈ (𝐼 ∖ {𝑌}))
61	59, 60	sylnibr 331	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐽)
62	54, 43	feq3dd 6672	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍:𝐼⟶(Base‘(Scalar‘𝑊)))
63	62, 5	ffvelcdmd 7060	. . . . . . . . 9 ⊢ (𝜑 → (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)))
64	37, 38, 39, 41, 63	asclelbas 21922	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘(𝑍‘𝑌)) ∈ (Base‘𝑊))
65	13, 27, 30, 35, 64	grpsubcld 33180	. . . . . . 7 ⊢ (𝜑 → (𝑋 − (𝐴‘(𝑍‘𝑌))) ∈ (Base‘𝑊))
66		2fveq3 6866	. . . . . . . 8 ⊢ (𝑛 = 𝑌 → (𝐴‘(𝑍‘𝑛)) = (𝐴‘(𝑍‘𝑌)))
67	66	oveq2d 7406	. . . . . . 7 ⊢ (𝑛 = 𝑌 → (𝑋 − (𝐴‘(𝑍‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑌))))
68	14, 16, 22, 26, 58, 5, 61, 65, 67	gsumunsn 19990	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ (𝐽 ∪ {𝑌}) ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
69	2, 11, 68	3eqtrd 2800	. . . . 5 ⊢ (𝜑 → 𝐹 = ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
70		eqid 2761	. . . . . . . . 9 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
71		eqid 2761	. . . . . . . . 9 ⊢ (._g‘𝑀) = (._g‘𝑀)
72		eqid 2761	. . . . . . . . 9 ⊢ (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
73		eqid 2761	. . . . . . . . 9 ⊢ ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
74		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → 𝑛 ∈ 𝐽)
75	74	fvresd 6881	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → ((𝑍 ↾ 𝐽)‘𝑛) = (𝑍‘𝑛))
76	75	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)) = (𝐴‘(𝑍‘𝑛)))
77	76	oveq2d 7406	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐽) → (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))) = (𝑋 − (𝐴‘(𝑍‘𝑛))))
78	77	mpteq2dva 5190	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))) = (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))
79	78	oveq2d 7406	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))))
80	58	ralrimiva 3153	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ 𝐽 (𝑋 − (𝐴‘(𝑍‘𝑛))) ∈ (Base‘𝑊))
81	14, 22, 26, 80	gsummptcl 19997	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) ∈ (Base‘𝑊))
82	79, 81	eqeltrd 2861	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘𝑊))
83	19, 33, 13, 70, 12, 71, 72, 73, 32, 82	ply1coedeg 33745	. . . . . . . 8 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
84		vietalem.3	. . . . . . . . . . 11 ⊢ (𝜑 → ((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))) = (♯‘𝐽))
85	84	oveq2d 7406	. . . . . . . . . 10 ⊢ (𝜑 → (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) = (0...(♯‘𝐽)))
86	85	mpteq1d 5187	. . . . . . . . 9 ⊢ (𝜑 → (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))
87	86	oveq2d 7406	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...((deg₁‘𝑅)‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
88	83, 79, 87	3eqtr3d 2804	. . . . . . 7 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
89	29	ringcmnd 20320	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ CMnd)
90		hashcl 14362	. . . . . . . . 9 ⊢ (𝐽 ∈ Fin → (♯‘𝐽) ∈ ℕ₀)
91	26, 90	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐽) ∈ ℕ₀)
92	19	ply1lmod 22300	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑊 ∈ LMod)
93	32, 92	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ LMod)
94	93	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑊 ∈ LMod)
95	82	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘𝑊))
96	52	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Poly₁‘𝑅) = (Poly₁‘(Scalar‘𝑊)))
97	19, 96	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 = (Poly₁‘(Scalar‘𝑊)))
98	97	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘𝑊) = (Base‘(Poly₁‘(Scalar‘𝑊))))
99	98	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (Base‘𝑊) = (Base‘(Poly₁‘(Scalar‘𝑊))))
100	95, 99	eleqtrd 2863	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘(Poly₁‘(Scalar‘𝑊))))
101		fz0ssnn0 13620	. . . . . . . . . . 11 ⊢ (0...(♯‘𝐽)) ⊆ ℕ₀
102		simpr 488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ (0...(♯‘𝐽)))
103	101, 102	sselid 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ ℕ₀)
104		eqid 2761	. . . . . . . . . . 11 ⊢ (Base‘(Poly₁‘(Scalar‘𝑊))) = (Base‘(Poly₁‘(Scalar‘𝑊)))
105		eqid 2761	. . . . . . . . . . 11 ⊢ (Poly₁‘(Scalar‘𝑊)) = (Poly₁‘(Scalar‘𝑊))
106	72, 104, 105, 39	coe1fvalcl 22261	. . . . . . . . . 10 ⊢ (((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))) ∈ (Base‘(Poly₁‘(Scalar‘𝑊))) ∧ 𝑙 ∈ ℕ₀) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) ∈ (Base‘(Scalar‘𝑊)))
107	100, 103, 106	syl2anc 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) ∈ (Base‘(Scalar‘𝑊)))
108	22	cmnmndd 19834	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ Mnd)
109	108	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
110	32	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
111	110, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
112	14, 71, 109, 103, 111	mulgnn0cld 19127	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑙(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
113	13, 38, 70, 39, 94, 107, 112	lmodvscld 20933	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
114		simpr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑙 = ((♯‘𝐽) − 𝑘))
115	114	fveq2d 6865	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙) = ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)))
116		oveq1 7397	. . . . . . . . . 10 ⊢ (𝑙 = ((♯‘𝐽) − 𝑘) → (𝑙(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
117	116	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (𝑙(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
118	115, 117	oveq12d 7408	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) = (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
119	13, 89, 91, 113, 118	gsummptrev 33196	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘𝑙)( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
120		fveq1 6860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑧‘𝑛) = ((𝑍 ↾ 𝐽)‘𝑛))
121	120	fveq2d 6865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝐴‘(𝑧‘𝑛)) = (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))
122	121	oveq2d 7406	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑋 − (𝐴‘(𝑧‘𝑛))) = (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))
123	122	mpteq2dv 5191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))) = (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))
124	123	oveq2d 7406	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))) = (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))
125	124	fveq2d 6865	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛)))))) = (coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛)))))))
126	125	fveq1d 6863	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)))
127		fveq2 6861	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
128	127	oveq2d 7406	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
129	126, 128	eqeq12d 2777	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (𝑍 ↾ 𝐽) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑧‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘𝑧)) ↔ ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
130	129	ralbidv 3184	. . . . . . . . . . . . 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 6875	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
133	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ V)
134	43, 47	fssresd 6725	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍 ↾ 𝐽):𝐽⟶𝐵)
135	133, 26, 134	elmapdd 8815	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
136	130, 131, 135	rspcdva 3581	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐽))((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
137	136	r19.21bi 3253	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘)) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
138	137	oveq1d 7405	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
139	138	mpteq2dva 5190	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))) = (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
140	139	oveq2d 7406	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
141		vieta.t	. . . . . . . . . . 11 ⊢ · = (._r‘𝑅)
142		eqid 2761	. . . . . . . . . . . . 13 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
143	142, 50	mgpbas 20181	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘(mulGrp‘𝑅))
144		vieta.p	. . . . . . . . . . . 12 ⊢ ↑ = (._g‘(mulGrp‘𝑅))
145	142	ringmgp 20275	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → (mulGrp‘𝑅) ∈ Mnd)
146	110, 145	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
147		fznn0sub2 13633	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑙) ∈ (0...(♯‘𝐽)))
148	147	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑙) ∈ (0...(♯‘𝐽)))
149	101, 148	sselid 3932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑙) ∈ ℕ₀)
150		vieta.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (inv_g‘𝑅)
151	32	ringgrpd 20278	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Grp)
152		vieta.1	. . . . . . . . . . . . . . 15 ⊢ 1 = (1_r‘𝑅)
153	50, 152, 32	ringidcld 20302	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ∈ 𝐵)
154	50, 150, 151, 153	grpinvcld 19020	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁‘ 1 ) ∈ 𝐵)
155	154	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
156	143, 144, 146, 149, 155	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) ∈ 𝐵)
157		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝐽 eval 𝑅) = (𝐽 eval 𝑅)
158		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝐽 mPoly 𝑅) = (𝐽 mPoly 𝑅)
159		eqid 2761	. . . . . . . . . . . 12 ⊢ (Base‘(𝐽 mPoly 𝑅)) = (Base‘(𝐽 mPoly 𝑅))
160	26	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
161	18	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
162		eqid 2761	. . . . . . . . . . . . 13 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐽) ∣ ℎ finSupp 0}
163	162, 160, 110, 149, 159	esplympl 33824	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)) ∈ (Base‘(𝐽 mPoly 𝑅)))
164	135	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
165	157, 158, 159, 50, 160, 161, 163, 164	evlcl 22142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
166	50, 141, 110, 156, 165	ringcld 20296	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
167	19, 13, 50, 70, 110, 166, 112	ply1vscl 22431	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
168	91	nn0cnd 12537	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘𝐽) ∈ ℂ)
169	168	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (♯‘𝐽) ∈ ℂ)
170		simplr 778	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ (0...(♯‘𝐽)))
171	101, 170	sselid 3932	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ ℕ₀)
172	171	nn0cnd 12537	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑘 ∈ ℂ)
173	169, 172	subcld 11535	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑘) ∈ ℂ)
174	114, 173	eqeltrd 2861	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → 𝑙 ∈ ℂ)
175	169, 174	subcld 11535	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑙) ∈ ℂ)
176	169, 174	nncand 11540	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = 𝑙)
177	176, 114	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = ((♯‘𝐽) − 𝑘))
178	169, 175, 172, 177	subcand 11576	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((♯‘𝐽) − 𝑙) = 𝑘)
179	178	oveq1d 7405	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
180	178	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)) = ((𝐽eSymPoly𝑅)‘𝑘))
181	180	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙))) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)))
182	181	fveq1d 6863	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
183	179, 182	oveq12d 7408	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
184	183, 117	oveq12d 7408	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) ∧ 𝑙 = ((♯‘𝐽) − 𝑘)) → (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
185	13, 89, 91, 167, 184	gsummptrev 33196	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))))
186	140, 185	eqtr4d 2799	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((coe₁‘(𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘((𝑍 ↾ 𝐽)‘𝑛))))))‘((♯‘𝐽) − 𝑘))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
187	88, 119, 186	3eqtrd 2800	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛))))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
188	187	oveq1d 7405	. . . . 5 ⊢ (𝜑 → ((𝑀 Σ_g (𝑛 ∈ 𝐽 ↦ (𝑋 − (𝐴‘(𝑍‘𝑛)))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
189		eqid 2761	. . . . . . 7 ⊢ (+_g‘𝑊) = (+_g‘𝑊)
190	32	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
191	190, 145	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
192		elfznn0 13618	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...(♯‘𝐽)) → 𝑖 ∈ ℕ₀)
193	192	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑖 ∈ ℕ₀)
194	154	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
195	143, 144, 191, 193, 194	mulgnn0cld 19127	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑖 ↑ (𝑁‘ 1 )) ∈ 𝐵)
196	26	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
197	18	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
198	162, 196, 190, 193, 159	esplympl 33824	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑖) ∈ (Base‘(𝐽 mPoly 𝑅)))
199	135	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
200	157, 158, 159, 50, 196, 197, 198, 199	evlcl 22142	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
201	50, 141, 190, 195, 200	ringcld 20296	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
202	108	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
203		fznn0sub2 13633	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑖) ∈ (0...(♯‘𝐽)))
204	203	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑖) ∈ (0...(♯‘𝐽)))
205	101, 204	sselid 3932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑖) ∈ ℕ₀)
206	35	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
207	14, 71, 202, 205, 206	mulgnn0cld 19127	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
208	19, 13, 50, 70, 190, 201, 207	ply1vscl 22431	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(♯‘𝐽))) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
209		oveq1 7397	. . . . . . . . 9 ⊢ (𝑖 = 0 → (𝑖 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
210		2fveq3 6866	. . . . . . . . . 10 ⊢ (𝑖 = 0 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)))
211	210	fveq1d 6863	. . . . . . . . 9 ⊢ (𝑖 = 0 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))
212	209, 211	oveq12d 7408	. . . . . . . 8 ⊢ (𝑖 = 0 → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))))
213		oveq2 7398	. . . . . . . . 9 ⊢ (𝑖 = 0 → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − 0))
214	213	oveq1d 7405	. . . . . . . 8 ⊢ (𝑖 = 0 → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − 0)(._g‘𝑀)𝑋))
215	212, 214	oveq12d 7408	. . . . . . 7 ⊢ (𝑖 = 0 → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋)))
216		oveq1 7397	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → (𝑖 ↑ (𝑁‘ 1 )) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
217		2fveq3 6866	. . . . . . . . . 10 ⊢ (𝑖 = (♯‘𝐽) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽))))
218	217	fveq1d 6863	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))
219	216, 218	oveq12d 7408	. . . . . . . 8 ⊢ (𝑖 = (♯‘𝐽) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))
220		oveq2 7398	. . . . . . . . 9 ⊢ (𝑖 = (♯‘𝐽) → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − (♯‘𝐽)))
221	220	oveq1d 7405	. . . . . . . 8 ⊢ (𝑖 = (♯‘𝐽) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))
222	219, 221	oveq12d 7408	. . . . . . 7 ⊢ (𝑖 = (♯‘𝐽) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)))
223		oveq1 7397	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (𝑖 ↑ (𝑁‘ 1 )) = (𝑘 ↑ (𝑁‘ 1 )))
224		2fveq3 6866	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)))
225	224	fveq1d 6863	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))
226	223, 225	oveq12d 7408	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))
227		oveq2 7398	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − 𝑘))
228	227	oveq1d 7405	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
229	226, 228	oveq12d 7408	. . . . . . 7 ⊢ (𝑖 = 𝑘 → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
230		oveq1 7397	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → (𝑖 ↑ (𝑁‘ 1 )) = ((𝑘 + 1) ↑ (𝑁‘ 1 )))
231		2fveq3 6866	. . . . . . . . . 10 ⊢ (𝑖 = (𝑘 + 1) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1))))
232	231	fveq1d 6863	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))
233	230, 232	oveq12d 7408	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → ((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽))) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
234		oveq2 7398	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 + 1) → ((♯‘𝐽) − 𝑖) = ((♯‘𝐽) − (𝑘 + 1)))
235	234	oveq1d 7405	. . . . . . . 8 ⊢ (𝑖 = (𝑘 + 1) → (((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋) = (((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))
236	233, 235	oveq12d 7408	. . . . . . 7 ⊢ (𝑖 = (𝑘 + 1) → (((𝑖 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑖))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑖)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)))
237		eqid 2761	. . . . . . . . 9 ⊢ (inv_g‘𝑊) = (inv_g‘𝑊)
238	32, 145	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd)
239		0nn0 12489	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ₀
240	239	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℕ₀)
241	143, 144, 238, 240, 154	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ (𝜑 → (0 ↑ (𝑁‘ 1 )) ∈ 𝐵)
242	152, 153	eqeltrrid 2866	. . . . . . . . . . 11 ⊢ (𝜑 → (1_r‘𝑅) ∈ 𝐵)
243	50, 141, 32, 241, 242	ringcld 20296	. . . . . . . . . 10 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)) ∈ 𝐵)
244		vieta.h	. . . . . . . . . . . 12 ⊢ 𝐻 = (♯‘𝐼)
245		hashcl 14362	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ Fin → (♯‘𝐼) ∈ ℕ₀)
246	23, 245	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐼) ∈ ℕ₀)
247	244, 246	eqeltrid 2865	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ ℕ₀)
248	14, 71, 108, 247, 35	mulgnn0cld 19127	. . . . . . . . . 10 ⊢ (𝜑 → (𝐻(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
249	19, 13, 50, 70, 32, 243, 248	ply1vscl 22431	. . . . . . . . 9 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
250	143, 144, 238, 247, 154	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) ∈ 𝐵)
251		vieta.q	. . . . . . . . . . . 12 ⊢ 𝑄 = (𝐼 eval 𝑅)
252		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝐼 mPoly 𝑅) = (𝐼 mPoly 𝑅)
253		eqid 2761	. . . . . . . . . . . 12 ⊢ (Base‘(𝐼 mPoly 𝑅)) = (Base‘(𝐼 mPoly 𝑅))
254		vieta.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝐼eSymPoly𝑅)
255	254	fveq1i 6862	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐻) = ((𝐼eSymPoly𝑅)‘𝐻)
256		eqid 2761	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ₀ ↑_m 𝐼) ∣ ℎ finSupp 0}
257	256, 23, 32, 247, 253	esplympl 33824	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘𝐻) ∈ (Base‘(𝐼 mPoly 𝑅)))
258	255, 257	eqeltrid 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝐻) ∈ (Base‘(𝐼 mPoly 𝑅)))
259	133, 23, 43	elmapdd 8815	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑_m 𝐼))
260	251, 252, 253, 50, 23, 18, 258, 259	evlcl 22142	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄‘(𝐸‘𝐻))‘𝑍) ∈ 𝐵)
261	50, 141, 32, 250, 260	ringcld 20296	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) ∈ 𝐵)
262	14, 71, 108, 240, 35	mulgnn0cld 19127	. . . . . . . . . 10 ⊢ (𝜑 → (0(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
263	19, 13, 50, 70, 32, 261, 262	ply1vscl 22431	. . . . . . . . 9 ⊢ (𝜑 → (((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
264	13, 189, 27, 237, 30, 249, 263	grpsubinv 19044	. . . . . . . 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 33824	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘0) ∈ (Base‘(𝐽 mPoly 𝑅)))
266	157, 158, 159, 50, 26, 18, 265, 135	evlcl 22142	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
267	50, 141, 32, 241, 266	ringcld 20296	. . . . . . . . . . . 12 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
268	267, 54	eleqtrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
269	168	subid1d 11524	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − 0) = (♯‘𝐽))
270	269, 91	eqeltrd 2861	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐽) − 0) ∈ ℕ₀)
271	14, 71, 108, 270, 35	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ (𝜑 → (((♯‘𝐽) − 0)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
272	13, 38, 39, 70, 15, 41, 268, 271, 35	assaassd 33711	. . . . . . . . . 10 ⊢ (𝜑 → ((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) = (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
273		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘(𝐽 mPoly 𝑅)) = (1_r‘(𝐽 mPoly 𝑅))
274	26, 32, 273	esplyfval0 33821	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘0) = (1_r‘(𝐽 mPoly 𝑅)))
275	274	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)) = ((𝐽 eval 𝑅)‘(1_r‘(𝐽 mPoly 𝑅))))
276		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (algSc‘(𝐽 mPoly 𝑅)) = (algSc‘(𝐽 mPoly 𝑅))
277		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
278	158, 276, 277, 273, 26, 32	mplascl1 22065	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)) = (1_r‘(𝐽 mPoly 𝑅)))
279	278	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅))) = ((𝐽 eval 𝑅)‘(1_r‘(𝐽 mPoly 𝑅))))
280	275, 279	eqtr4d 2799	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0)) = ((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅))))
281	280	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)))‘(𝑍 ↾ 𝐽)))
282	157, 158, 50, 276, 26, 18, 242, 134	evlscaval 33797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((algSc‘(𝐽 mPoly 𝑅))‘(1_r‘𝑅)))‘(𝑍 ↾ 𝐽)) = (1_r‘𝑅))
283	281, 282	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)) = (1_r‘𝑅))
284	283	oveq2d 7406	. . . . . . . . . . 11 ⊢ (𝜑 → ((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽))) = ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)))
285	14, 71, 16	mulgnn0p1 19117	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ Mnd ∧ (♯‘𝐽) ∈ ℕ₀ ∧ 𝑋 ∈ (Base‘𝑊)) → (((♯‘𝐽) + 1)(._g‘𝑀)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
286	108, 91, 35, 285	syl3anc 1389	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) + 1)(._g‘𝑀)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
287		hashdifsn 14420	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ Fin ∧ 𝑌 ∈ 𝐼) → (♯‘(𝐼 ∖ {𝑌})) = ((♯‘𝐼) − 1))
288	23, 5, 287	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (♯‘(𝐼 ∖ {𝑌})) = ((♯‘𝐼) − 1))
289	3	fveq2i 6864	. . . . . . . . . . . . . . . 16 ⊢ (♯‘𝐽) = (♯‘(𝐼 ∖ {𝑌}))
290	244	oveq1i 7400	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 − 1) = ((♯‘𝐼) − 1)
291	288, 289, 290	3eqtr4g 2821	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐽) = (𝐻 − 1))
292	291	oveq1d 7405	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((♯‘𝐽) + 1) = ((𝐻 − 1) + 1))
293	247	nn0cnd 12537	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 ∈ ℂ)
294		1cnd 11168	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℂ)
295	293, 294	npcand 11539	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐻 − 1) + 1) = 𝐻)
296	292, 295	eqtr2d 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐻 = ((♯‘𝐽) + 1))
297	296	oveq1d 7405	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐻(._g‘𝑀)𝑋) = (((♯‘𝐽) + 1)(._g‘𝑀)𝑋))
298	269	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐽) − 0)(._g‘𝑀)𝑋) = ((♯‘𝐽)(._g‘𝑀)𝑋))
299	298	oveq1d 7405	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋) = (((♯‘𝐽)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
300	286, 297, 299	3eqtr4rd 2807	. . . . . . . . . . 11 ⊢ (𝜑 → ((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋) = (𝐻(._g‘𝑀)𝑋))
301	284, 300	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − 0)(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))
302	272, 301	eqtr2d 2797	. . . . . . . . 9 ⊢ (𝜑 → (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)) = ((((0 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘0))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 0)(._g‘𝑀)𝑋))(._r‘𝑊)𝑋))
303	52	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (._r‘𝑅) = (._r‘(Scalar‘𝑊)))
304	141, 303	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ (𝜑 → · = (._r‘(Scalar‘𝑊)))
305	304	oveqd 7407	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
306	305	oveq1d 7405	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)))
307	43, 5	ffvelcdmd 7060	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑍‘𝑌) ∈ 𝐵)
308	143, 144, 238, 91, 154	mulgnn0cld 19127	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝐽) ↑ (𝑁‘ 1 )) ∈ 𝐵)
309	162, 26, 32, 91, 159	esplympl 33824	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐽eSymPoly𝑅)‘(♯‘𝐽)) ∈ (Base‘(𝐽 mPoly 𝑅)))
310	157, 158, 159, 50, 26, 18, 309, 135	evlcl 22142	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
311	50, 141, 18, 307, 308, 310	crng12d 20294	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
312	296	oveq1d 7405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) = (((♯‘𝐽) + 1) ↑ (𝑁‘ 1 )))
313	152, 150, 144, 32, 91	ringm1expp1 33374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((♯‘𝐽) + 1) ↑ (𝑁‘ 1 )) = (𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 ))))
314	312, 313	eqtrd 2796	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐻 ↑ (𝑁‘ 1 )) = (𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 ))))
315	314	fveq2d 6865	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) = (𝑁‘(𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 )))))
316	50, 150, 151, 308	grpinvinvd 33179	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁‘(𝑁‘((♯‘𝐽) ↑ (𝑁‘ 1 )))) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
317	315, 316	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) = ((♯‘𝐽) ↑ (𝑁‘ 1 )))
318		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
319		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (𝐽eSymPoly𝑅) = (𝐽eSymPoly𝑅)
320		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (♯‘𝐽) = (♯‘𝐽)
321	50, 318, 141, 251, 157, 254, 319, 244, 320, 3, 23, 18, 5, 43	esplyfvn 33834	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄‘(𝐸‘𝐻))‘𝑍) = ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))
322	317, 321	oveq12d 7408	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) = (((♯‘𝐽) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))))
323	311, 322	eqtr4d 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
324	50, 141, 150, 32, 250, 260	ringmneg1 20340	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑁‘(𝐻 ↑ (𝑁‘ 1 ))) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) = (𝑁‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
325	52	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (inv_g‘𝑅) = (inv_g‘(Scalar‘𝑊)))
326	150, 325	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 = (inv_g‘(Scalar‘𝑊)))
327	326	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))) = ((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
328	323, 324, 327	3eqtrd 2800	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))) = ((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))))
329	168	subidd 11523	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − (♯‘𝐽)) = 0)
330	329	oveq1d 7405	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋) = (0(._g‘𝑀)𝑋))
331	328, 330	oveq12d 7408	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌) · (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
332	50, 141, 32, 308, 310	ringcld 20296	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
333	332, 54	eleqtrd 2863	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
334	329, 240	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((♯‘𝐽) − (♯‘𝐽)) ∈ ℕ₀)
335	14, 71, 108, 334, 35	mulgnn0cld 19127	. . . . . . . . . . . 12 ⊢ (𝜑 → (((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
336		eqid 2761	. . . . . . . . . . . . 13 ⊢ (._r‘(Scalar‘𝑊)) = (._r‘(Scalar‘𝑊))
337	13, 38, 70, 39, 336	lmodvsass 20941	. . . . . . . . . . . 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 1390	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))(((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
339	306, 331, 338	3eqtr3d 2804	. . . . . . . . . 10 ⊢ (𝜑 → (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
340		eqid 2761	. . . . . . . . . . 11 ⊢ (inv_g‘(Scalar‘𝑊)) = (inv_g‘(Scalar‘𝑊))
341	261, 54	eleqtrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)) ∈ (Base‘(Scalar‘𝑊)))
342	13, 38, 70, 237, 39, 340, 93, 262, 341	lmodvsneg 20960	. . . . . . . . . 10 ⊢ (𝜑 → ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((inv_g‘(Scalar‘𝑊))‘((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
343	19, 13, 50, 70, 32, 332, 335	ply1vscl 22431	. . . . . . . . . . 11 ⊢ (𝜑 → ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
344	37, 38, 39, 13, 15, 70	asclmul2 21926	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ AssAlg ∧ (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ ((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋)) ∈ (Base‘𝑊)) → (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
345	41, 63, 343, 344	syl3anc 1389	. . . . . . . . . 10 ⊢ (𝜑 → (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))))
346	339, 342, 345	3eqtr4d 2806	. . . . . . . . 9 ⊢ (𝜑 → ((inv_g‘𝑊)‘(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))) = (((((♯‘𝐽) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(♯‘𝐽)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (♯‘𝐽))(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))))
347	302, 346	oveq12d 7408	. . . . . . . 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 2798	. . . . . . 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 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Ring)
350	349, 145	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
351		fzossfz 13677	. . . . . . . . . . . . . . . 16 ⊢ (0..^(♯‘𝐽)) ⊆ (0...(♯‘𝐽))
352		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ (0..^(♯‘𝐽)))
353	351, 352	sselid 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ (0...(♯‘𝐽)))
354	101, 353	sselid 3932	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ ℕ₀)
355		peano2nn0 12514	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
356	354, 355	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ ℕ₀)
357	154	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
358	143, 144, 350, 356, 357	mulgnn0cld 19127	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 + 1) ↑ (𝑁‘ 1 )) ∈ 𝐵)
359	26	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐽 ∈ Fin)
360	18	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ CRing)
361	162, 359, 349, 356, 159	esplympl 33824	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘(𝑘 + 1)) ∈ (Base‘(𝐽 mPoly 𝑅)))
362	135	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
363	157, 158, 159, 50, 359, 360, 361, 362	evlcl 22142	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
364	43	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑍:𝐼⟶𝐵)
365	5	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑌 ∈ 𝐼)
366	364, 365	ffvelcdmd 7060	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍‘𝑌) ∈ 𝐵)
367	162, 359, 349, 354, 159	esplympl 33824	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐽 mPoly 𝑅)))
368	157, 158, 159, 50, 359, 360, 367, 362	evlcl 22142	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
369	50, 141, 349, 366, 368	ringcld 20296	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
370	50, 318, 141, 349, 358, 363, 369	ringdid 20299	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
371	23	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐼 ∈ Fin)
372	254	fveq1i 6862	. . . . . . . . . . . . . 14 ⊢ (𝐸‘(𝑘 + 1)) = ((𝐼eSymPoly𝑅)‘(𝑘 + 1))
373	141, 371, 360, 365, 3, 319, 353, 162, 372, 50, 251, 157, 318, 364	esplyindfv 33833	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍) = (((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
374	32	ringabld 20319	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ Abel)
375	374	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Abel)
376	50, 318, 375, 369, 363	ablcomd 33185	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))(+_g‘𝑅)(((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
377	373, 376	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
378	377	oveq2d 7406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))(+_g‘𝑅)((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
379		eqid 2761	. . . . . . . . . . . 12 ⊢ (-_g‘𝑅) = (-_g‘𝑅)
380	151	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑅 ∈ Grp)
381	50, 141, 349, 358, 363	ringcld 20296	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
382	50, 141, 349, 358, 369	ringcld 20296	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) ∈ 𝐵)
383	50, 318, 379, 150, 380, 381, 382	grpsubinv 19044	. . . . . . . . . . 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 2806	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘𝑅)(𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))))
385	52	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝜑 → (-_g‘𝑅) = (-_g‘(Scalar‘𝑊)))
386	385	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (-_g‘𝑅) = (-_g‘(Scalar‘𝑊)))
387		eqidd 2762	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))))
388	238	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (mulGrp‘𝑅) ∈ Mnd)
389		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
390	154	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑁‘ 1 ) ∈ 𝐵)
391	143, 144, 388, 389, 390	mulgnn0cld 19127	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
392	354, 391	syldan 600	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
393	50, 141, 349, 392, 368, 366	ringassd 20293	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌))))
394	152, 150, 144, 349, 354	ringm1expp1 33374	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 + 1) ↑ (𝑁‘ 1 )) = (𝑁‘(𝑘 ↑ (𝑁‘ 1 ))))
395	394	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) = (𝑁‘(𝑁‘(𝑘 ↑ (𝑁‘ 1 )))))
396	50, 150, 380, 392	grpinvinvd 33179	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘(𝑁‘(𝑘 ↑ (𝑁‘ 1 )))) = (𝑘 ↑ (𝑁‘ 1 )))
397	395, 396	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) = (𝑘 ↑ (𝑁‘ 1 )))
398	50, 141, 360, 366, 368	crngcomd 20291	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌)))
399	397, 398	oveq12d 7408	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑘 ↑ (𝑁‘ 1 )) · ((((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) · (𝑍‘𝑌))))
400	50, 141, 150, 349, 358, 369	ringmneg1 20340	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑁‘((𝑘 + 1) ↑ (𝑁‘ 1 ))) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = (𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))))
401	393, 399, 400	3eqtr2rd 2803	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑁‘(((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑍‘𝑌) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))) = (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)))
402	386, 387, 401	oveq123d 7411	. . . . . . . . . 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 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))))
404	403	oveq1d 7405	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))(-_g‘(Scalar‘𝑊))(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
405		eqid 2761	. . . . . . . . 9 ⊢ (-_g‘(Scalar‘𝑊)) = (-_g‘(Scalar‘𝑊))
406	349, 92	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑊 ∈ LMod)
407	54	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐵 = (Base‘(Scalar‘𝑊)))
408	381, 407	eleqtrd 2863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
409	50, 141, 349, 392, 368	ringcld 20296	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
410	50, 141, 349, 409, 366	ringcld 20296	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) ∈ 𝐵)
411	410, 407	eleqtrd 2863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) ∈ (Base‘(Scalar‘𝑊)))
412	108	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑀 ∈ Mnd)
413		fz0ssnn0 13620	. . . . . . . . . . 11 ⊢ (0...𝐻) ⊆ ℕ₀
414		fzossfz 13677	. . . . . . . . . . . 12 ⊢ (0..^𝐻) ⊆ (0...𝐻)
415		fzssp1 13565	. . . . . . . . . . . . . . . 16 ⊢ (1...(♯‘𝐽)) ⊆ (1...((♯‘𝐽) + 1))
416	296	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝐻) = (1...((♯‘𝐽) + 1)))
417	415, 416	sseqtrrid 3977	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ (1...𝐻))
418	417	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (1...(♯‘𝐽)) ⊆ (1...𝐻))
419	359, 90	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) ∈ ℕ₀)
420		fz0add1fz1 13734	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐽) ∈ ℕ₀ ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...(♯‘𝐽)))
421	419, 352, 420	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...(♯‘𝐽)))
422	418, 421	sseldd 3935	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (1...𝐻))
423		ubmelfzo 13729	. . . . . . . . . . . . 13 ⊢ ((𝑘 + 1) ∈ (1...𝐻) → (𝐻 − (𝑘 + 1)) ∈ (0..^𝐻))
424	422, 423	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ (0..^𝐻))
425	414, 424	sselid 3932	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ (0...𝐻))
426	413, 425	sselid 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) ∈ ℕ₀)
427	349, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
428	14, 71, 412, 426, 427	mulgnn0cld 19127	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
429	13, 70, 38, 39, 27, 405, 406, 408, 411, 428	lmodsubdir 20974	. . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐻 = ((♯‘𝐽) + 1))
431	430	oveq1d 7405	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = (((♯‘𝐽) + 1) − (𝑘 + 1)))
432	168	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) ∈ ℂ)
433		1cnd 11168	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 1 ∈ ℂ)
434	356	nn0cnd 12537	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ ℂ)
435	432, 433, 434	addsubd 11556	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) + 1) − (𝑘 + 1)) = (((♯‘𝐽) − (𝑘 + 1)) + 1))
436	431, 435	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = (((♯‘𝐽) − (𝑘 + 1)) + 1))
437	436	oveq1d 7405	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋))
438		fzofzp1 13763	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0..^(♯‘𝐽)) → (𝑘 + 1) ∈ (0...(♯‘𝐽)))
439	438	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑘 + 1) ∈ (0...(♯‘𝐽)))
440		fznn0sub2 13633	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 + 1) ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − (𝑘 + 1)) ∈ (0...(♯‘𝐽)))
441	439, 440	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − (𝑘 + 1)) ∈ (0...(♯‘𝐽)))
442	101, 441	sselid 3932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − (𝑘 + 1)) ∈ ℕ₀)
443	14, 71, 16	mulgnn0p1 19117	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ Mnd ∧ ((♯‘𝐽) − (𝑘 + 1)) ∈ ℕ₀ ∧ 𝑋 ∈ (Base‘𝑊)) → ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
444	412, 442, 427, 443	syl3anc 1389	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((♯‘𝐽) − (𝑘 + 1)) + 1)(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
445	437, 444	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = ((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋))
446	445	oveq2d 7406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
447	360, 40	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑊 ∈ AssAlg)
448	14, 71, 412, 442, 427	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
449	13, 38, 39, 70, 15, 447, 408, 448, 427	assaassd 33711	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋)(._r‘𝑊)𝑋)))
450	446, 449	eqtr4d 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((((𝑘 + 1) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘(𝑘 + 1)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − (𝑘 + 1))(._g‘𝑀)𝑋))(._r‘𝑊)𝑋))
451	63	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)))
452	409, 407	eleqtrd 2863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ (Base‘(Scalar‘𝑊)))
453		fznn0sub2 13633	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...(♯‘𝐽)) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
454	353, 453	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
455	101, 454	sselid 3932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ ℕ₀)
456	14, 71, 412, 455, 427	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
457	13, 38, 70, 39, 336	lmodvsass 20941	. . . . . . . . . . 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 1390	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
459	50, 141, 360, 409, 366	crngcomd 20291	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
460	304	oveqd 7407	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
461	460	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝑍‘𝑌) · ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
462	459, 461	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌)) = ((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))))
463	291	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (♯‘𝐽) = (𝐻 − 1))
464	463	oveq1d 7405	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) = ((𝐻 − 1) − 𝑘))
465	293	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝐻 ∈ ℂ)
466	354	nn0cnd 12537	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → 𝑘 ∈ ℂ)
467	465, 466, 433	sub32d 11567	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − 𝑘) − 1) = ((𝐻 − 1) − 𝑘))
468	465, 466, 433	subsub4d 11566	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − 𝑘) − 1) = (𝐻 − (𝑘 + 1)))
469	464, 467, 468	3eqtr2rd 2803	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (𝐻 − (𝑘 + 1)) = ((♯‘𝐽) − 𝑘))
470	469	oveq1d 7405	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋) = (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))
471	462, 470	oveq12d 7408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = (((𝑍‘𝑌)(._r‘(Scalar‘𝑊))((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))
472	19, 13, 50, 70, 349, 409, 456	ply1vscl 22431	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
473	37, 38, 39, 13, 15, 70	asclmul2 21926	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ AssAlg ∧ (𝑍‘𝑌) ∈ (Base‘(Scalar‘𝑊)) ∧ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊)) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
474	447, 451, 472, 473	syl3anc 1389	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))) = ((𝑍‘𝑌)( ·_𝑠 ‘𝑊)(((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))
475	458, 471, 474	3eqtr4d 2806	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) → ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) · (𝑍‘𝑌))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)) = ((((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))(._r‘𝑊)(𝐴‘(𝑍‘𝑌))))
476	450, 475	oveq12d 7408	. . . . . . . 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 2800	. . . . . . 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 33211	. . . . . 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 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ Ring)
480	479, 145	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
481	101	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐽)) ⊆ ℕ₀)
482	481	sselda 3934	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑘 ∈ ℕ₀)
483	154	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
484	143, 144, 480, 482, 483	mulgnn0cld 19127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
485	26	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝐽 ∈ Fin)
486	18	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑅 ∈ CRing)
487	162, 485, 479, 482, 159	esplympl 33824	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((𝐽eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐽 mPoly 𝑅)))
488	135	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (𝑍 ↾ 𝐽) ∈ (𝐵 ↑_m 𝐽))
489	157, 158, 159, 50, 485, 486, 487, 488	evlcl 22142	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) ∈ 𝐵)
490	50, 141, 479, 484, 489	ringcld 20296	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) ∈ 𝐵)
491	108	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑀 ∈ Mnd)
492	453	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ (0...(♯‘𝐽)))
493	101, 492	sselid 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → ((♯‘𝐽) − 𝑘) ∈ ℕ₀)
494	35	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
495	14, 71, 491, 493, 494	mulgnn0cld 19127	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
496	19, 13, 50, 70, 479, 490, 495	ply1vscl 22431	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(♯‘𝐽))) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
497		oveq1 7397	. . . . . . . . . . 11 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → (𝑘 ↑ (𝑁‘ 1 )) = (((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )))
498		2fveq3 6866	. . . . . . . . . . . 12 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘)) = ((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙))))
499	498	fveq1d 6863	. . . . . . . . . . 11 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)) = (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))
500	497, 499	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝑘 = ((♯‘𝐽) − 𝑙) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))))
501	500	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽))) = ((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽))))
502		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑘 = ((♯‘𝐽) − 𝑙))
503	502	oveq2d 7406	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − 𝑘) = ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)))
504	168	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (♯‘𝐽) ∈ ℂ)
505	103	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑙 ∈ ℕ₀)
506	505	nn0cnd 12537	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → 𝑙 ∈ ℂ)
507	504, 506	nncand 11540	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − ((♯‘𝐽) − 𝑙)) = 𝑙)
508	503, 507	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → ((♯‘𝐽) − 𝑘) = 𝑙)
509	508	oveq1d 7405	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋) = (𝑙(._g‘𝑀)𝑋))
510	501, 509	oveq12d 7408	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) ∧ 𝑘 = ((♯‘𝐽) − 𝑙)) → (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)) = (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))
511	13, 89, 91, 496, 510	gsummptrev 33196	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
512	511	oveq1d 7405	. . . . . 6 ⊢ (𝜑 → ((𝑊 Σ_g (𝑘 ∈ (0...(♯‘𝐽)) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘𝑘))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(((♯‘𝐽) − 𝑘)(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))))
513	32	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑅 ∈ Ring)
514	513, 145	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (mulGrp‘𝑅) ∈ Mnd)
515		fz1ssfz0 13621	. . . . . . . . . . . . . . 15 ⊢ (1...(♯‘𝐽)) ⊆ (0...(♯‘𝐽))
516	515, 101	sstri 3943	. . . . . . . . . . . . . 14 ⊢ (1...(♯‘𝐽)) ⊆ ℕ₀
517	516	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ ℕ₀)
518	517	sselda 3934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑙 ∈ ℕ₀)
519	154	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝑁‘ 1 ) ∈ 𝐵)
520	143, 144, 514, 518, 519	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
521	23	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝐼 ∈ Fin)
522	18	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑅 ∈ CRing)
523	254	fveq1i 6862	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝑙) = ((𝐼eSymPoly𝑅)‘𝑙)
524	256, 521, 513, 518, 253	esplympl 33824	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
525	523, 524	eqeltrid 2865	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
526	259	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
527	251, 252, 253, 50, 521, 522, 525, 526	evlcl 22142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
528	50, 141, 513, 520, 527	ringcld 20296	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
529	108	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑀 ∈ Mnd)
530		fzssp1 13565	. . . . . . . . . . . . . . . 16 ⊢ (0...(♯‘𝐽)) ⊆ (0...((♯‘𝐽) + 1))
531	296	oveq2d 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0...𝐻) = (0...((♯‘𝐽) + 1)))
532	530, 531	sseqtrrid 3977	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0...(♯‘𝐽)) ⊆ (0...𝐻))
533	515, 532	sstrid 3945	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐽)) ⊆ (0...𝐻))
534	533	sselda 3934	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑙 ∈ (0...𝐻))
535		fznn0sub2 13633	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ (0...𝐻) → (𝐻 − 𝑙) ∈ (0...𝐻))
536	534, 535	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ (0...𝐻))
537	413, 536	sselid 3932	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ ℕ₀)
538	513, 34	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → 𝑋 ∈ (Base‘𝑊))
539	14, 71, 529, 537, 538	mulgnn0cld 19127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
540	19, 13, 50, 70, 513, 528, 539	ply1vscl 22431	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ (1...(♯‘𝐽))) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
541		oveq1 7397	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → (𝑙 ↑ (𝑁‘ 1 )) = ((𝑘 + 1) ↑ (𝑁‘ 1 )))
542		2fveq3 6866	. . . . . . . . . . . . 13 ⊢ (𝑙 = (𝑘 + 1) → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘(𝑘 + 1))))
543	542	fveq1d 6863	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))
544	541, 543	oveq12d 7408	. . . . . . . . . . 11 ⊢ (𝑙 = (𝑘 + 1) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = (((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍)))
545		oveq2 7398	. . . . . . . . . . . 12 ⊢ (𝑙 = (𝑘 + 1) → (𝐻 − 𝑙) = (𝐻 − (𝑘 + 1)))
546	545	oveq1d 7405	. . . . . . . . . . 11 ⊢ (𝑙 = (𝑘 + 1) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = ((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋))
547	544, 546	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝑙 = (𝑘 + 1) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
548	547	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0..^(♯‘𝐽))) ∧ 𝑙 = (𝑘 + 1)) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))
549	13, 89, 91, 540, 548	gsummptp1 33197	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0..^(♯‘𝐽)) ↦ ((((𝑘 + 1) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝑘 + 1)))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − (𝑘 + 1))(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
550	549	oveq1d 7405	. . . . . . 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 7397	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → (𝑘 ↑ (𝑁‘ 1 )) = (𝑙 ↑ (𝑁‘ 1 )))
552		2fveq3 6866	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑙 → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘𝑙)))
553	552	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘𝑙))‘𝑍))
554	551, 553	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)))
555		oveq2 7398	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → (𝐻 − 𝑘) = (𝐻 − 𝑙))
556	555	oveq1d 7405	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) = ((𝐻 − 𝑙)(._g‘𝑀)𝑋))
557	554, 556	oveq12d 7408	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) = (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
558	557	cbvmptv 5201	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
559	558	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
560	559	oveq2d 7406	. . . . . . . 8 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
561		nn0uz 12870	. . . . . . . . . . 11 ⊢ ℕ₀ = (ℤ_≥‘0)
562	247, 561	eleqtrdi 2871	. . . . . . . . . 10 ⊢ (𝜑 → 𝐻 ∈ (ℤ_≥‘0))
563	32	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑅 ∈ Ring)
564	563, 145	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (mulGrp‘𝑅) ∈ Mnd)
565	413	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝐻) ⊆ ℕ₀)
566	565	sselda 3934	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑙 ∈ ℕ₀)
567	154	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝑁‘ 1 ) ∈ 𝐵)
568	143, 144, 564, 566, 567	mulgnn0cld 19127	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
569	23	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝐼 ∈ Fin)
570	18	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑅 ∈ CRing)
571	256, 569, 563, 566, 253	esplympl 33824	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
572	523, 571	eqeltrid 2865	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
573	259	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
574	251, 252, 253, 50, 569, 570, 572, 573	evlcl 22142	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
575	50, 141, 563, 568, 574	ringcld 20296	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
576	108	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑀 ∈ Mnd)
577		fznn0sub 13554	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ (0...𝐻) → (𝐻 − 𝑙) ∈ ℕ₀)
578	577	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐻 − 𝑙) ∈ ℕ₀)
579	563, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → 𝑋 ∈ (Base‘𝑊))
580	14, 71, 576, 578, 579	mulgnn0cld 19127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
581	19, 13, 50, 70, 563, 575, 580	ply1vscl 22431	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
582		oveq1 7397	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → (𝑙 ↑ (𝑁‘ 1 )) = (𝐻 ↑ (𝑁‘ 1 )))
583		2fveq3 6866	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝐻 → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘𝐻)))
584	583	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘𝐻))‘𝑍))
585	582, 584	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝐻 → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
586	585	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍)))
587		oveq2 7398	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝐻 → (𝐻 − 𝑙) = (𝐻 − 𝐻))
588	293	subidd 11523	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐻 − 𝐻) = 0)
589	587, 588	sylan9eqr 2818	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → (𝐻 − 𝑙) = 0)
590	589	oveq1d 7405	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = (0(._g‘𝑀)𝑋))
591	586, 590	oveq12d 7408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 = 𝐻) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = (((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))
592	13, 189, 89, 562, 581, 591	gsummptfzsplitra 33198	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋))))
593	91	nn0zd 12586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (♯‘𝐽) ∈ ℤ)
594		fzval3 13733	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐽) ∈ ℤ → (0...(♯‘𝐽)) = (0..^((♯‘𝐽) + 1)))
595	593, 594	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...(♯‘𝐽)) = (0..^((♯‘𝐽) + 1)))
596	296	oveq2d 7406	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝐻) = (0..^((♯‘𝐽) + 1)))
597	595, 596	eqtr4d 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0...(♯‘𝐽)) = (0..^𝐻))
598	597	mpteq1d 5187	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))) = (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
599	598	oveq2d 7406	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))))
600	91, 561	eleqtrdi 2871	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐽) ∈ (ℤ_≥‘0))
601	143, 144, 146, 103, 155	mulgnn0cld 19127	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝑙 ↑ (𝑁‘ 1 )) ∈ 𝐵)
602	23	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝐼 ∈ Fin)
603	256, 602, 110, 103, 253	esplympl 33824	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐼eSymPoly𝑅)‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
604	523, 603	eqeltrid 2865	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐸‘𝑙) ∈ (Base‘(𝐼 mPoly 𝑅)))
605	259	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
606	251, 252, 253, 50, 602, 161, 604, 605	evlcl 22142	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝑄‘(𝐸‘𝑙))‘𝑍) ∈ 𝐵)
607	50, 141, 110, 601, 606	ringcld 20296	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) ∈ 𝐵)
608	532	sselda 3934	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → 𝑙 ∈ (0...𝐻))
609	608, 535	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ (0...𝐻))
610	413, 609	sselid 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (𝐻 − 𝑙) ∈ ℕ₀)
611	14, 71, 109, 610, 111	mulgnn0cld 19127	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
612	19, 13, 50, 70, 110, 607, 611	ply1vscl 22431	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...(♯‘𝐽))) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
613		oveq1 7397	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 0 → (𝑙 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
614	613	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝑙 ↑ (𝑁‘ 1 )) = (0 ↑ (𝑁‘ 1 )))
615		2fveq3 6866	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 = 0 → (𝑄‘(𝐸‘𝑙)) = (𝑄‘(𝐸‘0)))
616	615	fveq1d 6863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 0 → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘0))‘𝑍))
617	616	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = ((𝑄‘(𝐸‘0))‘𝑍))
618		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1_r‘(𝐼 mPoly 𝑅)) = (1_r‘(𝐼 mPoly 𝑅))
619	23, 32, 618	esplyfval0 33821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐼eSymPoly𝑅)‘0) = (1_r‘(𝐼 mPoly 𝑅)))
620	254	fveq1i 6862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐸‘0) = ((𝐼eSymPoly𝑅)‘0)
621	620	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸‘0) = ((𝐼eSymPoly𝑅)‘0))
622		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (algSc‘(𝐼 mPoly 𝑅)) = (algSc‘(𝐼 mPoly 𝑅))
623	252, 622, 277, 618, 23, 32	mplascl1 22065	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)) = (1_r‘(𝐼 mPoly 𝑅)))
624	619, 621, 623	3eqtr4d 2806	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐸‘0) = ((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))
625	624	fveq2d 6865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑄‘(𝐸‘0)) = (𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅))))
626	625	fveq1d 6863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘(𝐸‘0))‘𝑍) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍))
627	626	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘0))‘𝑍) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍))
628	251, 252, 50, 622, 23, 18, 242, 43	evlscaval 33797	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍) = (1_r‘𝑅))
629	628	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑅))‘(1_r‘𝑅)))‘𝑍) = (1_r‘𝑅))
630	617, 627, 629	3eqtrd 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑄‘(𝐸‘𝑙))‘𝑍) = (1_r‘𝑅))
631	614, 630	oveq12d 7408	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍)) = ((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅)))
632		oveq2 7398	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 0 → (𝐻 − 𝑙) = (𝐻 − 0))
633	632	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 𝑙) = (𝐻 − 0))
634	293	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑙 = 0) → 𝐻 ∈ ℂ)
635	634	subid1d 11524	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 0) = 𝐻)
636	633, 635	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑙 = 0) → (𝐻 − 𝑙) = 𝐻)
637	636	oveq1d 7405	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑙 = 0) → ((𝐻 − 𝑙)(._g‘𝑀)𝑋) = (𝐻(._g‘𝑀)𝑋))
638	631, 637	oveq12d 7408	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑙 = 0) → (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) = (((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋)))
639	13, 189, 89, 600, 612, 638	gsummptfzsplitla 33199	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))))
640		0p1e1 12331	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 1) = 1
641	640	oveq1i 7400	. . . . . . . . . . . . . . . 16 ⊢ ((0 + 1)...(♯‘𝐽)) = (1...(♯‘𝐽))
642	641	mpteq1i 5188	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))) = (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))
643	642	oveq2i 7401	. . . . . . . . . . . . . 14 ⊢ (𝑊 Σ_g (𝑙 ∈ ((0 + 1)...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))
644	643	oveq2i 7401	. . . . . . . . . . . . 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 20319	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 ∈ Abel)
647		fzfid 13979	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...(♯‘𝐽)) ∈ Fin)
648	540	ralrimiva 3153	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑙 ∈ (1...(♯‘𝐽))(((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
649	13, 89, 647, 648	gsummptcl 19997	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) ∈ (Base‘𝑊))
650	13, 189, 646, 249, 649	ablcomd 33185	. . . . . . . . . . . 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 2800	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))))
652	599, 651	eqtr3d 2798	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 Σ_g (𝑙 ∈ (0..^𝐻) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋)))) = ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)(((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))))
653	652	oveq1d 7405	. . . . . . . . 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 2797	. . . . . . . 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 18977	. . . . . . . 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 2803	. . . . . . 7 ⊢ (𝜑 → ((𝑊 Σ_g (𝑙 ∈ (1...(♯‘𝐽)) ↦ (((𝑙 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑙))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑙)(._g‘𝑀)𝑋))))(+_g‘𝑊)((((0 ↑ (𝑁‘ 1 )) · (1_r‘𝑅))( ·_𝑠 ‘𝑊)(𝐻(._g‘𝑀)𝑋))(+_g‘𝑊)(((𝐻 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝐻))‘𝑍))( ·_𝑠 ‘𝑊)(0(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))))
657	32	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑅 ∈ Ring)
658	657, 145	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (mulGrp‘𝑅) ∈ Mnd)
659	565	sselda 3934	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑘 ∈ ℕ₀)
660	154	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝑁‘ 1 ) ∈ 𝐵)
661	143, 144, 658, 659, 660	mulgnn0cld 19127	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝑘 ↑ (𝑁‘ 1 )) ∈ 𝐵)
662	23	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝐼 ∈ Fin)
663	18	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑅 ∈ CRing)
664	254	fveq1i 6862	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑘) = ((𝐼eSymPoly𝑅)‘𝑘)
665	256, 662, 657, 659, 253	esplympl 33824	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘𝑘) ∈ (Base‘(𝐼 mPoly 𝑅)))
666	664, 665	eqeltrid 2865	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐸‘𝑘) ∈ (Base‘(𝐼 mPoly 𝑅)))
667	259	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑍 ∈ (𝐵 ↑_m 𝐼))
668	251, 252, 253, 50, 662, 663, 666, 667	evlcl 22142	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘𝑘))‘𝑍) ∈ 𝐵)
669	50, 141, 657, 661, 668	ringcld 20296	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) ∈ 𝐵)
670	108	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑀 ∈ Mnd)
671		fznn0sub2 13633	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝐻) → (𝐻 − 𝑘) ∈ (0...𝐻))
672	671	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐻 − 𝑘) ∈ (0...𝐻))
673	413, 672	sselid 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (𝐻 − 𝑘) ∈ ℕ₀)
674	35	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → 𝑋 ∈ (Base‘𝑊))
675	14, 71, 670, 673, 674	mulgnn0cld 19127	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) ∈ (Base‘𝑊))
676	19, 13, 50, 70, 657, 669, 675	ply1vscl 22431	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝐻)) → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) ∈ (Base‘𝑊))
677		oveq1 7397	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐻 − 𝑙) → (𝑘 ↑ (𝑁‘ 1 )) = ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )))
678		2fveq3 6866	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐻 − 𝑙) → (𝑄‘(𝐸‘𝑘)) = (𝑄‘(𝐸‘(𝐻 − 𝑙))))
679	678	fveq1d 6863	. . . . . . . . . . 11 ⊢ (𝑘 = (𝐻 − 𝑙) → ((𝑄‘(𝐸‘𝑘))‘𝑍) = ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))
680	677, 679	oveq12d 7408	. . . . . . . . . 10 ⊢ (𝑘 = (𝐻 − 𝑙) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)))
681	680	adantl 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → ((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍)) = (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)))
682		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑘 = (𝐻 − 𝑙))
683	682	oveq2d 7406	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − 𝑘) = (𝐻 − (𝐻 − 𝑙)))
684	293	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝐻 ∈ ℂ)
685	566	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑙 ∈ ℕ₀)
686	685	nn0cnd 12537	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → 𝑙 ∈ ℂ)
687	684, 686	nncand 11540	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − (𝐻 − 𝑙)) = 𝑙)
688	683, 687	eqtrd 2796	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (𝐻 − 𝑘) = 𝑙)
689	688	oveq1d 7405	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → ((𝐻 − 𝑘)(._g‘𝑀)𝑋) = (𝑙(._g‘𝑀)𝑋))
690	681, 689	oveq12d 7408	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑙 ∈ (0...𝐻)) ∧ 𝑘 = (𝐻 − 𝑙)) → (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)) = ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))
691	13, 89, 247, 676, 690	gsummptrev 33196	. . . . . . 7 ⊢ (𝜑 → (𝑊 Σ_g (𝑘 ∈ (0...𝐻) ↦ (((𝑘 ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘𝑘))‘𝑍))( ·_𝑠 ‘𝑊)((𝐻 − 𝑘)(._g‘𝑀)𝑋)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
692	550, 656, 691	3eqtrd 2800	. . . . . 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 2804	. . . . 5 ⊢ (𝜑 → ((𝑊 Σ_g (𝑙 ∈ (0...(♯‘𝐽)) ↦ (((((♯‘𝐽) − 𝑙) ↑ (𝑁‘ 1 )) · (((𝐽 eval 𝑅)‘((𝐽eSymPoly𝑅)‘((♯‘𝐽) − 𝑙)))‘(𝑍 ↾ 𝐽)))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))(._r‘𝑊)(𝑋 − (𝐴‘(𝑍‘𝑌)))) = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
694	69, 188, 693	3eqtrd 2800	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))
695	694	fveq2d 6865	. . 3 ⊢ (𝜑 → (coe₁‘𝐹) = (coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋))))))
696	695	fveq1d 6863	. 2 ⊢ (𝜑 → ((coe₁‘𝐹)‘𝐾) = ((coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))‘𝐾))
697	12	fveq2i 6864	. . 3 ⊢ (._g‘𝑀) = (._g‘(mulGrp‘𝑊))
698	143, 144, 564, 578, 567	mulgnn0cld 19127	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) ∈ 𝐵)
699	254	fveq1i 6862	. . . . . . 7 ⊢ (𝐸‘(𝐻 − 𝑙)) = ((𝐼eSymPoly𝑅)‘(𝐻 − 𝑙))
700	256, 569, 563, 578, 253	esplympl 33824	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝐼eSymPoly𝑅)‘(𝐻 − 𝑙)) ∈ (Base‘(𝐼 mPoly 𝑅)))
701	699, 700	eqeltrid 2865	. . . . . 6 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (𝐸‘(𝐻 − 𝑙)) ∈ (Base‘(𝐼 mPoly 𝑅)))
702	251, 252, 253, 50, 569, 570, 701, 573	evlcl 22142	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍) ∈ 𝐵)
703	50, 141, 563, 698, 702	ringcld 20296	. . . 4 ⊢ ((𝜑 ∧ 𝑙 ∈ (0...𝐻)) → (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) ∈ 𝐵)
704	703	ralrimiva 3153	. . 3 ⊢ (𝜑 → ∀𝑙 ∈ (0...𝐻)(((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) ∈ 𝐵)
705		vieta.k	. . 3 ⊢ (𝜑 → 𝐾 ∈ (0...𝐻))
706		oveq2 7398	. . . . 5 ⊢ (𝑙 = 𝐾 → (𝐻 − 𝑙) = (𝐻 − 𝐾))
707	706	oveq1d 7405	. . . 4 ⊢ (𝑙 = 𝐾 → ((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) = ((𝐻 − 𝐾) ↑ (𝑁‘ 1 )))
708	706	fveq2d 6865	. . . . . 6 ⊢ (𝑙 = 𝐾 → (𝐸‘(𝐻 − 𝑙)) = (𝐸‘(𝐻 − 𝐾)))
709	708	fveq2d 6865	. . . . 5 ⊢ (𝑙 = 𝐾 → (𝑄‘(𝐸‘(𝐻 − 𝑙))) = (𝑄‘(𝐸‘(𝐻 − 𝐾))))
710	709	fveq1d 6863	. . . 4 ⊢ (𝑙 = 𝐾 → ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍) = ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍))
711	707, 710	oveq12d 7408	. . 3 ⊢ (𝑙 = 𝐾 → (((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍)) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))
712	19, 13, 33, 697, 32, 50, 70, 247, 704, 705, 711	gsummoncoe1fz 33754	. 2 ⊢ (𝜑 → ((coe₁‘(𝑊 Σ_g (𝑙 ∈ (0...𝐻) ↦ ((((𝐻 − 𝑙) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝑙)))‘𝑍))( ·_𝑠 ‘𝑊)(𝑙(._g‘𝑀)𝑋)))))‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))
713	696, 712	eqtrd 2796	1 ⊢ (𝜑 → ((coe₁‘𝐹)‘𝐾) = (((𝐻 − 𝐾) ↑ (𝑁‘ 1 )) · ((𝑄‘(𝐸‘(𝐻 − 𝐾)))‘𝑍)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ∀wral 3075 {crab 3413 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ⊆ wss 3902 {csn 4579 class class class wbr 5097 ↦ cmpt 5178 ↾ cres 5645 ⟶wf 6511 ‘cfv 6515 (class class class)co 7390 ↑_m cmap 8801 Fincfn 8920 finSupp cfsupp 9300 ℂcc 11064 0cc0 11066 1c1 11067 + caddc 11069 − cmin 11407 ℕ₀cn0 12474 ℤcz 12561 ℤ_≥cuz 12832 ...cfz 13505 ..^cfzo 13652 ♯chash 14336 Basecbs 17235 +_gcplusg 17276 ._rcmulr 17277 Scalarcsca 17279 ·_𝑠 cvsca 17280 Σ_g cgsu 17459 Mndcmnd 18758 Grpcgrp 18965 inv_gcminusg 18966 -_gcsg 18967 ._gcmg 19099 CMndccmn 19810 Abelcabl 19811 mulGrpcmgp 20176 1_rcur 20217 Ringcrg 20269 CRingccrg 20270 IDomncidom 20729 LModclmod 20914 AssAlgcasa 21889 algSccascl 21891 mPoly cmpl 21945 eval cevl 22113 var₁cv1 22225 Poly₁cpl1 22226 coe₁cco1 22227 deg₁cdg1 26101 eSymPolycesply 33813

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143 ax-pre-sup 11144 ax-addf 11145 ax-mulf 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-isom 6524 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7654 df-ofr 7655 df-om 7841 df-1st 7964 df-2nd 7965 df-supp 8134 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-2o 8431 df-oadd 8434 df-er 8671 df-map 8803 df-pm 8804 df-ixp 8873 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-fsupp 9301 df-sup 9381 df-oi 9451 df-dju 9852 df-card 9890 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-div 11838 df-ind 12189 df-nn 12204 df-2 12273 df-3 12274 df-4 12275 df-5 12276 df-6 12277 df-7 12278 df-8 12279 df-9 12280 df-n0 12475 df-xnn0 12548 df-z 12562 df-dec 12682 df-uz 12833 df-rp 12987 df-fz 13506 df-fzo 13653 df-seq 14008 df-fac 14280 df-bc 14309 df-hash 14337 df-struct 17173 df-sets 17190 df-slot 17208 df-ndx 17220 df-base 17236 df-ress 17257 df-plusg 17289 df-mulr 17290 df-starv 17291 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-hom 17300 df-cco 17301 df-0g 17460 df-gsum 17461 df-prds 17466 df-pws 17468 df-mre 17604 df-mrc 17605 df-acs 17607 df-mgm 18664 df-sgrp 18743 df-mnd 18759 df-mhm 18807 df-submnd 18808 df-grp 18968 df-minusg 18969 df-sbg 18970 df-mulg 19100 df-subg 19155 df-ghm 19244 df-cntz 19347 df-cmn 19812 df-abl 19813 df-mgp 20177 df-rng 20189 df-ur 20218 df-srg 20223 df-ring 20271 df-cring 20272 df-rhm 20507 df-subrng 20582 df-subrg 20606 df-idom 20732 df-lmod 20916 df-lss 20986 df-lsp 21026 df-cnfld 21412 df-zring 21486 df-zrh 21542 df-assa 21892 df-asp 21893 df-ascl 21894 df-psr 21948 df-mvr 21949 df-mpl 21950 df-opsr 21952 df-evls 22114 df-evl 22115 df-psr1 22229 df-vr1 22230 df-ply1 22231 df-coe1 22232 df-mdeg 26102 df-deg1 26103 df-extv 33787 df-esply 33815

This theorem is referenced by: vieta 33837

W3C validator