| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mhpind.h |
⊢ 𝐻 = ( 𝐼 mHomP 𝑅 ) |
| 2 |
|
mhpind.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
| 3 |
|
mhpind.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
| 4 |
|
mhpind.p |
⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) |
| 5 |
|
mhpind.a |
⊢ + = ( +g ‘ 𝑃 ) |
| 6 |
|
mhpind.d |
⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } |
| 7 |
|
mhpind.s |
⊢ 𝑆 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } |
| 8 |
|
mhpind.r |
⊢ ( 𝜑 → 𝑅 ∈ Grp ) |
| 9 |
|
mhpind.x |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 10 |
|
mhpind.0 |
⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ 𝐺 ) |
| 11 |
|
mhpind.1 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ 𝐺 ) |
| 12 |
|
mhpind.2 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐺 ) |
| 13 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
| 14 |
|
ovexd |
⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V ) |
| 15 |
6 14
|
rabexd |
⊢ ( 𝜑 → 𝐷 ∈ V ) |
| 16 |
|
ssrab2 |
⊢ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ⊆ 𝐷 |
| 17 |
16
|
a1i |
⊢ ( 𝜑 → { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ⊆ 𝐷 ) |
| 18 |
|
reldmmhp |
⊢ Rel dom mHomP |
| 19 |
18 1 9
|
elfvov1 |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
| 20 |
1 9
|
mhprcl |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
| 21 |
1 3 6 19 8 20
|
mhp0cl |
⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 22 |
21 10
|
elind |
⊢ ( 𝜑 → ( 𝐷 × { 0 } ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) |
| 23 |
7
|
eleq2i |
⊢ ( 𝑎 ∈ 𝑆 ↔ 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
| 24 |
23
|
biimpri |
⊢ ( 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } → 𝑎 ∈ 𝑆 ) |
| 25 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
| 26 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑁 ∈ ℕ0 ) |
| 27 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝐷 ) → 𝑏 ∈ 𝐵 ) |
| 28 |
2 3
|
grpidcl |
⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 ) |
| 29 |
8 28
|
syl |
⊢ ( 𝜑 → 0 ∈ 𝐵 ) |
| 30 |
29
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝐷 ) → 0 ∈ 𝐵 ) |
| 31 |
27 30
|
ifcld |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ 𝐷 ) → if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ∈ 𝐵 ) |
| 32 |
31
|
fmpttd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝐷 ⟶ 𝐵 ) |
| 33 |
2
|
fvexi |
⊢ 𝐵 ∈ V |
| 34 |
33
|
a1i |
⊢ ( 𝜑 → 𝐵 ∈ V ) |
| 35 |
34 15
|
elmapd |
⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐵 ↑m 𝐷 ) ↔ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝐷 ⟶ 𝐵 ) ) |
| 36 |
35
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐵 ↑m 𝐷 ) ↔ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) : 𝐷 ⟶ 𝐵 ) ) |
| 37 |
32 36
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐵 ↑m 𝐷 ) ) |
| 38 |
|
eqid |
⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 ) |
| 39 |
|
eqid |
⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) |
| 40 |
38 2 6 39 19
|
psrbas |
⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐵 ↑m 𝐷 ) ) |
| 41 |
40
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐵 ↑m 𝐷 ) ) |
| 42 |
37 41
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) |
| 43 |
3
|
fvexi |
⊢ 0 ∈ V |
| 44 |
43
|
a1i |
⊢ ( 𝜑 → 0 ∈ V ) |
| 45 |
|
eqid |
⊢ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) = ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) |
| 46 |
15 44 45
|
sniffsupp |
⊢ ( 𝜑 → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) finSupp 0 ) |
| 47 |
46
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) finSupp 0 ) |
| 48 |
4 38 39 3 25
|
mplelbas |
⊢ ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ 𝑃 ) ↔ ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) finSupp 0 ) ) |
| 49 |
42 47 48
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( Base ‘ 𝑃 ) ) |
| 50 |
|
elneeldif |
⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑎 ≠ 𝑠 ) |
| 51 |
50
|
necomd |
⊢ ( ( 𝑎 ∈ 𝑆 ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑠 ≠ 𝑎 ) |
| 52 |
51
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑠 ≠ 𝑎 ) |
| 53 |
52
|
adantlrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → 𝑠 ≠ 𝑎 ) |
| 54 |
53
|
neneqd |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → ¬ 𝑠 = 𝑎 ) |
| 55 |
54
|
iffalsed |
⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) ∧ 𝑠 ∈ ( 𝐷 ∖ 𝑆 ) ) → if ( 𝑠 = 𝑎 , 𝑏 , 0 ) = 0 ) |
| 56 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐷 ∈ V ) |
| 57 |
55 56
|
suppss2 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) supp 0 ) ⊆ 𝑆 ) |
| 58 |
57 7
|
sseqtrdi |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
| 59 |
1 4 25 3 6 26 49 58
|
ismhp2 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 60 |
59 11
|
elind |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) |
| 61 |
24 60
|
sylanr1 |
⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑠 ∈ 𝐷 ↦ if ( 𝑠 = 𝑎 , 𝑏 , 0 ) ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) |
| 62 |
|
elinel1 |
⊢ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 63 |
62
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 64 |
1 4 25 63
|
mhpmpl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) ) |
| 65 |
|
elinel1 |
⊢ ( 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 66 |
65
|
ad2antll |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 67 |
1 4 25 66
|
mhpmpl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑃 ) ) |
| 68 |
4 25 13 5 64 67
|
mpladd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ) |
| 69 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → 𝑅 ∈ Grp ) |
| 70 |
1 4 5 69 63 66
|
mhpaddcl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ) |
| 71 |
70 12
|
elind |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) |
| 72 |
68 71
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) ) → ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) |
| 73 |
1 4 25 9
|
mhpmpl |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) ) |
| 74 |
4 2 25 6 73
|
mplelf |
⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ 𝐵 ) |
| 75 |
4 25 3 73
|
mplelsfi |
⊢ ( 𝜑 → 𝑋 finSupp 0 ) |
| 76 |
1 3 6 9
|
mhpdeg |
⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) |
| 77 |
2 3 13 8 15 17 22 61 72 74 75 76
|
fsuppssind |
⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ 𝐺 ) ) |
| 78 |
77
|
elin2d |
⊢ ( 𝜑 → 𝑋 ∈ 𝐺 ) |