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 𝐻 = ( 𝐼 mHomP 𝑅 )
mhppwdeg.p 𝑃 = ( 𝐼 mPoly 𝑅 )
mhppwdeg.t 𝑇 = ( mulGrp ‘ 𝑃 )
mhppwdeg.e = ( .g𝑇 )
mhppwdeg.r ( 𝜑𝑅 ∈ Ring )
mhppwdeg.n ( 𝜑𝑁 ∈ ℕ0 )
mhppwdeg.x ( 𝜑𝑋 ∈ ( 𝐻𝑀 ) )
Assertion mhppwdeg ( 𝜑 → ( 𝑁 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 mhppwdeg.h 𝐻 = ( 𝐼 mHomP 𝑅 )
2 mhppwdeg.p 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mhppwdeg.t 𝑇 = ( mulGrp ‘ 𝑃 )
4 mhppwdeg.e = ( .g𝑇 )
5 mhppwdeg.r ( 𝜑𝑅 ∈ Ring )
6 mhppwdeg.n ( 𝜑𝑁 ∈ ℕ0 )
7 mhppwdeg.x ( 𝜑𝑋 ∈ ( 𝐻𝑀 ) )
8 oveq1 ( 𝑥 = 0 → ( 𝑥 𝑋 ) = ( 0 𝑋 ) )
9 oveq2 ( 𝑥 = 0 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 0 ) )
10 9 fveq2d ( 𝑥 = 0 → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · 0 ) ) )
11 8 10 eleq12d ( 𝑥 = 0 → ( ( 𝑥 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( 0 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 0 ) ) ) )
12 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 𝑋 ) = ( 𝑦 𝑋 ) )
13 oveq2 ( 𝑥 = 𝑦 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 𝑦 ) )
14 13 fveq2d ( 𝑥 = 𝑦 → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) )
15 12 14 eleq12d ( 𝑥 = 𝑦 → ( ( 𝑥 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) )
16 oveq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 𝑋 ) = ( ( 𝑦 + 1 ) 𝑋 ) )
17 oveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑀 · 𝑥 ) = ( 𝑀 · ( 𝑦 + 1 ) ) )
18 17 fveq2d ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) )
19 16 18 eleq12d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( ( 𝑦 + 1 ) 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) ) )
20 oveq1 ( 𝑥 = 𝑁 → ( 𝑥 𝑋 ) = ( 𝑁 𝑋 ) )
21 oveq2 ( 𝑥 = 𝑁 → ( 𝑀 · 𝑥 ) = ( 𝑀 · 𝑁 ) )
22 21 fveq2d ( 𝑥 = 𝑁 → ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )
23 20 22 eleq12d ( 𝑥 = 𝑁 → ( ( 𝑥 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑥 ) ) ↔ ( 𝑁 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) ) )
24 reldmmhp Rel dom mHomP
25 24 1 7 elfvov1 ( 𝜑𝐼 ∈ V )
26 2 25 5 mplsca ( 𝜑𝑅 = ( Scalar ‘ 𝑃 ) )
27 26 fveq2d ( 𝜑 → ( 1r𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
28 27 fveq2d ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r𝑅 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) )
29 eqid ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
30 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
31 2 25 5 mpllmodd ( 𝜑𝑃 ∈ LMod )
32 2 25 5 mplringd ( 𝜑𝑃 ∈ Ring )
33 29 30 31 32 ascl1 ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) = ( 1r𝑃 ) )
34 28 33 eqtrd ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r𝑅 ) ) = ( 1r𝑃 ) )
35 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
36 eqid ( 1r𝑅 ) = ( 1r𝑅 )
37 35 36 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
38 5 37 syl ( 𝜑 → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
39 1 2 29 35 25 5 38 mhpsclcl ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r𝑅 ) ) ∈ ( 𝐻 ‘ 0 ) )
40 34 39 eqeltrrd ( 𝜑 → ( 1r𝑃 ) ∈ ( 𝐻 ‘ 0 ) )
41 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
42 1 2 41 7 mhpmpl ( 𝜑𝑋 ∈ ( Base ‘ 𝑃 ) )
43 3 41 mgpbas ( Base ‘ 𝑃 ) = ( Base ‘ 𝑇 )
44 eqid ( 1r𝑃 ) = ( 1r𝑃 )
45 3 44 ringidval ( 1r𝑃 ) = ( 0g𝑇 )
46 43 45 4 mulg0 ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 𝑋 ) = ( 1r𝑃 ) )
47 42 46 syl ( 𝜑 → ( 0 𝑋 ) = ( 1r𝑃 ) )
48 1 7 mhprcl ( 𝜑𝑀 ∈ ℕ0 )
49 48 nn0cnd ( 𝜑𝑀 ∈ ℂ )
50 49 mul01d ( 𝜑 → ( 𝑀 · 0 ) = 0 )
51 50 fveq2d ( 𝜑 → ( 𝐻 ‘ ( 𝑀 · 0 ) ) = ( 𝐻 ‘ 0 ) )
52 40 47 51 3eltr4d ( 𝜑 → ( 0 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 0 ) ) )
53 eqid ( .r𝑃 ) = ( .r𝑃 )
54 5 ad2antrr ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑅 ∈ Ring )
55 simpr ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) )
56 7 ad2antrr ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑋 ∈ ( 𝐻𝑀 ) )
57 1 2 53 54 55 56 mhpmulcl ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑦 𝑋 ) ( .r𝑃 ) 𝑋 ) ∈ ( 𝐻 ‘ ( ( 𝑀 · 𝑦 ) + 𝑀 ) ) )
58 3 ringmgp ( 𝑃 ∈ Ring → 𝑇 ∈ Mnd )
59 32 58 syl ( 𝜑𝑇 ∈ Mnd )
60 59 ad2antrr ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑇 ∈ Mnd )
61 simplr ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑦 ∈ ℕ0 )
62 42 ad2antrr ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
63 3 53 mgpplusg ( .r𝑃 ) = ( +g𝑇 )
64 43 4 63 mulgnn0p1 ( ( 𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑦 + 1 ) 𝑋 ) = ( ( 𝑦 𝑋 ) ( .r𝑃 ) 𝑋 ) )
65 60 61 62 64 syl3anc ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑦 + 1 ) 𝑋 ) = ( ( 𝑦 𝑋 ) ( .r𝑃 ) 𝑋 ) )
66 49 ad2antrr ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑀 ∈ ℂ )
67 61 nn0cnd ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 𝑦 ∈ ℂ )
68 1cnd ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → 1 ∈ ℂ )
69 66 67 68 adddid ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑀 · ( 𝑦 + 1 ) ) = ( ( 𝑀 · 𝑦 ) + ( 𝑀 · 1 ) ) )
70 66 mulridd ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑀 · 1 ) = 𝑀 )
71 70 oveq2d ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑀 · 𝑦 ) + ( 𝑀 · 1 ) ) = ( ( 𝑀 · 𝑦 ) + 𝑀 ) )
72 69 71 eqtrd ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝑀 · ( 𝑦 + 1 ) ) = ( ( 𝑀 · 𝑦 ) + 𝑀 ) )
73 72 fveq2d ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) = ( 𝐻 ‘ ( ( 𝑀 · 𝑦 ) + 𝑀 ) ) )
74 57 65 73 3eltr4d ( ( ( 𝜑𝑦 ∈ ℕ0 ) ∧ ( 𝑦 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑦 ) ) ) → ( ( 𝑦 + 1 ) 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · ( 𝑦 + 1 ) ) ) )
75 11 15 19 23 52 74 nn0indd ( ( 𝜑𝑁 ∈ ℕ0 ) → ( 𝑁 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )
76 6 75 mpdan ( 𝜑 → ( 𝑁 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) )