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 
|- 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 ) ) ) ) )