Metamath Proof Explorer

Theorem deg1pow

Description: Exact degree of a power of a polynomial in an integral domain. (Contributed by metakunt, 6-May-2025)

Ref Expression
Hypotheses deg1pow.1 
|- ( ph -> R e. IDomn )
deg1pow.2 
|- ( ph -> F e. ( Base ` ( Poly1 ` R ) ) )
deg1pow.3 
|- ( ph -> F =/= ( 0g ` ( Poly1 ` R ) ) )
deg1pow.4 
|- ( ph -> A e. NN0 )
deg1pow.5 
|- .^ = ( .g ` ( mulGrp ` ( Poly1 ` R ) ) )
deg1pow.6 
|- D = ( deg1 ` R )
Assertion deg1pow 
|- ( ph -> ( D ` ( A .^ F ) ) = ( A x. ( D ` F ) ) )

Proof

Step Hyp Ref Expression
1 deg1pow.1 
 |-  ( ph -> R e. IDomn )
2 deg1pow.2 
 |-  ( ph -> F e. ( Base ` ( Poly1 ` R ) ) )
3 deg1pow.3 
 |-  ( ph -> F =/= ( 0g ` ( Poly1 ` R ) ) )
4 deg1pow.4 
 |-  ( ph -> A e. NN0 )
5 deg1pow.5 
 |-  .^ = ( .g ` ( mulGrp ` ( Poly1 ` R ) ) )
6 deg1pow.6 
 |-  D = ( deg1 ` R )
7 fvoveq1 
 |-  ( x = 0 -> ( D ` ( x .^ F ) ) = ( D ` ( 0 .^ F ) ) )
8 oveq1 
 |-  ( x = 0 -> ( x x. ( D ` F ) ) = ( 0 x. ( D ` F ) ) )
9 7 8 eqeq12d 
 |-  ( x = 0 -> ( ( D ` ( x .^ F ) ) = ( x x. ( D ` F ) ) <-> ( D ` ( 0 .^ F ) ) = ( 0 x. ( D ` F ) ) ) )
10 fvoveq1 
 |-  ( x = y -> ( D ` ( x .^ F ) ) = ( D ` ( y .^ F ) ) )
11 oveq1 
 |-  ( x = y -> ( x x. ( D ` F ) ) = ( y x. ( D ` F ) ) )
12 10 11 eqeq12d 
 |-  ( x = y -> ( ( D ` ( x .^ F ) ) = ( x x. ( D ` F ) ) <-> ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) )
13 fvoveq1 
 |-  ( x = ( y + 1 ) -> ( D ` ( x .^ F ) ) = ( D ` ( ( y + 1 ) .^ F ) ) )
14 oveq1 
 |-  ( x = ( y + 1 ) -> ( x x. ( D ` F ) ) = ( ( y + 1 ) x. ( D ` F ) ) )
15 13 14 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( D ` ( x .^ F ) ) = ( x x. ( D ` F ) ) <-> ( D ` ( ( y + 1 ) .^ F ) ) = ( ( y + 1 ) x. ( D ` F ) ) ) )
16 fvoveq1 
 |-  ( x = A -> ( D ` ( x .^ F ) ) = ( D ` ( A .^ F ) ) )
17 oveq1 
 |-  ( x = A -> ( x x. ( D ` F ) ) = ( A x. ( D ` F ) ) )
18 16 17 eqeq12d 
 |-  ( x = A -> ( ( D ` ( x .^ F ) ) = ( x x. ( D ` F ) ) <-> ( D ` ( A .^ F ) ) = ( A x. ( D ` F ) ) ) )
19 eqid 
 |-  ( mulGrp ` ( Poly1 ` R ) ) = ( mulGrp ` ( Poly1 ` R ) )
20 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
21 19 20 mgpbas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( mulGrp ` ( Poly1 ` R ) ) )
22 eqid 
 |-  ( 1r ` ( Poly1 ` R ) ) = ( 1r ` ( Poly1 ` R ) )
23 19 22 ringidval 
 |-  ( 1r ` ( Poly1 ` R ) ) = ( 0g ` ( mulGrp ` ( Poly1 ` R ) ) )
24 21 23 5 mulg0 
 |-  ( F e. ( Base ` ( Poly1 ` R ) ) -> ( 0 .^ F ) = ( 1r ` ( Poly1 ` R ) ) )
25 2 24 syl 
 |-  ( ph -> ( 0 .^ F ) = ( 1r ` ( Poly1 ` R ) ) )
26 25 fveq2d 
 |-  ( ph -> ( D ` ( 0 .^ F ) ) = ( D ` ( 1r ` ( Poly1 ` R ) ) ) )
27 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
28 27 simprbi 
 |-  ( R e. IDomn -> R e. Domn )
29 domnring 
 |-  ( R e. Domn -> R e. Ring )
30 28 29 syl 
 |-  ( R e. IDomn -> R e. Ring )
31 1 30 syl 
 |-  ( ph -> R e. Ring )
32 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
33 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
34 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
35 32 33 34 22 ply1scl1 
 |-  ( R e. Ring -> ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) = ( 1r ` ( Poly1 ` R ) ) )
36 31 35 syl 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) = ( 1r ` ( Poly1 ` R ) ) )
37 36 eqcomd 
 |-  ( ph -> ( 1r ` ( Poly1 ` R ) ) = ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) )
38 37 fveq2d 
 |-  ( ph -> ( D ` ( 1r ` ( Poly1 ` R ) ) ) = ( D ` ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) ) )
39 eqid 
 |-  ( Base ` R ) = ( Base ` R )
40 39 34 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
41 31 40 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
42 1 28 syl 
 |-  ( ph -> R e. Domn )
43 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
44 42 43 syl 
 |-  ( ph -> R e. NzRing )
45 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
46 34 45 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
47 44 46 syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
48 6 32 39 33 45 deg1scl 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( D ` ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) ) = 0 )
49 31 41 47 48 syl3anc 
 |-  ( ph -> ( D ` ( ( algSc ` ( Poly1 ` R ) ) ` ( 1r ` R ) ) ) = 0 )
50 38 49 eqtrd 
 |-  ( ph -> ( D ` ( 1r ` ( Poly1 ` R ) ) ) = 0 )
51 26 50 eqtrd 
 |-  ( ph -> ( D ` ( 0 .^ F ) ) = 0 )
52 eqid 
 |-  ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) )
53 6 32 52 20 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. ( Base ` ( Poly1 ` R ) ) /\ F =/= ( 0g ` ( Poly1 ` R ) ) ) -> ( D ` F ) e. NN0 )
54 31 2 3 53 syl3anc 
 |-  ( ph -> ( D ` F ) e. NN0 )
55 54 nn0cnd 
 |-  ( ph -> ( D ` F ) e. CC )
56 55 mul02d 
 |-  ( ph -> ( 0 x. ( D ` F ) ) = 0 )
57 56 eqcomd 
 |-  ( ph -> 0 = ( 0 x. ( D ` F ) ) )
58 51 57 eqtrd 
 |-  ( ph -> ( D ` ( 0 .^ F ) ) = ( 0 x. ( D ` F ) ) )
59 32 ply1idom 
 |-  ( R e. IDomn -> ( Poly1 ` R ) e. IDomn )
60 1 59 syl 
 |-  ( ph -> ( Poly1 ` R ) e. IDomn )
61 60 idomringd 
 |-  ( ph -> ( Poly1 ` R ) e. Ring )
62 61 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> ( Poly1 ` R ) e. Ring )
63 62 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( Poly1 ` R ) e. Ring )
64 19 ringmgp 
 |-  ( ( Poly1 ` R ) e. Ring -> ( mulGrp ` ( Poly1 ` R ) ) e. Mnd )
65 63 64 syl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( mulGrp ` ( Poly1 ` R ) ) e. Mnd )
66 simplr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> y e. NN0 )
67 2 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> F e. ( Base ` ( Poly1 ` R ) ) )
68 eqid 
 |-  ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( +g ` ( mulGrp ` ( Poly1 ` R ) ) )
69 21 5 68 mulgnn0p1 
 |-  ( ( ( mulGrp ` ( Poly1 ` R ) ) e. Mnd /\ y e. NN0 /\ F e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( y + 1 ) .^ F ) = ( ( y .^ F ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) F ) )
70 65 66 67 69 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( ( y + 1 ) .^ F ) = ( ( y .^ F ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) F ) )
71 70 fveq2d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( D ` ( ( y + 1 ) .^ F ) ) = ( D ` ( ( y .^ F ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) F ) ) )
72 eqid 
 |-  ( .r ` ( Poly1 ` R ) ) = ( .r ` ( Poly1 ` R ) )
73 19 72 mgpplusg 
 |-  ( .r ` ( Poly1 ` R ) ) = ( +g ` ( mulGrp ` ( Poly1 ` R ) ) )
74 73 eqcomi 
 |-  ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) = ( .r ` ( Poly1 ` R ) )
75 1 idomdomd 
 |-  ( ph -> R e. Domn )
76 75 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> R e. Domn )
77 76 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> R e. Domn )
78 21 5 65 66 67 mulgnn0cld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( y .^ F ) e. ( Base ` ( Poly1 ` R ) ) )
79 60 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> ( Poly1 ` R ) e. IDomn )
80 79 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( Poly1 ` R ) e. IDomn )
81 3 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> F =/= ( 0g ` ( Poly1 ` R ) ) )
82 80 67 81 66 5 idomnnzpownz 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( y .^ F ) =/= ( 0g ` ( Poly1 ` R ) ) )
83 6 32 20 74 52 77 78 82 67 81 deg1mul 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( D ` ( ( y .^ F ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) F ) ) = ( ( D ` ( y .^ F ) ) + ( D ` F ) ) )
84 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) )
85 84 oveq1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( ( D ` ( y .^ F ) ) + ( D ` F ) ) = ( ( y x. ( D ` F ) ) + ( D ` F ) ) )
86 66 nn0cnd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> y e. CC )
87 55 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( D ` F ) e. CC )
88 86 87 adddirp1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( ( y + 1 ) x. ( D ` F ) ) = ( ( y x. ( D ` F ) ) + ( D ` F ) ) )
89 88 eqcomd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( ( y x. ( D ` F ) ) + ( D ` F ) ) = ( ( y + 1 ) x. ( D ` F ) ) )
90 85 89 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( ( D ` ( y .^ F ) ) + ( D ` F ) ) = ( ( y + 1 ) x. ( D ` F ) ) )
91 83 90 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( D ` ( ( y .^ F ) ( +g ` ( mulGrp ` ( Poly1 ` R ) ) ) F ) ) = ( ( y + 1 ) x. ( D ` F ) ) )
92 71 91 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( D ` ( y .^ F ) ) = ( y x. ( D ` F ) ) ) -> ( D ` ( ( y + 1 ) .^ F ) ) = ( ( y + 1 ) x. ( D ` F ) ) )
93 9 12 15 18 58 92 nn0indd 
 |-  ( ( ph /\ A e. NN0 ) -> ( D ` ( A .^ F ) ) = ( A x. ( D ` F ) ) )
94 93 ex 
 |-  ( ph -> ( A e. NN0 -> ( D ` ( A .^ F ) ) = ( A x. ( D ` F ) ) ) )
95 4 94 mpd 
 |-  ( ph -> ( D ` ( A .^ F ) ) = ( A x. ( D ` F ) ) )