Metamath Proof Explorer

Theorem mhppwdeg

Description: Degree of a homogeneous polynomial raised to a power. General version of deg1pw . (Contributed by SN, 26-Jul-2024) Remove sethood hypothesis. (Revised by SN, 18-May-2025)

Ref Expression
Hypotheses mhppwdeg.h 
|- H = ( I mHomP R )
mhppwdeg.p 
|- P = ( I mPoly R )
mhppwdeg.t 
|- T = ( mulGrp ` P )
mhppwdeg.e 
|- .^ = ( .g ` T )
mhppwdeg.r 
|- ( ph -> R e. Ring )
mhppwdeg.m 
|- ( ph -> M e. NN0 )
mhppwdeg.n 
|- ( ph -> N e. NN0 )
mhppwdeg.x 
|- ( ph -> X e. ( H ` M ) )
Assertion mhppwdeg 
|- ( ph -> ( N .^ X ) e. ( H ` ( M x. N ) ) )

Proof

Step Hyp Ref Expression
1 mhppwdeg.h 
 |-  H = ( I mHomP R )
2 mhppwdeg.p 
 |-  P = ( I mPoly R )
3 mhppwdeg.t 
 |-  T = ( mulGrp ` P )
4 mhppwdeg.e 
 |-  .^ = ( .g ` T )
5 mhppwdeg.r 
 |-  ( ph -> R e. Ring )
6 mhppwdeg.m 
 |-  ( ph -> M e. NN0 )
7 mhppwdeg.n 
 |-  ( ph -> N e. NN0 )
8 mhppwdeg.x 
 |-  ( ph -> X e. ( H ` M ) )
9 oveq1 
 |-  ( x = 0 -> ( x .^ X ) = ( 0 .^ X ) )
10 oveq2 
 |-  ( x = 0 -> ( M x. x ) = ( M x. 0 ) )
11 10 fveq2d 
 |-  ( x = 0 -> ( H ` ( M x. x ) ) = ( H ` ( M x. 0 ) ) )
12 9 11 eleq12d 
 |-  ( x = 0 -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( 0 .^ X ) e. ( H ` ( M x. 0 ) ) ) )
13 oveq1 
 |-  ( x = y -> ( x .^ X ) = ( y .^ X ) )
14 oveq2 
 |-  ( x = y -> ( M x. x ) = ( M x. y ) )
15 14 fveq2d 
 |-  ( x = y -> ( H ` ( M x. x ) ) = ( H ` ( M x. y ) ) )
16 13 15 eleq12d 
 |-  ( x = y -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( y .^ X ) e. ( H ` ( M x. y ) ) ) )
17 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .^ X ) = ( ( y + 1 ) .^ X ) )
18 oveq2 
 |-  ( x = ( y + 1 ) -> ( M x. x ) = ( M x. ( y + 1 ) ) )
19 18 fveq2d 
 |-  ( x = ( y + 1 ) -> ( H ` ( M x. x ) ) = ( H ` ( M x. ( y + 1 ) ) ) )
20 17 19 eleq12d 
 |-  ( x = ( y + 1 ) -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( ( y + 1 ) .^ X ) e. ( H ` ( M x. ( y + 1 ) ) ) ) )
21 oveq1 
 |-  ( x = N -> ( x .^ X ) = ( N .^ X ) )
22 oveq2 
 |-  ( x = N -> ( M x. x ) = ( M x. N ) )
23 22 fveq2d 
 |-  ( x = N -> ( H ` ( M x. x ) ) = ( H ` ( M x. N ) ) )
24 21 23 eleq12d 
 |-  ( x = N -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( N .^ X ) e. ( H ` ( M x. N ) ) ) )
25 reldmmhp 
 |-  Rel dom mHomP
26 25 1 8 elfvov1 
 |-  ( ph -> I e. _V )
27 2 26 5 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
28 27 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
29 28 fveq2d 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( algSc ` P ) ` ( 1r ` ( Scalar ` P ) ) ) )
30 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
31 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
32 2 mpllmod 
 |-  ( ( I e. _V /\ R e. Ring ) -> P e. LMod )
33 26 5 32 syl2anc 
 |-  ( ph -> P e. LMod )
34 2 mplring 
 |-  ( ( I e. _V /\ R e. Ring ) -> P e. Ring )
35 26 5 34 syl2anc 
 |-  ( ph -> P e. Ring )
36 30 31 33 35 ascl1 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` ( Scalar ` P ) ) ) = ( 1r ` P ) )
37 29 36 eqtrd 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
38 eqid 
 |-  ( Base ` R ) = ( Base ` R )
39 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
40 38 39 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
41 5 40 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
42 1 2 30 38 26 5 41 mhpsclcl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( H ` 0 ) )
43 37 42 eqeltrrd 
 |-  ( ph -> ( 1r ` P ) e. ( H ` 0 ) )
44 eqid 
 |-  ( Base ` P ) = ( Base ` P )
45 1 2 44 26 5 6 8 mhpmpl 
 |-  ( ph -> X e. ( Base ` P ) )
46 3 44 mgpbas 
 |-  ( Base ` P ) = ( Base ` T )
47 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
48 3 47 ringidval 
 |-  ( 1r ` P ) = ( 0g ` T )
49 46 48 4 mulg0 
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
50 45 49 syl 
 |-  ( ph -> ( 0 .^ X ) = ( 1r ` P ) )
51 6 nn0cnd 
 |-  ( ph -> M e. CC )
52 51 mul01d 
 |-  ( ph -> ( M x. 0 ) = 0 )
53 52 fveq2d 
 |-  ( ph -> ( H ` ( M x. 0 ) ) = ( H ` 0 ) )
54 43 50 53 3eltr4d 
 |-  ( ph -> ( 0 .^ X ) e. ( H ` ( M x. 0 ) ) )
55 eqid 
 |-  ( .r ` P ) = ( .r ` P )
56 5 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> R e. Ring )
57 6 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> M e. NN0 )
58 simplr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> y e. NN0 )
59 57 58 nn0mulcld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( M x. y ) e. NN0 )
60 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( y .^ X ) e. ( H ` ( M x. y ) ) )
61 8 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> X e. ( H ` M ) )
62 1 2 55 56 59 57 60 61 mhpmulcl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( y .^ X ) ( .r ` P ) X ) e. ( H ` ( ( M x. y ) + M ) ) )
63 3 ringmgp 
 |-  ( P e. Ring -> T e. Mnd )
64 35 63 syl 
 |-  ( ph -> T e. Mnd )
65 64 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> T e. Mnd )
66 45 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> X e. ( Base ` P ) )
67 3 55 mgpplusg 
 |-  ( .r ` P ) = ( +g ` T )
68 46 4 67 mulgnn0p1 
 |-  ( ( T e. Mnd /\ y e. NN0 /\ X e. ( Base ` P ) ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` P ) X ) )
69 65 58 66 68 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` P ) X ) )
70 51 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> M e. CC )
71 58 nn0cnd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> y e. CC )
72 1cnd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> 1 e. CC )
73 70 71 72 adddid 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( M x. ( y + 1 ) ) = ( ( M x. y ) + ( M x. 1 ) ) )
74 70 mulridd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( M x. 1 ) = M )
75 74 oveq2d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( M x. y ) + ( M x. 1 ) ) = ( ( M x. y ) + M ) )
76 73 75 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( M x. ( y + 1 ) ) = ( ( M x. y ) + M ) )
77 76 fveq2d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( H ` ( M x. ( y + 1 ) ) ) = ( H ` ( ( M x. y ) + M ) ) )
78 62 69 77 3eltr4d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> ( ( y + 1 ) .^ X ) e. ( H ` ( M x. ( y + 1 ) ) ) )
79 12 16 20 24 54 78 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( N .^ X ) e. ( H ` ( M x. N ) ) )
80 7 79 mpdan 
 |-  ( ph -> ( N .^ X ) e. ( H ` ( M x. N ) ) )