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