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