Proof of Theorem mdegldg
Step | Hyp | Ref
| Expression |
1 | | mdegval.d |
. . . . 5
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
2 | | mdegval.p |
. . . . 5
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
3 | | mdegval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑃) |
4 | | mdegval.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
5 | | mdegval.a |
. . . . 5
⊢ 𝐴 = {𝑚 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑚 “ ℕ) ∈
Fin} |
6 | | mdegval.h |
. . . . 5
⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) |
7 | 1, 2, 3, 4, 5, 6 | mdegval 23627 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
8 | 7 | 3ad2ant2 1076 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
9 | 2, 3 | mplrcl 19311 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) |
10 | 9 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐼 ∈ V) |
11 | 5, 6 | tdeglem1 23622 |
. . . . . . 7
⊢ (𝐼 ∈ V → 𝐻:𝐴⟶ℕ0) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐻:𝐴⟶ℕ0) |
13 | 12 | ffund 5962 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → Fun 𝐻) |
14 | | simp2 1055 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 ∈ 𝐵) |
15 | | simp1 1054 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝑅 ∈ Ring) |
16 | 2, 3, 4, 14, 15 | mplelsfi 19312 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 finSupp 0 ) |
17 | 16 | fsuppimpd 8165 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐹 supp 0 ) ∈
Fin) |
18 | | imafi 8142 |
. . . . 5
⊢ ((Fun
𝐻 ∧ (𝐹 supp 0 ) ∈ Fin) →
(𝐻 “ (𝐹 supp 0 )) ∈
Fin) |
19 | 13, 17, 18 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ∈
Fin) |
20 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 ≠ 𝑌) |
21 | | mdegldg.y |
. . . . . . . 8
⊢ 𝑌 = (0g‘𝑃) |
22 | | ringgrp 18375 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
23 | 22 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝑅 ∈ Grp) |
24 | 2, 5, 4, 21, 10, 23 | mpl0 19262 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝑌 = (𝐴 × { 0 })) |
25 | 20, 24 | neeqtrd 2851 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 ≠ (𝐴 × { 0 })) |
26 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
27 | 2, 26, 3, 5, 14 | mplelf 19254 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹:𝐴⟶(Base‘𝑅)) |
28 | 27 | ffnd 5959 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 Fn 𝐴) |
29 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝑅) ∈ V |
30 | 4, 29 | eqeltri 2684 |
. . . . . . . 8
⊢ 0 ∈
V |
31 | | ovex 6577 |
. . . . . . . . . 10
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
32 | 5, 31 | rabex2 4742 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
33 | | fnsuppeq0 7210 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → ((𝐹 supp 0 ) = ∅ ↔ 𝐹 = (𝐴 × { 0 }))) |
34 | 32, 33 | mp3an2 1404 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 0 ∈ V) → ((𝐹 supp 0 ) = ∅ ↔ 𝐹 = (𝐴 × { 0 }))) |
35 | 28, 30, 34 | sylancl 693 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐹 supp 0 ) = ∅ ↔ 𝐹 = (𝐴 × { 0 }))) |
36 | 35 | necon3bid 2826 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐹 supp 0 ) ≠ ∅ ↔
𝐹 ≠ (𝐴 × { 0 }))) |
37 | 25, 36 | mpbird 246 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐹 supp 0 ) ≠
∅) |
38 | 12 | ffnd 5959 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐻 Fn 𝐴) |
39 | | suppssdm 7195 |
. . . . . . . 8
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
40 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶(Base‘𝑅) → dom 𝐹 = 𝐴) |
41 | 27, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → dom 𝐹 = 𝐴) |
42 | 39, 41 | syl5sseq 3616 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐹 supp 0 ) ⊆ 𝐴) |
43 | | fnimaeq0 5926 |
. . . . . . 7
⊢ ((𝐻 Fn 𝐴 ∧ (𝐹 supp 0 ) ⊆ 𝐴) → ((𝐻 “ (𝐹 supp 0 )) = ∅ ↔ (𝐹 supp 0 ) =
∅)) |
44 | 38, 42, 43 | syl2anc 691 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐻 “ (𝐹 supp 0 )) = ∅ ↔ (𝐹 supp 0 ) =
∅)) |
45 | 44 | necon3bid 2826 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐻 “ (𝐹 supp 0 )) ≠ ∅ ↔
(𝐹 supp 0 ) ≠
∅)) |
46 | 37, 45 | mpbird 246 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ≠
∅) |
47 | | imassrn 5396 |
. . . . . 6
⊢ (𝐻 “ (𝐹 supp 0 )) ⊆ ran 𝐻 |
48 | | frn 5966 |
. . . . . . 7
⊢ (𝐻:𝐴⟶ℕ0 → ran 𝐻 ⊆
ℕ0) |
49 | 12, 48 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ran 𝐻 ⊆
ℕ0) |
50 | 47, 49 | syl5ss 3579 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ⊆
ℕ0) |
51 | | nn0ssre 11173 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ |
52 | | ressxr 9962 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
53 | 51, 52 | sstri 3577 |
. . . . 5
⊢
ℕ0 ⊆ ℝ* |
54 | 50, 53 | syl6ss 3580 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*) |
55 | | xrltso 11850 |
. . . . 5
⊢ < Or
ℝ* |
56 | | fisupcl 8258 |
. . . . 5
⊢ (( <
Or ℝ* ∧ ((𝐻 “ (𝐹 supp 0 )) ∈ Fin ∧ (𝐻 “ (𝐹 supp 0 )) ≠ ∅ ∧
(𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*)) → sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ∈ (𝐻 “
(𝐹 supp 0 ))) |
57 | 55, 56 | mpan 702 |
. . . 4
⊢ (((𝐻 “ (𝐹 supp 0 )) ∈ Fin ∧ (𝐻 “ (𝐹 supp 0 )) ≠ ∅ ∧
(𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*) → sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ∈ (𝐻 “
(𝐹 supp 0 ))) |
58 | 19, 46, 54, 57 | syl3anc 1318 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ∈ (𝐻 “
(𝐹 supp 0 ))) |
59 | 8, 58 | eqeltrd 2688 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐷‘𝐹) ∈ (𝐻 “ (𝐹 supp 0 ))) |
60 | | fvelimab 6163 |
. . . 4
⊢ ((𝐻 Fn 𝐴 ∧ (𝐹 supp 0 ) ⊆ 𝐴) → ((𝐷‘𝐹) ∈ (𝐻 “ (𝐹 supp 0 )) ↔ ∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹))) |
61 | 38, 42, 60 | syl2anc 691 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐷‘𝐹) ∈ (𝐻 “ (𝐹 supp 0 )) ↔ ∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹))) |
62 | | rexsupp 7200 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) →
(∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
63 | 32, 30, 62 | mp3an23 1408 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
64 | 28, 63 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
65 | 61, 64 | bitrd 267 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐷‘𝐹) ∈ (𝐻 “ (𝐹 supp 0 )) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
66 | 59, 65 | mpbid 221 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹))) |