Metamath Proof Explorer

Theorem vietadeg1

Description: The degree of a product of H of linear polynomials of the form X - Z is H . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses vieta.w 
|- W = ( Poly1 ` R )
vieta.b 
|- B = ( Base ` R )
vieta.3 
|- .- = ( -g ` W )
vieta.m 
|- M = ( mulGrp ` W )
vieta.q 
|- Q = ( I eval R )
vieta.e 
|- E = ( I eSymPoly R )
vieta.n 
|- N = ( invg ` R )
vieta.1 
|- .1. = ( 1r ` R )
vieta.t 
|- .x. = ( .r ` R )
vieta.x 
|- X = ( var1 ` R )
vieta.a 
|- A = ( algSc ` W )
vieta.p 
|- .^ = ( .g ` ( mulGrp ` R ) )
vieta.h 
|- H = ( # ` I )
vieta.i 
|- ( ph -> I e. Fin )
vieta.r 
|- ( ph -> R e. IDomn )
vieta.z 
|- ( ph -> Z : I --> B )
vieta.f 
|- F = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) )
vietadeg1.1 
|- D = ( deg1 ` R )
Assertion vietadeg1 
|- ( ph -> ( D ` F ) = H )

Proof

Step Hyp Ref Expression
1 vieta.w 
 |-  W = ( Poly1 ` R )
2 vieta.b 
 |-  B = ( Base ` R )
3 vieta.3 
 |-  .- = ( -g ` W )
4 vieta.m 
 |-  M = ( mulGrp ` W )
5 vieta.q 
 |-  Q = ( I eval R )
6 vieta.e 
 |-  E = ( I eSymPoly R )
7 vieta.n 
 |-  N = ( invg ` R )
8 vieta.1 
 |-  .1. = ( 1r ` R )
9 vieta.t 
 |-  .x. = ( .r ` R )
10 vieta.x 
 |-  X = ( var1 ` R )
11 vieta.a 
 |-  A = ( algSc ` W )
12 vieta.p 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
13 vieta.h 
 |-  H = ( # ` I )
14 vieta.i 
 |-  ( ph -> I e. Fin )
15 vieta.r 
 |-  ( ph -> R e. IDomn )
16 vieta.z 
 |-  ( ph -> Z : I --> B )
17 vieta.f 
 |-  F = ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) )
18 vietadeg1.1 
 |-  D = ( deg1 ` R )
19 17 fveq2i 
 |-  ( D ` F ) = ( D ` ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) )
20 eqid 
 |-  ( Base ` W ) = ( Base ` W )
21 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
22 15 idomringd 
 |-  ( ph -> R e. Ring )
23 1 ply1ring 
 |-  ( R e. Ring -> W e. Ring )
24 ringgrp 
 |-  ( W e. Ring -> W e. Grp )
25 22 23 24 3syl 
 |-  ( ph -> W e. Grp )
26 25 adantr 
 |-  ( ( ph /\ n e. I ) -> W e. Grp )
27 10 1 20 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` W ) )
28 22 27 syl 
 |-  ( ph -> X e. ( Base ` W ) )
29 28 adantr 
 |-  ( ( ph /\ n e. I ) -> X e. ( Base ` W ) )
30 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
31 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
32 15 idomcringd 
 |-  ( ph -> R e. CRing )
33 1 ply1assa 
 |-  ( R e. CRing -> W e. AssAlg )
34 32 33 syl 
 |-  ( ph -> W e. AssAlg )
35 34 adantr 
 |-  ( ( ph /\ n e. I ) -> W e. AssAlg )
36 16 ffvelcdmda 
 |-  ( ( ph /\ n e. I ) -> ( Z ` n ) e. B )
37 1 ply1sca 
 |-  ( R e. IDomn -> R = ( Scalar ` W ) )
38 15 37 syl 
 |-  ( ph -> R = ( Scalar ` W ) )
39 38 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` W ) ) )
40 2 39 eqtrid 
 |-  ( ph -> B = ( Base ` ( Scalar ` W ) ) )
41 40 adantr 
 |-  ( ( ph /\ n e. I ) -> B = ( Base ` ( Scalar ` W ) ) )
42 36 41 eleqtrd 
 |-  ( ( ph /\ n e. I ) -> ( Z ` n ) e. ( Base ` ( Scalar ` W ) ) )
43 11 30 31 35 42 asclelbas 
 |-  ( ( ph /\ n e. I ) -> ( A ` ( Z ` n ) ) e. ( Base ` W ) )
44 20 3 26 29 43 grpsubcld 
 |-  ( ( ph /\ n e. I ) -> ( X .- ( A ` ( Z ` n ) ) ) e. ( Base ` W ) )
45 15 idomdomd 
 |-  ( ph -> R e. Domn )
46 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
47 45 46 syl 
 |-  ( ph -> R e. NzRing )
48 18 1 10 47 deg1vr 
 |-  ( ph -> ( D ` X ) = 1 )
49 48 ad2antrr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) = 1 )
50 18 1 20 deg1cl 
 |-  ( X e. ( Base ` W ) -> ( D ` X ) e. ( NN0 u. { -oo } ) )
51 28 50 syl 
 |-  ( ph -> ( D ` X ) e. ( NN0 u. { -oo } ) )
52 51 nn0mnfxrd 
 |-  ( ph -> ( D ` X ) e. RR* )
53 52 ad2antrr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) e. RR* )
54 49 53 eqeltrrd 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> 1 e. RR* )
55 51 ad2antrr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) e. ( NN0 u. { -oo } ) )
56 0zd 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> 0 e. ZZ )
57 26 adantr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> W e. Grp )
58 29 adantr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> X e. ( Base ` W ) )
59 43 adantr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( A ` ( Z ` n ) ) e. ( Base ` W ) )
60 simpr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) )
61 20 21 3 grpsubeq0 
 |-  ( ( W e. Grp /\ X e. ( Base ` W ) /\ ( A ` ( Z ` n ) ) e. ( Base ` W ) ) -> ( ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) <-> X = ( A ` ( Z ` n ) ) ) )
62 61 biimpa 
 |-  ( ( ( W e. Grp /\ X e. ( Base ` W ) /\ ( A ` ( Z ` n ) ) e. ( Base ` W ) ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> X = ( A ` ( Z ` n ) ) )
63 57 58 59 60 62 syl31anc 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> X = ( A ` ( Z ` n ) ) )
64 63 fveq2d 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) = ( D ` ( A ` ( Z ` n ) ) ) )
65 22 adantr 
 |-  ( ( ph /\ n e. I ) -> R e. Ring )
66 18 1 2 11 deg1sclle 
 |-  ( ( R e. Ring /\ ( Z ` n ) e. B ) -> ( D ` ( A ` ( Z ` n ) ) ) <_ 0 )
67 65 36 66 syl2anc 
 |-  ( ( ph /\ n e. I ) -> ( D ` ( A ` ( Z ` n ) ) ) <_ 0 )
68 67 adantr 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` ( A ` ( Z ` n ) ) ) <_ 0 )
69 64 68 eqbrtrd 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) <_ 0 )
70 degltp1le 
 |-  ( ( ( D ` X ) e. ( NN0 u. { -oo } ) /\ 0 e. ZZ ) -> ( ( D ` X ) < ( 0 + 1 ) <-> ( D ` X ) <_ 0 ) )
71 70 biimpar 
 |-  ( ( ( ( D ` X ) e. ( NN0 u. { -oo } ) /\ 0 e. ZZ ) /\ ( D ` X ) <_ 0 ) -> ( D ` X ) < ( 0 + 1 ) )
72 55 56 69 71 syl21anc 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) < ( 0 + 1 ) )
73 0p1e1 
 |-  ( 0 + 1 ) = 1
74 72 73 breqtrdi 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) < 1 )
75 53 54 74 xrgtned 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> 1 =/= ( D ` X ) )
76 75 necomd 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> ( D ` X ) =/= 1 )
77 76 neneqd 
 |-  ( ( ( ph /\ n e. I ) /\ ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) ) -> -. ( D ` X ) = 1 )
78 49 77 pm2.65da 
 |-  ( ( ph /\ n e. I ) -> -. ( X .- ( A ` ( Z ` n ) ) ) = ( 0g ` W ) )
79 78 neqned 
 |-  ( ( ph /\ n e. I ) -> ( X .- ( A ` ( Z ` n ) ) ) =/= ( 0g ` W ) )
80 44 79 eldifsnd 
 |-  ( ( ph /\ n e. I ) -> ( X .- ( A ` ( Z ` n ) ) ) e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
81 80 fmpttd 
 |-  ( ph -> ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) : I --> ( ( Base ` W ) \ { ( 0g ` W ) } ) )
82 18 1 20 4 21 14 15 81 deg1prod 
 |-  ( ph -> ( D ` ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ) = sum_ k e. I ( D ` ( ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ` k ) ) )
83 eqid 
 |-  ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) = ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) )
84 2fveq3 
 |-  ( n = k -> ( A ` ( Z ` n ) ) = ( A ` ( Z ` k ) ) )
85 84 oveq2d 
 |-  ( n = k -> ( X .- ( A ` ( Z ` n ) ) ) = ( X .- ( A ` ( Z ` k ) ) ) )
86 simpr 
 |-  ( ( ph /\ k e. I ) -> k e. I )
87 ovexd 
 |-  ( ( ph /\ k e. I ) -> ( X .- ( A ` ( Z ` k ) ) ) e. _V )
88 83 85 86 87 fvmptd3 
 |-  ( ( ph /\ k e. I ) -> ( ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ` k ) = ( X .- ( A ` ( Z ` k ) ) ) )
89 88 fveq2d 
 |-  ( ( ph /\ k e. I ) -> ( D ` ( ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ` k ) ) = ( D ` ( X .- ( A ` ( Z ` k ) ) ) ) )
90 18 1 20 deg1xrcl 
 |-  ( ( A ` ( Z ` n ) ) e. ( Base ` W ) -> ( D ` ( A ` ( Z ` n ) ) ) e. RR* )
91 43 90 syl 
 |-  ( ( ph /\ n e. I ) -> ( D ` ( A ` ( Z ` n ) ) ) e. RR* )
92 0xr 
 |-  0 e. RR*
93 92 a1i 
 |-  ( ( ph /\ n e. I ) -> 0 e. RR* )
94 1xr 
 |-  1 e. RR*
95 94 a1i 
 |-  ( ( ph /\ n e. I ) -> 1 e. RR* )
96 0lt1 
 |-  0 < 1
97 96 a1i 
 |-  ( ( ph /\ n e. I ) -> 0 < 1 )
98 91 93 95 67 97 xrlelttrd 
 |-  ( ( ph /\ n e. I ) -> ( D ` ( A ` ( Z ` n ) ) ) < 1 )
99 48 adantr 
 |-  ( ( ph /\ n e. I ) -> ( D ` X ) = 1 )
100 98 99 breqtrrd 
 |-  ( ( ph /\ n e. I ) -> ( D ` ( A ` ( Z ` n ) ) ) < ( D ` X ) )
101 1 18 65 20 3 29 43 100 deg1sub 
 |-  ( ( ph /\ n e. I ) -> ( D ` ( X .- ( A ` ( Z ` n ) ) ) ) = ( D ` X ) )
102 101 99 eqtrd 
 |-  ( ( ph /\ n e. I ) -> ( D ` ( X .- ( A ` ( Z ` n ) ) ) ) = 1 )
103 102 ralrimiva 
 |-  ( ph -> A. n e. I ( D ` ( X .- ( A ` ( Z ` n ) ) ) ) = 1 )
104 85 fveqeq2d 
 |-  ( n = k -> ( ( D ` ( X .- ( A ` ( Z ` n ) ) ) ) = 1 <-> ( D ` ( X .- ( A ` ( Z ` k ) ) ) ) = 1 ) )
105 104 cbvralvw 
 |-  ( A. n e. I ( D ` ( X .- ( A ` ( Z ` n ) ) ) ) = 1 <-> A. k e. I ( D ` ( X .- ( A ` ( Z ` k ) ) ) ) = 1 )
106 103 105 sylib 
 |-  ( ph -> A. k e. I ( D ` ( X .- ( A ` ( Z ` k ) ) ) ) = 1 )
107 106 r19.21bi 
 |-  ( ( ph /\ k e. I ) -> ( D ` ( X .- ( A ` ( Z ` k ) ) ) ) = 1 )
108 89 107 eqtrd 
 |-  ( ( ph /\ k e. I ) -> ( D ` ( ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ` k ) ) = 1 )
109 108 sumeq2dv 
 |-  ( ph -> sum_ k e. I ( D ` ( ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ` k ) ) = sum_ k e. I 1 )
110 1cnd 
 |-  ( ph -> 1 e. CC )
111 fsumconst 
 |-  ( ( I e. Fin /\ 1 e. CC ) -> sum_ k e. I 1 = ( ( # ` I ) x. 1 ) )
112 14 110 111 syl2anc 
 |-  ( ph -> sum_ k e. I 1 = ( ( # ` I ) x. 1 ) )
113 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
114 14 113 syl 
 |-  ( ph -> ( # ` I ) e. NN0 )
115 114 nn0cnd 
 |-  ( ph -> ( # ` I ) e. CC )
116 115 mulridd 
 |-  ( ph -> ( ( # ` I ) x. 1 ) = ( # ` I ) )
117 116 13 eqtr4di 
 |-  ( ph -> ( ( # ` I ) x. 1 ) = H )
118 109 112 117 3eqtrd 
 |-  ( ph -> sum_ k e. I ( D ` ( ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ` k ) ) = H )
119 82 118 eqtrd 
 |-  ( ph -> ( D ` ( M gsum ( n e. I |-> ( X .- ( A ` ( Z ` n ) ) ) ) ) ) = H )
120 19 119 eqtrid 
 |-  ( ph -> ( D ` F ) = H )