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	|- P = ( Poly1 ` R )
	ply1coedeg.x	|- X = ( var1 ` R )
	ply1coedeg.b	|- B = ( Base ` P )
	ply1coedeg.n	|- .x. = ( .s ` P )
	ply1coedeg.m	|- M = ( mulGrp ` P )
	ply1coedeg.e	|- .^ = ( .g ` M )
	ply1coedeg.a	|- A = ( coe1 ` K )
	ply1coedeg.d	|- D = ( ( deg1 ` R ) ` K )
	ply1coedeg.r	|- ( ph -> R e. Ring )
	ply1coedeg.k	|- ( ph -> K e. B )
Assertion	ply1coedeg	|- ( ph -> K = ( P gsum ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1coedeg.p	|- P = ( Poly1 ` R )
2		ply1coedeg.x	|- X = ( var1 ` R )
3		ply1coedeg.b	|- B = ( Base ` P )
4		ply1coedeg.n	|- .x. = ( .s ` P )
5		ply1coedeg.m	|- M = ( mulGrp ` P )
6		ply1coedeg.e	|- .^ = ( .g ` M )
7		ply1coedeg.a	|- A = ( coe1 ` K )
8		ply1coedeg.d	|- D = ( ( deg1 ` R ) ` K )
9		ply1coedeg.r	|- ( ph -> R e. Ring )
10		ply1coedeg.k	|- ( ph -> K e. B )
11		simpr	|- ( ( ph /\ K = ( 0g ` P ) ) -> K = ( 0g ` P ) )
12	8	a1i	|- ( ( ph /\ K = ( 0g ` P ) ) -> D = ( ( deg1 ` R ) ` K ) )
13	11	fveq2d	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( ( deg1 ` R ) ` K ) = ( ( deg1 ` R ) ` ( 0g ` P ) ) )
14		eqid	|- ( deg1 ` R ) = ( deg1 ` R )
15		eqid	|- ( 0g ` P ) = ( 0g ` P )
16	14 1 15	deg1z	|- ( R e. Ring -> ( ( deg1 ` R ) ` ( 0g ` P ) ) = -oo )
17	9 16	syl	|- ( ph -> ( ( deg1 ` R ) ` ( 0g ` P ) ) = -oo )
18	17	adantr	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( ( deg1 ` R ) ` ( 0g ` P ) ) = -oo )
19	12 13 18	3eqtrd	|- ( ( ph /\ K = ( 0g ` P ) ) -> D = -oo )
20	19	oveq2d	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( 0 ... D ) = ( 0 ... -oo ) )
21		mnfnre	|- -oo e/ RR
22	21	neli	|- -. -oo e. RR
23		zre	|- ( -oo e. ZZ -> -oo e. RR )
24	22 23	mto	|- -. -oo e. ZZ
25	24	nelir	|- -oo e/ ZZ
26	25	olci	|- ( 0 e/ ZZ \/ -oo e/ ZZ )
27		fz0	|- ( ( 0 e/ ZZ \/ -oo e/ ZZ ) -> ( 0 ... -oo ) = (/) )
28	26 27	ax-mp	|- ( 0 ... -oo ) = (/)
29	20 28	eqtrdi	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( 0 ... D ) = (/) )
30	29	mpteq1d	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) = ( k e. (/) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) )
31		mpt0	|- ( k e. (/) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) = (/)
32	30 31	eqtrdi	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) = (/) )
33	32	oveq2d	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( P gsum ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) = ( P gsum (/) ) )
34	15	gsum0	|- ( P gsum (/) ) = ( 0g ` P )
35	33 34	eqtrdi	|- ( ( ph /\ K = ( 0g ` P ) ) -> ( P gsum ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) = ( 0g ` P ) )
36	11 35	eqtr4d	|- ( ( ph /\ K = ( 0g ` P ) ) -> K = ( P gsum ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
37	1 2 3 4 5 6 7	ply1coe	|- ( ( R e. Ring /\ K e. B ) -> K = ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
38	9 10 37	syl2anc	|- ( ph -> K = ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
39	38	adantr	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> K = ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
40	1	ply1ring	|- ( R e. Ring -> P e. Ring )
41	9 40	syl	|- ( ph -> P e. Ring )
42	41	ringcmnd	|- ( ph -> P e. CMnd )
43	42	adantr	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> P e. CMnd )
44		nn0ex	|- NN0 e. _V
45	44	a1i	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> NN0 e. _V )
46	10	ad2antrr	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> K e. B )
47		difssd	|- ( ph -> ( NN0 \ ( 0 ... D ) ) C_ NN0 )
48	47	sselda	|- ( ( ph /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> k e. NN0 )
49	48	adantlr	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> k e. NN0 )
50	9	adantr	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> R e. Ring )
51	10	adantr	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> K e. B )
52		simpr	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> K =/= ( 0g ` P ) )
53	14 1 15 3	deg1nn0cl	|- ( ( R e. Ring /\ K e. B /\ K =/= ( 0g ` P ) ) -> ( ( deg1 ` R ) ` K ) e. NN0 )
54	50 51 52 53	syl3anc	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> ( ( deg1 ` R ) ` K ) e. NN0 )
55	8 54	eqeltrid	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> D e. NN0 )
56	55	nn0zd	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> D e. ZZ )
57		nn0diffz0	|- ( D e. NN0 -> ( NN0 \ ( 0 ... D ) ) = ( ZZ>= ` ( D + 1 ) ) )
58	55 57	syl	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> ( NN0 \ ( 0 ... D ) ) = ( ZZ>= ` ( D + 1 ) ) )
59	58	eleq2d	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> ( k e. ( NN0 \ ( 0 ... D ) ) <-> k e. ( ZZ>= ` ( D + 1 ) ) ) )
60	59	biimpa	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> k e. ( ZZ>= ` ( D + 1 ) ) )
61		eluzp1l	|- ( ( D e. ZZ /\ k e. ( ZZ>= ` ( D + 1 ) ) ) -> D < k )
62	56 60 61	syl2an2r	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> D < k )
63	8 62	eqbrtrrid	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( ( deg1 ` R ) ` K ) < k )
64		eqid	|- ( 0g ` R ) = ( 0g ` R )
65	14 1 3 64 7	deg1lt	|- ( ( K e. B /\ k e. NN0 /\ ( ( deg1 ` R ) ` K ) < k ) -> ( A ` k ) = ( 0g ` R ) )
66	46 49 63 65	syl3anc	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( A ` k ) = ( 0g ` R ) )
67	1	ply1sca	|- ( R e. Ring -> R = ( Scalar ` P ) )
68	9 67	syl	|- ( ph -> R = ( Scalar ` P ) )
69	68	fveq2d	|- ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
70	69	ad2antrr	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
71	66 70	eqtrd	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( A ` k ) = ( 0g ` ( Scalar ` P ) ) )
72	71	oveq1d	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( ( A ` k ) .x. ( k .^ X ) ) = ( ( 0g ` ( Scalar ` P ) ) .x. ( k .^ X ) ) )
73	1	ply1lmod	|- ( R e. Ring -> P e. LMod )
74	9 73	syl	|- ( ph -> P e. LMod )
75	5 3	mgpbas	|- B = ( Base ` M )
76	5	ringmgp	|- ( P e. Ring -> M e. Mnd )
77	41 76	syl	|- ( ph -> M e. Mnd )
78	77	adantr	|- ( ( ph /\ k e. NN0 ) -> M e. Mnd )
79		simpr	|- ( ( ph /\ k e. NN0 ) -> k e. NN0 )
80	2 1 3	vr1cl	|- ( R e. Ring -> X e. B )
81	9 80	syl	|- ( ph -> X e. B )
82	81	adantr	|- ( ( ph /\ k e. NN0 ) -> X e. B )
83	75 6 78 79 82	mulgnn0cld	|- ( ( ph /\ k e. NN0 ) -> ( k .^ X ) e. B )
84	48 83	syldan	|- ( ( ph /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( k .^ X ) e. B )
85		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
86		eqid	|- ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
87	3 85 4 86 15	lmod0vs	|- ( ( P e. LMod /\ ( k .^ X ) e. B ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( k .^ X ) ) = ( 0g ` P ) )
88	74 84 87	syl2an2r	|- ( ( ph /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( k .^ X ) ) = ( 0g ` P ) )
89	88	adantlr	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( ( 0g ` ( Scalar ` P ) ) .x. ( k .^ X ) ) = ( 0g ` P ) )
90	72 89	eqtrd	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. ( NN0 \ ( 0 ... D ) ) ) -> ( ( A ` k ) .x. ( k .^ X ) ) = ( 0g ` P ) )
91		fzfid	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> ( 0 ... D ) e. Fin )
92		eqid	|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
93	74	adantr	|- ( ( ph /\ k e. NN0 ) -> P e. LMod )
94		eqid	|- ( Base ` R ) = ( Base ` R )
95	7 3 1 94	coe1fvalcl	|- ( ( K e. B /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` R ) )
96	10 95	sylan	|- ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` R ) )
97	68	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
98	97	adantr	|- ( ( ph /\ k e. NN0 ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
99	96 98	eleqtrd	|- ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. ( Base ` ( Scalar ` P ) ) )
100	3 85 4 92 93 99 83	lmodvscld	|- ( ( ph /\ k e. NN0 ) -> ( ( A ` k ) .x. ( k .^ X ) ) e. B )
101	100	adantlr	|- ( ( ( ph /\ K =/= ( 0g ` P ) ) /\ k e. NN0 ) -> ( ( A ` k ) .x. ( k .^ X ) ) e. B )
102		fz0ssnn0	|- ( 0 ... D ) C_ NN0
103	102	a1i	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> ( 0 ... D ) C_ NN0 )
104	3 15 43 45 90 91 101 103	gsummptres2	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> ( P gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) = ( P gsum ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
105	39 104	eqtrd	|- ( ( ph /\ K =/= ( 0g ` P ) ) -> K = ( P gsum ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )
106	36 105	pm2.61dane	|- ( ph -> K = ( P gsum ( k e. ( 0 ... D ) |-> ( ( A ` k ) .x. ( k .^ X ) ) ) ) )