| Step | Hyp | Ref
| Expression |
| 1 | | deg1z.d |
. . . 4
⊢ 𝐷 = (deg1‘𝑅) |
| 2 | 1 | deg1fval 26119 |
. . 3
⊢ 𝐷 = (1o mDeg 𝑅) |
| 3 | | eqid 2737 |
. . 3
⊢
(1o mPoly 𝑅) = (1o mPoly 𝑅) |
| 4 | | deg1z.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
| 5 | | deg1nn0cl.b |
. . . 4
⊢ 𝐵 = (Base‘𝑃) |
| 6 | 4, 5 | ply1bas 22196 |
. . 3
⊢ 𝐵 = (Base‘(1o
mPoly 𝑅)) |
| 7 | | deg1ldg.y |
. . 3
⊢ 𝑌 = (0g‘𝑅) |
| 8 | | psr1baslem 22186 |
. . 3
⊢
(ℕ0 ↑m 1o) = {𝑐 ∈ (ℕ0
↑m 1o) ∣ (◡𝑐 “ ℕ) ∈
Fin} |
| 9 | | tdeglem2 26100 |
. . 3
⊢ (𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0
↑m 1o) ↦ (ℂfld
Σg 𝑎)) |
| 10 | | deg1z.z |
. . . 4
⊢ 0 =
(0g‘𝑃) |
| 11 | 3, 4, 10 | ply1mpl0 22258 |
. . 3
⊢ 0 =
(0g‘(1o mPoly 𝑅)) |
| 12 | 2, 3, 6, 7, 8, 9, 11 | mdegldg 26105 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ∃𝑏 ∈ (ℕ0
↑m 1o)((𝐹‘𝑏) ≠ 𝑌 ∧ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹))) |
| 13 | | deg1ldg.a |
. . . . . . . . . . 11
⊢ 𝐴 = (coe1‘𝐹) |
| 14 | 13 | fvcoe1 22209 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝐵 ∧ 𝑏 ∈ (ℕ0
↑m 1o)) → (𝐹‘𝑏) = (𝐴‘(𝑏‘∅))) |
| 15 | 14 | 3ad2antl2 1187 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ (ℕ0
↑m 1o)) → (𝐹‘𝑏) = (𝐴‘(𝑏‘∅))) |
| 16 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑎‘∅) = (𝑏‘∅)) |
| 17 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅)) = (𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅)) |
| 18 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝑏‘∅) ∈
V |
| 19 | 16, 17, 18 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (ℕ0
↑m 1o) → ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝑏‘∅)) |
| 20 | 19 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑏 ∈ (ℕ0
↑m 1o) → (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) = (𝐴‘(𝑏‘∅))) |
| 21 | 20 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ (ℕ0
↑m 1o)) → (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) = (𝐴‘(𝑏‘∅))) |
| 22 | 15, 21 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ (ℕ0
↑m 1o)) → (𝐹‘𝑏) = (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏))) |
| 23 | 22 | neeq1d 3000 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ (ℕ0
↑m 1o)) → ((𝐹‘𝑏) ≠ 𝑌 ↔ (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌)) |
| 24 | 23 | anbi1d 631 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ (ℕ0
↑m 1o)) → (((𝐹‘𝑏) ≠ 𝑌 ∧ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹)) ↔ ((𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌 ∧ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹)))) |
| 25 | 24 | biancomd 463 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ (ℕ0
↑m 1o)) → (((𝐹‘𝑏) ≠ 𝑌 ∧ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹)) ↔ (((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹) ∧ (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌))) |
| 26 | 25 | rexbidva 3177 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (∃𝑏 ∈ (ℕ0
↑m 1o)((𝐹‘𝑏) ≠ 𝑌 ∧ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹)) ↔ ∃𝑏 ∈ (ℕ0
↑m 1o)(((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹) ∧ (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌))) |
| 27 | | df1o2 8513 |
. . . . . 6
⊢
1o = {∅} |
| 28 | | nn0ex 12532 |
. . . . . 6
⊢
ℕ0 ∈ V |
| 29 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 30 | 27, 28, 29, 17 | mapsnf1o2 8934 |
. . . . 5
⊢ (𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅)):(ℕ0
↑m 1o)–1-1-onto→ℕ0 |
| 31 | | f1ofo 6855 |
. . . . 5
⊢ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅)):(ℕ0
↑m 1o)–1-1-onto→ℕ0 → (𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅)):(ℕ0
↑m 1o)–onto→ℕ0) |
| 32 | | eqeq1 2741 |
. . . . . . 7
⊢ (((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = 𝑑 → (((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹) ↔ 𝑑 = (𝐷‘𝐹))) |
| 33 | | fveq2 6906 |
. . . . . . . 8
⊢ (((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = 𝑑 → (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) = (𝐴‘𝑑)) |
| 34 | 33 | neeq1d 3000 |
. . . . . . 7
⊢ (((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = 𝑑 → ((𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌 ↔ (𝐴‘𝑑) ≠ 𝑌)) |
| 35 | 32, 34 | anbi12d 632 |
. . . . . 6
⊢ (((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = 𝑑 → ((((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹) ∧ (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌) ↔ (𝑑 = (𝐷‘𝐹) ∧ (𝐴‘𝑑) ≠ 𝑌))) |
| 36 | 35 | cbvexfo 7310 |
. . . . 5
⊢ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅)):(ℕ0
↑m 1o)–onto→ℕ0 → (∃𝑏 ∈ (ℕ0
↑m 1o)(((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹) ∧ (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌) ↔ ∃𝑑 ∈ ℕ0 (𝑑 = (𝐷‘𝐹) ∧ (𝐴‘𝑑) ≠ 𝑌))) |
| 37 | 30, 31, 36 | mp2b 10 |
. . . 4
⊢
(∃𝑏 ∈
(ℕ0 ↑m 1o)(((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹) ∧ (𝐴‘((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏)) ≠ 𝑌) ↔ ∃𝑑 ∈ ℕ0 (𝑑 = (𝐷‘𝐹) ∧ (𝐴‘𝑑) ≠ 𝑌)) |
| 38 | 26, 37 | bitrdi 287 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (∃𝑏 ∈ (ℕ0
↑m 1o)((𝐹‘𝑏) ≠ 𝑌 ∧ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹)) ↔ ∃𝑑 ∈ ℕ0 (𝑑 = (𝐷‘𝐹) ∧ (𝐴‘𝑑) ≠ 𝑌))) |
| 39 | 1, 4, 10, 5 | deg1nn0cl 26127 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈
ℕ0) |
| 40 | | fveq2 6906 |
. . . . . 6
⊢ (𝑑 = (𝐷‘𝐹) → (𝐴‘𝑑) = (𝐴‘(𝐷‘𝐹))) |
| 41 | 40 | neeq1d 3000 |
. . . . 5
⊢ (𝑑 = (𝐷‘𝐹) → ((𝐴‘𝑑) ≠ 𝑌 ↔ (𝐴‘(𝐷‘𝐹)) ≠ 𝑌)) |
| 42 | 41 | ceqsrexv 3655 |
. . . 4
⊢ ((𝐷‘𝐹) ∈ ℕ0 →
(∃𝑑 ∈
ℕ0 (𝑑 =
(𝐷‘𝐹) ∧ (𝐴‘𝑑) ≠ 𝑌) ↔ (𝐴‘(𝐷‘𝐹)) ≠ 𝑌)) |
| 43 | 39, 42 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (∃𝑑 ∈ ℕ0
(𝑑 = (𝐷‘𝐹) ∧ (𝐴‘𝑑) ≠ 𝑌) ↔ (𝐴‘(𝐷‘𝐹)) ≠ 𝑌)) |
| 44 | 38, 43 | bitrd 279 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (∃𝑏 ∈ (ℕ0
↑m 1o)((𝐹‘𝑏) ≠ 𝑌 ∧ ((𝑎 ∈ (ℕ0
↑m 1o) ↦ (𝑎‘∅))‘𝑏) = (𝐷‘𝐹)) ↔ (𝐴‘(𝐷‘𝐹)) ≠ 𝑌)) |
| 45 | 12, 44 | mpbid 232 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐴‘(𝐷‘𝐹)) ≠ 𝑌) |