Proof of Theorem mhpind
Step | Hyp | Ref
| Expression |
1 | | mhpind.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
2 | | mhpind.z |
. . 3
⊢ 0 =
(0g‘𝑅) |
3 | | eqid 2735 |
. . 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 5346 |
. . 3
⊢ (𝜑 → 𝐷 ∈ V) |
8 | | ssrab2 4090 |
. . . 4
⊢ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} ⊆ 𝐷 |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} ⊆ 𝐷) |
10 | | mhpind.h |
. . . . 5
⊢ 𝐻 = (𝐼 mHomP 𝑅) |
11 | | reldmmhp 22159 |
. . . . . 6
⊢ Rel dom
mHomP |
12 | | mhpind.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) |
13 | 11, 10, 12 | elfvov1 7473 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ V) |
14 | 10, 12 | mhprcl 22165 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
15 | 10, 2, 5, 13, 4, 14 | mhp0cl 22168 |
. . . 4
⊢ (𝜑 → (𝐷 × { 0 }) ∈ (𝐻‘𝑁)) |
16 | | mhpind.0 |
. . . 4
⊢ (𝜑 → (𝐷 × { 0 }) ∈ 𝐺) |
17 | 15, 16 | elind 4210 |
. . 3
⊢ (𝜑 → (𝐷 × { 0 }) ∈ ((𝐻‘𝑁) ∩ 𝐺)) |
18 | | mhpind.s |
. . . . . 6
⊢ 𝑆 = {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} |
19 | 18 | eleq2i 2831 |
. . . . 5
⊢ (𝑎 ∈ 𝑆 ↔ 𝑎 ∈ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁}) |
20 | 19 | biimpri 228 |
. . . 4
⊢ (𝑎 ∈ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} → 𝑎 ∈ 𝑆) |
21 | | mhpind.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
22 | | eqid 2735 |
. . . . . 6
⊢
(Base‘𝑃) =
(Base‘𝑃) |
23 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → 𝑁 ∈
ℕ0) |
24 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑠 ∈ 𝐷) → 𝑏 ∈ 𝐵) |
25 | 1, 2 | grpidcl 18996 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
26 | 4, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ 𝐵) |
27 | 26 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑠 ∈ 𝐷) → 0 ∈ 𝐵) |
28 | 24, 27 | ifcld 4577 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑠 ∈ 𝐷) → if(𝑠 = 𝑎, 𝑏, 0 ) ∈ 𝐵) |
29 | 28 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )):𝐷⟶𝐵) |
30 | 1 | fvexi 6921 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
31 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ V) |
32 | 31, 7 | elmapd 8879 |
. . . . . . . . . 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 2735 |
. . . . . . . . . 10
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
36 | | eqid 2735 |
. . . . . . . . . 10
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
37 | 35, 1, 5, 36, 13 | psrbas 21971 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = (𝐵 ↑m 𝐷)) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (Base‘(𝐼 mPwSer 𝑅)) = (𝐵 ↑m 𝐷)) |
39 | 34, 38 | eleqtrrd 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈
(Base‘(𝐼 mPwSer 𝑅))) |
40 | 2 | fvexi 6921 |
. . . . . . . . . 10
⊢ 0 ∈
V |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ V) |
42 | | eqid 2735 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) = (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) |
43 | 7, 41, 42 | sniffsupp 9438 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) finSupp 0
) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) finSupp 0
) |
45 | 21, 35, 36, 2, 22 | mplelbas 22029 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈
(Base‘𝑃) ↔
((𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈
(Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) finSupp 0
)) |
46 | 39, 44, 45 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈
(Base‘𝑃)) |
47 | | elneeldif 3977 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑠 ∈ (𝐷 ∖ 𝑆)) → 𝑎 ≠ 𝑠) |
48 | 47 | necomd 2994 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑠 ∈ (𝐷 ∖ 𝑆)) → 𝑠 ≠ 𝑎) |
49 | 48 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑠 ∈ (𝐷 ∖ 𝑆)) → 𝑠 ≠ 𝑎) |
50 | 49 | adantlrr 721 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑠 ∈ (𝐷 ∖ 𝑆)) → 𝑠 ≠ 𝑎) |
51 | 50 | neneqd 2943 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑠 ∈ (𝐷 ∖ 𝑆)) → ¬ 𝑠 = 𝑎) |
52 | 51 | iffalsed 4542 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑠 ∈ (𝐷 ∖ 𝑆)) → if(𝑠 = 𝑎, 𝑏, 0 ) = 0 ) |
53 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → 𝐷 ∈ V) |
54 | 52, 53 | suppss2 8224 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → ((𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) supp 0 ) ⊆ 𝑆) |
55 | 54, 18 | sseqtrdi 4046 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → ((𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁}) |
56 | 10, 21, 22, 2, 5, 23, 46, 55 | ismhp2 22163 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ (𝐻‘𝑁)) |
57 | | mhpind.1 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐺) |
58 | 56, 57 | elind 4210 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ ((𝐻‘𝑁) ∩ 𝐺)) |
59 | 20, 58 | sylanr1 682 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ 𝐵)) → (𝑠 ∈ 𝐷 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ ((𝐻‘𝑁) ∩ 𝐺)) |
60 | | mhpind.a |
. . . . 5
⊢ + =
(+g‘𝑃) |
61 | | elinel1 4211 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) → 𝑥 ∈ (𝐻‘𝑁)) |
62 | 61 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → 𝑥 ∈ (𝐻‘𝑁)) |
63 | 10, 21, 22, 62 | mhpmpl 22166 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → 𝑥 ∈ (Base‘𝑃)) |
64 | | elinel1 4211 |
. . . . . . 7
⊢ (𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺) → 𝑦 ∈ (𝐻‘𝑁)) |
65 | 64 | ad2antll 729 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → 𝑦 ∈ (𝐻‘𝑁)) |
66 | 10, 21, 22, 65 | mhpmpl 22166 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → 𝑦 ∈ (Base‘𝑃)) |
67 | 21, 22, 3, 60, 63, 66 | mpladd 22047 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) = (𝑥 ∘f
(+g‘𝑅)𝑦)) |
68 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → 𝑅 ∈ Grp) |
69 | 10, 21, 60, 68, 62, 65 | mhpaddcl 22173 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ (𝐻‘𝑁)) |
70 | | mhpind.2 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ 𝐺) |
71 | 69, 70 | elind 4210 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 + 𝑦) ∈ ((𝐻‘𝑁) ∩ 𝐺)) |
72 | 67, 71 | eqeltrrd 2840 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ 𝐺) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ 𝐺))) → (𝑥 ∘f
(+g‘𝑅)𝑦) ∈ ((𝐻‘𝑁) ∩ 𝐺)) |
73 | 10, 21, 22, 12 | mhpmpl 22166 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑃)) |
74 | 21, 1, 22, 5, 73 | mplelf 22036 |
. . 3
⊢ (𝜑 → 𝑋:𝐷⟶𝐵) |
75 | 21, 22, 2, 73 | mplelsfi 22033 |
. . 3
⊢ (𝜑 → 𝑋 finSupp 0 ) |
76 | 10, 2, 5, 12 | mhpdeg 22167 |
. . 3
⊢ (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑁}) |
77 | 1, 2, 3, 4, 7, 9, 17, 59, 72, 74, 75, 76 | fsuppssind 42580 |
. 2
⊢ (𝜑 → 𝑋 ∈ ((𝐻‘𝑁) ∩ 𝐺)) |
78 | 77 | elin2d 4215 |
1
⊢ (𝜑 → 𝑋 ∈ 𝐺) |