| 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 |
⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( 𝐻 ‘ ( 𝑀 · 𝑁 ) ) ) |