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 = {Poly}_{1} (R)$
	ply1coedeg.x	$⊢ X = {var}_{1} (R)$
	ply1coedeg.b	$⊢ B = {Base}_{P}$
	ply1coedeg.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1coedeg.m	$⊢ M = {mulGrp}_{P}$
	ply1coedeg.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
	ply1coedeg.a	$⊢ A = {coe}_{1} (K)$
	ply1coedeg.d	$⊢ D = \deg_{1} (R) (K)$
	ply1coedeg.r	$⊢ φ \to R \in Ring$
	ply1coedeg.k	$⊢ φ \to K \in B$
Assertion	ply1coedeg	$⊢ φ \to K = {\sum_{P}}_{k = 0}^{D} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$

Proof

Step	Hyp	Ref	Expression
1		ply1coedeg.p	$⊢ P = {Poly}_{1} (R)$
2		ply1coedeg.x	$⊢ X = {var}_{1} (R)$
3		ply1coedeg.b	$⊢ B = {Base}_{P}$
4		ply1coedeg.n	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		ply1coedeg.m	$⊢ M = {mulGrp}_{P}$
6		ply1coedeg.e	$⊢ \underset{˙}{\times} = \cdot_{M}$
7		ply1coedeg.a	$⊢ A = {coe}_{1} (K)$
8		ply1coedeg.d	$⊢ D = \deg_{1} (R) (K)$
9		ply1coedeg.r	$⊢ φ \to R \in Ring$
10		ply1coedeg.k	$⊢ φ \to K \in B$
11		simpr	$⊢ (φ \land K = 0_{P}) \to K = 0_{P}$
12	8	a1i	$⊢ (φ \land K = 0_{P}) \to D = \deg_{1} (R) (K)$
13	11	fveq2d	$⊢ (φ \land K = 0_{P}) \to \deg_{1} (R) (K) = \deg_{1} (R) (0_{P})$
14		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
15		eqid	$⊢ 0_{P} = 0_{P}$
16	14 1 15	deg1z	$⊢ R \in Ring \to \deg_{1} (R) (0_{P}) = −∞$
17	9 16	syl	$⊢ φ \to \deg_{1} (R) (0_{P}) = −∞$
18	17	adantr	$⊢ (φ \land K = 0_{P}) \to \deg_{1} (R) (0_{P}) = −∞$
19	12 13 18	3eqtrd	$⊢ (φ \land K = 0_{P}) \to D = −∞$
20	19	oveq2d	$⊢ (φ \land K = 0_{P}) \to (0 \dots D) = (0 \dots −∞)$
21		mnfnre	$⊢ −∞ \notin ℝ$
22	21	neli	$⊢ \neg −∞ \in ℝ$
23		zre	$⊢ −∞ \in ℤ \to −∞ \in ℝ$
24	22 23	mto	$⊢ \neg −∞ \in ℤ$
25	24	nelir	$⊢ −∞ \notin ℤ$
26	25	olci	$⊢ (0 \notin ℤ \lor −∞ \notin ℤ)$
27		fz0	$⊢ (0 \notin ℤ \lor −∞ \notin ℤ) \to (0 \dots −∞) = \emptyset$
28	26 27	ax-mp	$⊢ (0 \dots −∞) = \emptyset$
29	20 28	eqtrdi	$⊢ (φ \land K = 0_{P}) \to (0 \dots D) = \emptyset$
30	29	mpteq1d	$⊢ (φ \land K = 0_{P}) \to (k \in (0 \dots D) ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = (k \in \emptyset ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
31		mpt0	$⊢ (k \in \emptyset ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = \emptyset$
32	30 31	eqtrdi	$⊢ (φ \land K = 0_{P}) \to (k \in (0 \dots D) ⟼ A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = \emptyset$
33	32	oveq2d	$⊢ (φ \land K = 0_{P}) \to {\sum_{P}}_{k = 0}^{D} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = \sum_{P} \emptyset$
34	15	gsum0	$⊢ \sum_{P} \emptyset = 0_{P}$
35	33 34	eqtrdi	$⊢ (φ \land K = 0_{P}) \to {\sum_{P}}_{k = 0}^{D} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = 0_{P}$
36	11 35	eqtr4d	$⊢ (φ \land K = 0_{P}) \to K = {\sum_{P}}_{k = 0}^{D} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
37	1 2 3 4 5 6 7	ply1coe	$⊢ (R \in Ring \land K \in B) \to K = \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
38	9 10 37	syl2anc	$⊢ φ \to K = \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
39	38	adantr	$⊢ (φ \land K \neq 0_{P}) \to K = \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
40	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
41	9 40	syl	$⊢ φ \to P \in Ring$
42	41	ringcmnd	$⊢ φ \to P \in CMnd$
43	42	adantr	$⊢ (φ \land K \neq 0_{P}) \to P \in CMnd$
44		nn0ex	$⊢ ℕ_{0} \in V$
45	44	a1i	$⊢ (φ \land K \neq 0_{P}) \to ℕ_{0} \in V$
46	10	ad2antrr	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to K \in B$
47		difssd	$⊢ φ \to ℕ_{0} ∖ (0 \dots D) \subseteq ℕ_{0}$
48	47	sselda	$⊢ (φ \land k \in (ℕ_{0} ∖ (0 \dots D))) \to k \in ℕ_{0}$
49	48	adantlr	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to k \in ℕ_{0}$
50	9	adantr	$⊢ (φ \land K \neq 0_{P}) \to R \in Ring$
51	10	adantr	$⊢ (φ \land K \neq 0_{P}) \to K \in B$
52		simpr	$⊢ (φ \land K \neq 0_{P}) \to K \neq 0_{P}$
53	14 1 15 3	deg1nn0cl	$⊢ (R \in Ring \land K \in B \land K \neq 0_{P}) \to \deg_{1} (R) (K) \in ℕ_{0}$
54	50 51 52 53	syl3anc	$⊢ (φ \land K \neq 0_{P}) \to \deg_{1} (R) (K) \in ℕ_{0}$
55	8 54	eqeltrid	$⊢ (φ \land K \neq 0_{P}) \to D \in ℕ_{0}$
56	55	nn0zd	$⊢ (φ \land K \neq 0_{P}) \to D \in ℤ$
57		nn0diffz0	$⊢ D \in ℕ_{0} \to ℕ_{0} ∖ (0 \dots D) = ℤ_{\geq (D + 1)}$
58	55 57	syl	$⊢ (φ \land K \neq 0_{P}) \to ℕ_{0} ∖ (0 \dots D) = ℤ_{\geq (D + 1)}$
59	58	eleq2d	$⊢ (φ \land K \neq 0_{P}) \to (k \in (ℕ_{0} ∖ (0 \dots D)) \leftrightarrow k \in ℤ_{\geq (D + 1)})$
60	59	biimpa	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to k \in ℤ_{\geq (D + 1)}$
61		eluzp1l	$⊢ (D \in ℤ \land k \in ℤ_{\geq (D + 1)}) \to D < k$
62	56 60 61	syl2an2r	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to D < k$
63	8 62	eqbrtrrid	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to \deg_{1} (R) (K) < k$
64		eqid	$⊢ 0_{R} = 0_{R}$
65	14 1 3 64 7	deg1lt	$⊢ (K \in B \land k \in ℕ_{0} \land \deg_{1} (R) (K) < k) \to A (k) = 0_{R}$
66	46 49 63 65	syl3anc	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to A (k) = 0_{R}$
67	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
68	9 67	syl	$⊢ φ \to R = Scalar (P)$
69	68	fveq2d	$⊢ φ \to 0_{R} = 0_{Scalar (P)}$
70	69	ad2antrr	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to 0_{R} = 0_{Scalar (P)}$
71	66 70	eqtrd	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to A (k) = 0_{Scalar (P)}$
72	71	oveq1d	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) = 0_{Scalar (P)} \underset{˙}{\cdot} (k \underset{˙}{\times} X)$
73	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
74	9 73	syl	$⊢ φ \to P \in LMod$
75	5 3	mgpbas	$⊢ B = {Base}_{M}$
76	5	ringmgp	$⊢ P \in Ring \to M \in Mnd$
77	41 76	syl	$⊢ φ \to M \in Mnd$
78	77	adantr	$⊢ (φ \land k \in ℕ_{0}) \to M \in Mnd$
79		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
80	2 1 3	vr1cl	$⊢ R \in Ring \to X \in B$
81	9 80	syl	$⊢ φ \to X \in B$
82	81	adantr	$⊢ (φ \land k \in ℕ_{0}) \to X \in B$
83	75 6 78 79 82	mulgnn0cld	$⊢ (φ \land k \in ℕ_{0}) \to k \underset{˙}{\times} X \in B$
84	48 83	syldan	$⊢ (φ \land k \in (ℕ_{0} ∖ (0 \dots D))) \to k \underset{˙}{\times} X \in B$
85		eqid	$⊢ Scalar (P) = Scalar (P)$
86		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
87	3 85 4 86 15	lmod0vs	$⊢ (P \in LMod \land k \underset{˙}{\times} X \in B) \to 0_{Scalar (P)} \underset{˙}{\cdot} (k \underset{˙}{\times} X) = 0_{P}$
88	74 84 87	syl2an2r	$⊢ (φ \land k \in (ℕ_{0} ∖ (0 \dots D))) \to 0_{Scalar (P)} \underset{˙}{\cdot} (k \underset{˙}{\times} X) = 0_{P}$
89	88	adantlr	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to 0_{Scalar (P)} \underset{˙}{\cdot} (k \underset{˙}{\times} X) = 0_{P}$
90	72 89	eqtrd	$⊢ ((φ \land K \neq 0_{P}) \land k \in (ℕ_{0} ∖ (0 \dots D))) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) = 0_{P}$
91		fzfid	$⊢ (φ \land K \neq 0_{P}) \to (0 \dots D) \in Fin$
92		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
93	74	adantr	$⊢ (φ \land k \in ℕ_{0}) \to P \in LMod$
94		eqid	$⊢ {Base}_{R} = {Base}_{R}$
95	7 3 1 94	coe1fvalcl	$⊢ (K \in B \land k \in ℕ_{0}) \to A (k) \in {Base}_{R}$
96	10 95	sylan	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in {Base}_{R}$
97	68	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (P)}$
98	97	adantr	$⊢ (φ \land k \in ℕ_{0}) \to {Base}_{R} = {Base}_{Scalar (P)}$
99	96 98	eleqtrd	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \in {Base}_{Scalar (P)}$
100	3 85 4 92 93 99 83	lmodvscld	$⊢ (φ \land k \in ℕ_{0}) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) \in B$
101	100	adantlr	$⊢ ((φ \land K \neq 0_{P}) \land k \in ℕ_{0}) \to A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X) \in B$
102		fz0ssnn0	$⊢ (0 \dots D) \subseteq ℕ_{0}$
103	102	a1i	$⊢ (φ \land K \neq 0_{P}) \to (0 \dots D) \subseteq ℕ_{0}$
104	3 15 43 45 90 91 101 103	gsummptres2	$⊢ (φ \land K \neq 0_{P}) \to \underset{k \in ℕ_{0}}{\sum_{P}} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X)) = {\sum_{P}}_{k = 0}^{D} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
105	39 104	eqtrd	$⊢ (φ \land K \neq 0_{P}) \to K = {\sum_{P}}_{k = 0}^{D} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$
106	36 105	pm2.61dane	$⊢ φ \to K = {\sum_{P}}_{k = 0}^{D} (A (k) \underset{˙}{\cdot} (k \underset{˙}{\times} X))$

Metamath Proof Explorer

Theorem ply1coedeg

Proof