Theorem ply1coedeg

Description: Decompose a univariate polynomial K as a sum of powers, up to its degree D . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	ply1coedeg.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1coedeg.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1coedeg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1coedeg.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
	ply1coedeg.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	ply1coedeg.e	⊢ ↑ = ( .g ‘ 𝑀 )
	ply1coedeg.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
	ply1coedeg.d	⊢ 𝐷 = ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 )
	ply1coedeg.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1coedeg.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
Assertion	ply1coedeg	⊢ ( 𝜑 → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1coedeg.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1coedeg.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		ply1coedeg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1coedeg.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
5		ply1coedeg.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
6		ply1coedeg.e	⊢ ↑ = ( .g ‘ 𝑀 )
7		ply1coedeg.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
8		ply1coedeg.d	⊢ 𝐷 = ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 )
9		ply1coedeg.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10		ply1coedeg.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐵 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → 𝐾 = ( 0g ‘ 𝑃 ) )
12	8	a1i	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → 𝐷 = ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 ) )
13	11	fveq2d	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 ) = ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) )
14		eqid	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
15		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
16	14 1 15	deg1z	⊢ ( 𝑅 ∈ Ring → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
17	9 16	syl	⊢ ( 𝜑 → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
19	12 13 18	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → 𝐷 = -∞ )
20	19	oveq2d	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( 0 ... 𝐷 ) = ( 0 ... -∞ ) )
21		mnfnre	⊢ -∞ ∉ ℝ
22	21	neli	⊢ ¬ -∞ ∈ ℝ
23		zre	⊢ ( -∞ ∈ ℤ → -∞ ∈ ℝ )
24	22 23	mto	⊢ ¬ -∞ ∈ ℤ
25	24	nelir	⊢ -∞ ∉ ℤ
26	25	olci	⊢ ( 0 ∉ ℤ ∨ -∞ ∉ ℤ )
27		fz0	⊢ ( ( 0 ∉ ℤ ∨ -∞ ∉ ℤ ) → ( 0 ... -∞ ) = ∅ )
28	26 27	ax-mp	⊢ ( 0 ... -∞ ) = ∅
29	20 28	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( 0 ... 𝐷 ) = ∅ )
30	29	mpteq1d	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ∅ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) )
31		mpt0	⊢ ( 𝑘 ∈ ∅ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) = ∅
32	30 31	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) = ∅ )
33	32	oveq2d	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ∅ ) )
34	15	gsum0	⊢ ( 𝑃 Σg ∅ ) = ( 0g ‘ 𝑃 )
35	33 34	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 0g ‘ 𝑃 ) )
36	11 35	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐾 = ( 0g ‘ 𝑃 ) ) → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
37	1 2 3 4 5 6 7	ply1coe	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
38	9 10 37	syl2anc	⊢ ( 𝜑 → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
40	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
41	9 40	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
42	41	ringcmnd	⊢ ( 𝜑 → 𝑃 ∈ CMnd )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝑃 ∈ CMnd )
44		nn0ex	⊢ ℕ0 ∈ V
45	44	a1i	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ℕ0 ∈ V )
46	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → 𝐾 ∈ 𝐵 )
47		difssd	⊢ ( 𝜑 → ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ⊆ ℕ0 )
48	47	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → 𝑘 ∈ ℕ0 )
49	48	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → 𝑘 ∈ ℕ0 )
50	9	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝑅 ∈ Ring )
51	10	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝐾 ∈ 𝐵 )
52		simpr	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝐾 ≠ ( 0g ‘ 𝑃 ) )
53	14 1 15 3	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 ) ∈ ℕ0 )
54	50 51 52 53	syl3anc	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 ) ∈ ℕ0 )
55	8 54	eqeltrid	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝐷 ∈ ℕ0 )
56	55	nn0zd	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝐷 ∈ ℤ )
57		nn0diffz0	⊢ ( 𝐷 ∈ ℕ0 → ( ℕ0 ∖ ( 0 ... 𝐷 ) ) = ( ℤ≥ ‘ ( 𝐷 + 1 ) ) )
58	55 57	syl	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ( ℕ0 ∖ ( 0 ... 𝐷 ) ) = ( ℤ≥ ‘ ( 𝐷 + 1 ) ) )
59	58	eleq2d	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ↔ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐷 + 1 ) ) ) )
60	59	biimpa	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐷 + 1 ) ) )
61		eluzp1l	⊢ ( ( 𝐷 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐷 + 1 ) ) ) → 𝐷 < 𝑘 )
62	56 60 61	syl2an2r	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → 𝐷 < 𝑘 )
63	8 62	eqbrtrrid	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 ) < 𝑘 )
64		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
65	14 1 3 64 7	deg1lt	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝐾 ) < 𝑘 ) → ( 𝐴 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
66	46 49 63 65	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( 𝐴 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
67	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
68	9 67	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
69	68	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
70	69	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
71	66 70	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( 𝐴 ‘ 𝑘 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
72	71	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑘 ↑ 𝑋 ) ) )
73	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
74	9 73	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
75	5 3	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
76	5	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
77	41 76	syl	⊢ ( 𝜑 → 𝑀 ∈ Mnd )
78	77	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
79		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
80	2 1 3	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
81	9 80	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
82	81	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
83	75 6 78 79 82	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
84	48 83	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
85		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
86		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
87	3 85 4 86 15	lmod0vs	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
88	74 84 87	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
89	88	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
90	72 89	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ... 𝐷 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
91		fzfid	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ( 0 ... 𝐷 ) ∈ Fin )
92		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
93	74	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod )
94		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
95	7 3 1 94	coe1fvalcl	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
96	10 95	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
97	68	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
98	97	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
99	96 98	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
100	3 85 4 92 93 99 83	lmodvscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
101	100	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
102		fz0ssnn0	⊢ ( 0 ... 𝐷 ) ⊆ ℕ0
103	102	a1i	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ( 0 ... 𝐷 ) ⊆ ℕ0 )
104	3 15 43 45 90 91 101 103	gsummptres2	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
105	39 104	eqtrd	⊢ ( ( 𝜑 ∧ 𝐾 ≠ ( 0g ‘ 𝑃 ) ) → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
106	36 105	pm2.61dane	⊢ ( 𝜑 → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )