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
↑m 𝐼)
∣ (◡𝑚 “ ℕ) ∈
Fin} |
| 6 | | mdegval.h |
. . . . 5
⊢ 𝐻 = (ℎ ∈ 𝐴 ↦ (ℂfld
Σg ℎ)) |
| 7 | 1, 2, 3, 4, 5, 6 | mdegval 26102 |
. . . 4
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
| 8 | 7 | 3ad2ant2 1135 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐷‘𝐹) = sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< )) |
| 9 | 5, 6 | tdeglem1 26097 |
. . . . . . 7
⊢ 𝐻:𝐴⟶ℕ0 |
| 10 | 9 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐻:𝐴⟶ℕ0) |
| 11 | 10 | ffund 6740 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → Fun 𝐻) |
| 12 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 ∈ 𝐵) |
| 13 | 2, 3, 4, 12 | mplelsfi 22015 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 finSupp 0 ) |
| 14 | 13 | fsuppimpd 9409 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐹 supp 0 ) ∈
Fin) |
| 15 | | imafi 9353 |
. . . . 5
⊢ ((Fun
𝐻 ∧ (𝐹 supp 0 ) ∈ Fin) →
(𝐻 “ (𝐹 supp 0 )) ∈
Fin) |
| 16 | 11, 14, 15 | syl2anc 584 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ∈
Fin) |
| 17 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 ≠ 𝑌) |
| 18 | | mdegldg.y |
. . . . . . . 8
⊢ 𝑌 = (0g‘𝑃) |
| 19 | 2, 3 | mplrcl 22014 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝐵 → 𝐼 ∈ V) |
| 20 | 19 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐼 ∈ V) |
| 21 | | ringgrp 20235 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 22 | 21 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝑅 ∈ Grp) |
| 23 | 2, 5, 4, 18, 20, 22 | mpl0 22026 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝑌 = (𝐴 × { 0 })) |
| 24 | 17, 23 | neeqtrd 3010 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 ≠ (𝐴 × { 0 })) |
| 25 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 26 | 2, 25, 3, 5, 12 | mplelf 22018 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹:𝐴⟶(Base‘𝑅)) |
| 27 | 26 | ffnd 6737 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐹 Fn 𝐴) |
| 28 | 4 | fvexi 6920 |
. . . . . . . 8
⊢ 0 ∈
V |
| 29 | | ovex 7464 |
. . . . . . . . . 10
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 30 | 5, 29 | rabex2 5341 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
| 31 | | fnsuppeq0 8217 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) → ((𝐹 supp 0 ) = ∅ ↔ 𝐹 = (𝐴 × { 0 }))) |
| 32 | 30, 31 | mp3an2 1451 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 0 ∈ V) → ((𝐹 supp 0 ) = ∅ ↔ 𝐹 = (𝐴 × { 0 }))) |
| 33 | 27, 28, 32 | sylancl 586 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐹 supp 0 ) = ∅ ↔ 𝐹 = (𝐴 × { 0 }))) |
| 34 | 33 | necon3bid 2985 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐹 supp 0 ) ≠ ∅ ↔
𝐹 ≠ (𝐴 × { 0 }))) |
| 35 | 24, 34 | mpbird 257 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐹 supp 0 ) ≠
∅) |
| 36 | 10 | ffnd 6737 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → 𝐻 Fn 𝐴) |
| 37 | | suppssdm 8202 |
. . . . . . . 8
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
| 38 | 37, 26 | fssdm 6755 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐹 supp 0 ) ⊆ 𝐴) |
| 39 | | fnimaeq0 6701 |
. . . . . . 7
⊢ ((𝐻 Fn 𝐴 ∧ (𝐹 supp 0 ) ⊆ 𝐴) → ((𝐻 “ (𝐹 supp 0 )) = ∅ ↔ (𝐹 supp 0 ) =
∅)) |
| 40 | 36, 38, 39 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐻 “ (𝐹 supp 0 )) = ∅ ↔ (𝐹 supp 0 ) =
∅)) |
| 41 | 40 | necon3bid 2985 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐻 “ (𝐹 supp 0 )) ≠ ∅ ↔
(𝐹 supp 0 ) ≠
∅)) |
| 42 | 35, 41 | mpbird 257 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ≠
∅) |
| 43 | | imassrn 6089 |
. . . . . 6
⊢ (𝐻 “ (𝐹 supp 0 )) ⊆ ran 𝐻 |
| 44 | 10 | frnd 6744 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ran 𝐻 ⊆
ℕ0) |
| 45 | 43, 44 | sstrid 3995 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ⊆
ℕ0) |
| 46 | | nn0ssre 12530 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ |
| 47 | | ressxr 11305 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
| 48 | 46, 47 | sstri 3993 |
. . . . 5
⊢
ℕ0 ⊆ ℝ* |
| 49 | 45, 48 | sstrdi 3996 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*) |
| 50 | | xrltso 13183 |
. . . . 5
⊢ < Or
ℝ* |
| 51 | | fisupcl 9509 |
. . . . 5
⊢ (( <
Or ℝ* ∧ ((𝐻 “ (𝐹 supp 0 )) ∈ Fin ∧ (𝐻 “ (𝐹 supp 0 )) ≠ ∅ ∧
(𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*)) → sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ∈ (𝐻 “
(𝐹 supp 0 ))) |
| 52 | 50, 51 | mpan 690 |
. . . 4
⊢ (((𝐻 “ (𝐹 supp 0 )) ∈ Fin ∧ (𝐻 “ (𝐹 supp 0 )) ≠ ∅ ∧
(𝐻 “ (𝐹 supp 0 )) ⊆
ℝ*) → sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ∈ (𝐻 “
(𝐹 supp 0 ))) |
| 53 | 16, 42, 49, 52 | syl3anc 1373 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → sup((𝐻 “ (𝐹 supp 0 )), ℝ*,
< ) ∈ (𝐻 “
(𝐹 supp 0 ))) |
| 54 | 8, 53 | eqeltrd 2841 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (𝐷‘𝐹) ∈ (𝐻 “ (𝐹 supp 0 ))) |
| 55 | 36, 38 | fvelimabd 6982 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐷‘𝐹) ∈ (𝐻 “ (𝐹 supp 0 )) ↔ ∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹))) |
| 56 | | rexsupp 8207 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 0 ∈ V) →
(∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
| 57 | 30, 28, 56 | mp3an23 1455 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
| 58 | 27, 57 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → (∃𝑥 ∈ (𝐹 supp 0 )(𝐻‘𝑥) = (𝐷‘𝐹) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
| 59 | 55, 58 | bitrd 279 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ((𝐷‘𝐹) ∈ (𝐻 “ (𝐹 supp 0 )) ↔ ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹)))) |
| 60 | 54, 59 | mpbid 232 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 𝑌) → ∃𝑥 ∈ 𝐴 ((𝐹‘𝑥) ≠ 0 ∧ (𝐻‘𝑥) = (𝐷‘𝐹))) |