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)

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.i 
|- ( ph -> I e. V )
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.i 
 |-  ( ph -> I e. V )
6 mhppwdeg.r 
 |-  ( ph -> R e. Ring )
7 mhppwdeg.m 
 |-  ( ph -> M e. NN0 )
8 mhppwdeg.n 
 |-  ( ph -> N e. NN0 )
9 mhppwdeg.x 
 |-  ( ph -> X e. ( H ` M ) )
10 oveq1 
 |-  ( x = 0 -> ( x .^ X ) = ( 0 .^ X ) )
11 oveq2 
 |-  ( x = 0 -> ( M x. x ) = ( M x. 0 ) )
12 11 fveq2d 
 |-  ( x = 0 -> ( H ` ( M x. x ) ) = ( H ` ( M x. 0 ) ) )
13 10 12 eleq12d 
 |-  ( x = 0 -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( 0 .^ X ) e. ( H ` ( M x. 0 ) ) ) )
14 oveq1 
 |-  ( x = y -> ( x .^ X ) = ( y .^ X ) )
15 oveq2 
 |-  ( x = y -> ( M x. x ) = ( M x. y ) )
16 15 fveq2d 
 |-  ( x = y -> ( H ` ( M x. x ) ) = ( H ` ( M x. y ) ) )
17 14 16 eleq12d 
 |-  ( x = y -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( y .^ X ) e. ( H ` ( M x. y ) ) ) )
18 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .^ X ) = ( ( y + 1 ) .^ X ) )
19 oveq2 
 |-  ( x = ( y + 1 ) -> ( M x. x ) = ( M x. ( y + 1 ) ) )
20 19 fveq2d 
 |-  ( x = ( y + 1 ) -> ( H ` ( M x. x ) ) = ( H ` ( M x. ( y + 1 ) ) ) )
21 18 20 eleq12d 
 |-  ( x = ( y + 1 ) -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( ( y + 1 ) .^ X ) e. ( H ` ( M x. ( y + 1 ) ) ) ) )
22 oveq1 
 |-  ( x = N -> ( x .^ X ) = ( N .^ X ) )
23 oveq2 
 |-  ( x = N -> ( M x. x ) = ( M x. N ) )
24 23 fveq2d 
 |-  ( x = N -> ( H ` ( M x. x ) ) = ( H ` ( M x. N ) ) )
25 22 24 eleq12d 
 |-  ( x = N -> ( ( x .^ X ) e. ( H ` ( M x. x ) ) <-> ( N .^ X ) e. ( H ` ( M x. N ) ) ) )
26 2 5 6 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
27 26 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
28 27 fveq2d 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( algSc ` P ) ` ( 1r ` ( Scalar ` P ) ) ) )
29 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
30 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
31 2 mpllmod 
 |-  ( ( I e. V /\ R e. Ring ) -> P e. LMod )
32 5 6 31 syl2anc 
 |-  ( ph -> P e. LMod )
33 2 mplring 
 |-  ( ( I e. V /\ R e. Ring ) -> P e. Ring )
34 5 6 33 syl2anc 
 |-  ( ph -> P e. Ring )
35 29 30 32 34 ascl1 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` ( Scalar ` P ) ) ) = ( 1r ` P ) )
36 28 35 eqtrd 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
37 eqid 
 |-  ( Base ` R ) = ( Base ` R )
38 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
39 37 38 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
40 6 39 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
41 1 2 29 37 5 6 40 mhpsclcl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. ( H ` 0 ) )
42 36 41 eqeltrrd 
 |-  ( ph -> ( 1r ` P ) e. ( H ` 0 ) )
43 eqid 
 |-  ( Base ` P ) = ( Base ` P )
44 1 2 43 5 6 7 9 mhpmpl 
 |-  ( ph -> X e. ( Base ` P ) )
45 3 43 mgpbas 
 |-  ( Base ` P ) = ( Base ` T )
46 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
47 3 46 ringidval 
 |-  ( 1r ` P ) = ( 0g ` T )
48 45 47 4 mulg0 
 |-  ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) )
49 44 48 syl 
 |-  ( ph -> ( 0 .^ X ) = ( 1r ` P ) )
50 7 nn0cnd 
 |-  ( ph -> M e. CC )
51 50 mul01d 
 |-  ( ph -> ( M x. 0 ) = 0 )
52 51 fveq2d 
 |-  ( ph -> ( H ` ( M x. 0 ) ) = ( H ` 0 ) )
53 42 49 52 3eltr4d 
 |-  ( ph -> ( 0 .^ X ) e. ( H ` ( M x. 0 ) ) )
54 eqid 
 |-  ( .r ` P ) = ( .r ` P )
55 5 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> I e. V )
56 6 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> R e. Ring )
57 7 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 9 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> X e. ( H ` M ) )
62 1 2 54 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 34 63 syl 
 |-  ( ph -> T e. Mnd )
65 64 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> T e. Mnd )
66 44 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) e. ( H ` ( M x. y ) ) ) -> X e. ( Base ` P ) )
67 3 54 mgpplusg 
 |-  ( .r ` P ) = ( +g ` T )
68 45 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 50 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 mulid1d 
 |-  ( ( ( 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 13 17 21 25 53 78 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( N .^ X ) e. ( H ` ( M x. N ) ) )
80 8 79 mpdan 
 |-  ( ph -> ( N .^ X ) e. ( H ` ( M x. N ) ) )