This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ... 𝐷 ) ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )