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=ImHomPR
mhppwdeg.p P=ImPolyR
mhppwdeg.t T=mulGrpP
mhppwdeg.e ×˙=T
mhppwdeg.i φIV
mhppwdeg.r φRRing
mhppwdeg.m φM0
mhppwdeg.n φN0
mhppwdeg.x φXHM
Assertion mhppwdeg φN×˙XH M N

Proof

Step Hyp Ref Expression
1 mhppwdeg.h H=ImHomPR
2 mhppwdeg.p P=ImPolyR
3 mhppwdeg.t T=mulGrpP
4 mhppwdeg.e ×˙=T
5 mhppwdeg.i φIV
6 mhppwdeg.r φRRing
7 mhppwdeg.m φM0
8 mhppwdeg.n φN0
9 mhppwdeg.x φXHM
10 oveq1 x=0x×˙X=0×˙X
11 oveq2 x=0Mx= M0
12 11 fveq2d x=0HMx=H M0
13 10 12 eleq12d x=0x×˙XHMx0×˙XH M0
14 oveq1 x=yx×˙X=y×˙X
15 oveq2 x=yMx=My
16 15 fveq2d x=yHMx=HMy
17 14 16 eleq12d x=yx×˙XHMxy×˙XHMy
18 oveq1 x=y+1x×˙X=y+1×˙X
19 oveq2 x=y+1Mx=My+1
20 19 fveq2d x=y+1HMx=HMy+1
21 18 20 eleq12d x=y+1x×˙XHMxy+1×˙XHMy+1
22 oveq1 x=Nx×˙X=N×˙X
23 oveq2 x=NMx= M N
24 23 fveq2d x=NHMx=H M N
25 22 24 eleq12d x=Nx×˙XHMxN×˙XH M N
26 2 5 6 mplsca φR=ScalarP
27 26 fveq2d φ1R=1ScalarP
28 27 fveq2d φalgScP1R=algScP1ScalarP
29 eqid algScP=algScP
30 eqid ScalarP=ScalarP
31 2 mpllmod IVRRingPLMod
32 5 6 31 syl2anc φPLMod
33 2 mplring IVRRingPRing
34 5 6 33 syl2anc φPRing
35 29 30 32 34 ascl1 φalgScP1ScalarP=1P
36 28 35 eqtrd φalgScP1R=1P
37 eqid BaseR=BaseR
38 eqid 1R=1R
39 37 38 ringidcl RRing1RBaseR
40 6 39 syl φ1RBaseR
41 1 2 29 37 5 6 40 mhpsclcl φalgScP1RH0
42 36 41 eqeltrrd φ1PH0
43 eqid BaseP=BaseP
44 1 2 43 5 6 7 9 mhpmpl φXBaseP
45 3 43 mgpbas BaseP=BaseT
46 eqid 1P=1P
47 3 46 ringidval 1P=0T
48 45 47 4 mulg0 XBaseP0×˙X=1P
49 44 48 syl φ0×˙X=1P
50 7 nn0cnd φM
51 50 mul01d φ M0=0
52 51 fveq2d φH M0=H0
53 42 49 52 3eltr4d φ0×˙XH M0
54 eqid P=P
55 5 ad2antrr φy0y×˙XHMyIV
56 6 ad2antrr φy0y×˙XHMyRRing
57 7 ad2antrr φy0y×˙XHMyM0
58 simplr φy0y×˙XHMyy0
59 57 58 nn0mulcld φy0y×˙XHMyMy0
60 simpr φy0y×˙XHMyy×˙XHMy
61 9 ad2antrr φy0y×˙XHMyXHM
62 1 2 54 55 56 59 57 60 61 mhpmulcl φy0y×˙XHMyy×˙XPXHMy+M
63 3 ringmgp PRingTMnd
64 34 63 syl φTMnd
65 64 ad2antrr φy0y×˙XHMyTMnd
66 44 ad2antrr φy0y×˙XHMyXBaseP
67 3 54 mgpplusg P=+T
68 45 4 67 mulgnn0p1 TMndy0XBasePy+1×˙X=y×˙XPX
69 65 58 66 68 syl3anc φy0y×˙XHMyy+1×˙X=y×˙XPX
70 50 ad2antrr φy0y×˙XHMyM
71 58 nn0cnd φy0y×˙XHMyy
72 1cnd φy0y×˙XHMy1
73 70 71 72 adddid φy0y×˙XHMyMy+1=My+ M1
74 70 mulid1d φy0y×˙XHMy M1=M
75 74 oveq2d φy0y×˙XHMyMy+ M1=My+M
76 73 75 eqtrd φy0y×˙XHMyMy+1=My+M
77 76 fveq2d φy0y×˙XHMyHMy+1=HMy+M
78 62 69 77 3eltr4d φy0y×˙XHMyy+1×˙XHMy+1
79 13 17 21 25 53 78 nn0indd φN0N×˙XH M N
80 8 79 mpdan φN×˙XH M N