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