Step | Hyp | Ref
| Expression |
1 | | mhpinvcl.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
2 | | mhpinvcl.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Grp) |
3 | | mhpinvcl.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
4 | 3 | mplgrp 19918 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp) → 𝑃 ∈ Grp) |
5 | 1, 2, 4 | syl2anc 584 |
. . 3
⊢ (𝜑 → 𝑃 ∈ Grp) |
6 | | mhpinvcl.h |
. . . 4
⊢ 𝐻 = (𝐼 mHomP 𝑅) |
7 | | eqid 2794 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
8 | | mhpinvcl.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
9 | | mhpinvcl.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) |
10 | 6, 3, 7, 1, 2, 8, 9 | mhpmpl 20018 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (Base‘𝑃)) |
11 | | mhpinvcl.m |
. . . 4
⊢ 𝑀 = (invg‘𝑃) |
12 | 7, 11 | grpinvcl 17908 |
. . 3
⊢ ((𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃)) → (𝑀‘𝑋) ∈ (Base‘𝑃)) |
13 | 5, 10, 12 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝑀‘𝑋) ∈ (Base‘𝑃)) |
14 | | eqid 2794 |
. . . . . . . 8
⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅) |
15 | | eqid 2794 |
. . . . . . . . . 10
⊢
(Base‘(𝐼
mPwSer 𝑅)) =
(Base‘(𝐼 mPwSer 𝑅)) |
16 | | eqid 2794 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
17 | 3, 14, 15, 16, 7 | mplbas 19897 |
. . . . . . . . 9
⊢
(Base‘𝑃) =
{𝑓 ∈
(Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)} |
18 | 17 | eqcomi 2803 |
. . . . . . . 8
⊢ {𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)} = (Base‘𝑃) |
19 | 14, 3, 18, 1, 2 | mplsubg 19905 |
. . . . . . 7
⊢ (𝜑 → {𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)} ∈ (SubGrp‘(𝐼 mPwSer 𝑅))) |
20 | 10, 17 | syl6eleq 2892 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ {𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)}) |
21 | | eqid 2794 |
. . . . . . . . 9
⊢ {𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)} = {𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)} |
22 | 3, 14, 15, 16, 21 | mplval 19896 |
. . . . . . . 8
⊢ 𝑃 = ((𝐼 mPwSer 𝑅) ↾s {𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)}) |
23 | | eqid 2794 |
. . . . . . . 8
⊢
(invg‘(𝐼 mPwSer 𝑅)) = (invg‘(𝐼 mPwSer 𝑅)) |
24 | 22, 23, 11 | subginv 18040 |
. . . . . . 7
⊢ (({𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)} ∈ (SubGrp‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 ∈ {𝑓 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∣ 𝑓 finSupp (0g‘𝑅)}) →
((invg‘(𝐼
mPwSer 𝑅))‘𝑋) = (𝑀‘𝑋)) |
25 | 19, 20, 24 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((invg‘(𝐼
mPwSer 𝑅))‘𝑋) = (𝑀‘𝑋)) |
26 | | eqid 2794 |
. . . . . . 7
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
27 | | eqid 2794 |
. . . . . . 7
⊢
(invg‘𝑅) = (invg‘𝑅) |
28 | 3, 14, 15, 16, 7 | mplelbas 19898 |
. . . . . . . . 9
⊢ (𝑋 ∈ (Base‘𝑃) ↔ (𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 finSupp (0g‘𝑅))) |
29 | 10, 28 | sylib 219 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 finSupp (0g‘𝑅))) |
30 | 29 | simpld 495 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅))) |
31 | 14, 1, 2, 26, 27, 15, 23, 30 | psrneg 19868 |
. . . . . 6
⊢ (𝜑 →
((invg‘(𝐼
mPwSer 𝑅))‘𝑋) =
((invg‘𝑅)
∘ 𝑋)) |
32 | 25, 31 | eqtr3d 2832 |
. . . . 5
⊢ (𝜑 → (𝑀‘𝑋) = ((invg‘𝑅) ∘ 𝑋)) |
33 | 32 | oveq1d 7034 |
. . . 4
⊢ (𝜑 → ((𝑀‘𝑋) supp (0g‘𝑅)) =
(((invg‘𝑅)
∘ 𝑋) supp
(0g‘𝑅))) |
34 | | fvexd 6556 |
. . . . 5
⊢ (𝜑 → (0g‘𝑅) ∈ V) |
35 | | eqid 2794 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
36 | 35, 27 | grpinvf 17907 |
. . . . . . 7
⊢ (𝑅 ∈ Grp →
(invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
37 | 2, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(invg‘𝑅):(Base‘𝑅)⟶(Base‘𝑅)) |
38 | 37 | ffnd 6386 |
. . . . 5
⊢ (𝜑 →
(invg‘𝑅)
Fn (Base‘𝑅)) |
39 | | fvexd 6556 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) ∈ V) |
40 | 3, 35, 7, 26, 10 | mplelf 19901 |
. . . . . 6
⊢ (𝜑 → 𝑋:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
41 | 40 | ffnd 6386 |
. . . . 5
⊢ (𝜑 → 𝑋 Fn {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
42 | | ovexd 7053 |
. . . . . 6
⊢ (𝜑 → (ℕ0
↑𝑚 𝐼) ∈ V) |
43 | 26, 42 | rabexd 5130 |
. . . . 5
⊢ (𝜑 → {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
44 | 34, 38, 39, 41, 43 | suppcofnd 7725 |
. . . 4
⊢ (𝜑 →
(((invg‘𝑅)
∘ 𝑋) supp
(0g‘𝑅)) =
{𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘(𝑋‘𝑥)) ≠ (0g‘𝑅))}) |
45 | | suppvalfn 7691 |
. . . . . 6
⊢ ((𝑋 Fn {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∧ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈ V ∧
(0g‘𝑅)
∈ V) → (𝑋 supp
(0g‘𝑅)) =
{𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ (𝑋‘𝑥) ≠ (0g‘𝑅)}) |
46 | 41, 43, 34, 45 | syl3anc 1364 |
. . . . 5
⊢ (𝜑 → (𝑋 supp (0g‘𝑅)) = {𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ (𝑋‘𝑥) ≠ (0g‘𝑅)}) |
47 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Grp) |
48 | 40 | ffvelrnda 6719 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑋‘𝑥) ∈ (Base‘𝑅)) |
49 | 35, 16 | grpidcl 17889 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Grp →
(0g‘𝑅)
∈ (Base‘𝑅)) |
50 | 47, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(0g‘𝑅)
∈ (Base‘𝑅)) |
51 | | eqid 2794 |
. . . . . . . . . . 11
⊢
(+g‘𝑅) = (+g‘𝑅) |
52 | 35, 51, 16, 27 | grpinvid1 17911 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Grp ∧ (𝑋‘𝑥) ∈ (Base‘𝑅) ∧ (0g‘𝑅) ∈ (Base‘𝑅)) →
(((invg‘𝑅)‘(𝑋‘𝑥)) = (0g‘𝑅) ↔ ((𝑋‘𝑥)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))) |
53 | 47, 48, 50, 52 | syl3anc 1364 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(((invg‘𝑅)‘(𝑋‘𝑥)) = (0g‘𝑅) ↔ ((𝑋‘𝑥)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅))) |
54 | 35, 51, 16 | grprid 17892 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Grp ∧ (𝑋‘𝑥) ∈ (Base‘𝑅)) → ((𝑋‘𝑥)(+g‘𝑅)(0g‘𝑅)) = (𝑋‘𝑥)) |
55 | 47, 48, 54 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑋‘𝑥)(+g‘𝑅)(0g‘𝑅)) = (𝑋‘𝑥)) |
56 | 55 | eqeq1d 2796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(((𝑋‘𝑥)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅) ↔ (𝑋‘𝑥) = (0g‘𝑅))) |
57 | 53, 56 | bitr2d 281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑋‘𝑥) = (0g‘𝑅) ↔ ((invg‘𝑅)‘(𝑋‘𝑥)) = (0g‘𝑅))) |
58 | 57 | necon3bid 3027 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑋‘𝑥) ≠ (0g‘𝑅) ↔ ((invg‘𝑅)‘(𝑋‘𝑥)) ≠ (0g‘𝑅))) |
59 | 48 | biantrurd 533 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(((invg‘𝑅)‘(𝑋‘𝑥)) ≠ (0g‘𝑅) ↔ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘(𝑋‘𝑥)) ≠ (0g‘𝑅)))) |
60 | 58, 59 | bitrd 280 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑋‘𝑥) ≠ (0g‘𝑅) ↔ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘(𝑋‘𝑥)) ≠ (0g‘𝑅)))) |
61 | 60 | rabbidva 3423 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ (𝑋‘𝑥) ≠ (0g‘𝑅)} = {𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘(𝑋‘𝑥)) ≠ (0g‘𝑅))}) |
62 | 46, 61 | eqtr2d 2831 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∣ ((𝑋‘𝑥) ∈ (Base‘𝑅) ∧ ((invg‘𝑅)‘(𝑋‘𝑥)) ≠ (0g‘𝑅))} = (𝑋 supp (0g‘𝑅))) |
63 | 33, 44, 62 | 3eqtrd 2834 |
. . 3
⊢ (𝜑 → ((𝑀‘𝑋) supp (0g‘𝑅)) = (𝑋 supp (0g‘𝑅))) |
64 | | eqid 2794 |
. . . 4
⊢ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
65 | 6, 16, 64, 1, 2, 8,
9 | mhpdeg 20019 |
. . 3
⊢ (𝜑 → (𝑋 supp (0g‘𝑅)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣
Σ𝑗 ∈
ℕ0 (𝑔‘𝑗) = 𝑁}) |
66 | 63, 65 | eqsstrd 3928 |
. 2
⊢ (𝜑 → ((𝑀‘𝑋) supp (0g‘𝑅)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣
Σ𝑗 ∈
ℕ0 (𝑔‘𝑗) = 𝑁}) |
67 | 6, 3, 7, 16, 64, 1, 2, 8 | ismhp 20017 |
. 2
⊢ (𝜑 → ((𝑀‘𝑋) ∈ (𝐻‘𝑁) ↔ ((𝑀‘𝑋) ∈ (Base‘𝑃) ∧ ((𝑀‘𝑋) supp (0g‘𝑅)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} ∣
Σ𝑗 ∈
ℕ0 (𝑔‘𝑗) = 𝑁}))) |
68 | 13, 66, 67 | mpbir2and 709 |
1
⊢ (𝜑 → (𝑀‘𝑋) ∈ (𝐻‘𝑁)) |