| Step | Hyp | Ref
| Expression |
| 1 | | ply1dg1rt.o |
. . . . 5
⊢ 𝑂 = (eval1‘𝑅) |
| 2 | | ply1dg1rt.p |
. . . . 5
⊢ 𝑃 = (Poly1‘𝑅) |
| 3 | | ply1dg1rt.u |
. . . . 5
⊢ 𝑈 = (Base‘𝑃) |
| 4 | | ply1dg1rt.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Field) |
| 5 | 4 | fldcrngd 20742 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 7 | | ply1dg1rt.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑈) |
| 8 | 1, 2, 3, 5, 6, 7 | evl1fvf 33589 |
. . . 4
⊢ (𝜑 → (𝑂‘𝐺):(Base‘𝑅)⟶(Base‘𝑅)) |
| 9 | 8 | ffnd 6737 |
. . 3
⊢ (𝜑 → (𝑂‘𝐺) Fn (Base‘𝑅)) |
| 10 | | fniniseg2 7082 |
. . 3
⊢ ((𝑂‘𝐺) Fn (Base‘𝑅) → (◡(𝑂‘𝐺) “ { 0 }) = {𝑥 ∈ (Base‘𝑅) ∣ ((𝑂‘𝐺)‘𝑥) = 0 }) |
| 11 | 9, 10 | syl 17 |
. 2
⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) = {𝑥 ∈ (Base‘𝑅) ∣ ((𝑂‘𝐺)‘𝑥) = 0 }) |
| 12 | | fveqeq2 6915 |
. . 3
⊢ (𝑥 = 𝑍 → (((𝑂‘𝐺)‘𝑥) = 0 ↔ ((𝑂‘𝐺)‘𝑍) = 0 )) |
| 13 | | ply1dg1rt.z |
. . . 4
⊢ 𝑍 = ((𝑁‘𝐵) / 𝐴) |
| 14 | 5 | crngringd 20243 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 15 | | ply1dg1rt.x |
. . . . . 6
⊢ 𝑁 = (invg‘𝑅) |
| 16 | 5 | crnggrpd 20244 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 17 | | ply1dg1rt.b |
. . . . . . 7
⊢ 𝐵 = (𝐶‘0) |
| 18 | | 0nn0 12541 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
| 19 | | ply1dg1rt.c |
. . . . . . . . 9
⊢ 𝐶 = (coe1‘𝐺) |
| 20 | 19, 3, 2, 6 | coe1fvalcl 22214 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑈 ∧ 0 ∈ ℕ0) →
(𝐶‘0) ∈
(Base‘𝑅)) |
| 21 | 7, 18, 20 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝐶‘0) ∈ (Base‘𝑅)) |
| 22 | 17, 21 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (Base‘𝑅)) |
| 23 | 6, 15, 16, 22 | grpinvcld 19006 |
. . . . 5
⊢ (𝜑 → (𝑁‘𝐵) ∈ (Base‘𝑅)) |
| 24 | | ply1dg1rt.a |
. . . . . 6
⊢ 𝐴 = (𝐶‘1) |
| 25 | 4 | flddrngd 20741 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ DivRing) |
| 26 | | 1nn0 12542 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
| 27 | 19, 3, 2, 6 | coe1fvalcl 22214 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑈 ∧ 1 ∈ ℕ0) →
(𝐶‘1) ∈
(Base‘𝑅)) |
| 28 | 7, 26, 27 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → (𝐶‘1) ∈ (Base‘𝑅)) |
| 29 | | ply1dg1rt.1 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷‘𝐺) = 1) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 → (𝐶‘(𝐷‘𝐺)) = (𝐶‘1)) |
| 31 | 29, 26 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℕ0) |
| 32 | | ply1dg1rt.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (deg1‘𝑅) |
| 33 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 34 | 32, 2, 33, 3 | deg1nn0clb 26129 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝑈) → (𝐺 ≠ (0g‘𝑃) ↔ (𝐷‘𝐺) ∈
ℕ0)) |
| 35 | 34 | biimpar 477 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝑈) ∧ (𝐷‘𝐺) ∈ ℕ0) → 𝐺 ≠ (0g‘𝑃)) |
| 36 | 14, 7, 31, 35 | syl21anc 838 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ≠ (0g‘𝑃)) |
| 37 | | ply1dg1rt.0 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
| 38 | 32, 2, 33, 3, 37, 19 | deg1ldg 26131 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝑈 ∧ 𝐺 ≠ (0g‘𝑃)) → (𝐶‘(𝐷‘𝐺)) ≠ 0 ) |
| 39 | 14, 7, 36, 38 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝐶‘(𝐷‘𝐺)) ≠ 0 ) |
| 40 | 30, 39 | eqnetrrd 3009 |
. . . . . . 7
⊢ (𝜑 → (𝐶‘1) ≠ 0 ) |
| 41 | | eqid 2737 |
. . . . . . . . 9
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 42 | 6, 41, 37 | drngunit 20734 |
. . . . . . . 8
⊢ (𝑅 ∈ DivRing → ((𝐶‘1) ∈
(Unit‘𝑅) ↔
((𝐶‘1) ∈
(Base‘𝑅) ∧ (𝐶‘1) ≠ 0
))) |
| 43 | 42 | biimpar 477 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ ((𝐶‘1) ∈
(Base‘𝑅) ∧ (𝐶‘1) ≠ 0 )) →
(𝐶‘1) ∈
(Unit‘𝑅)) |
| 44 | 25, 28, 40, 43 | syl12anc 837 |
. . . . . 6
⊢ (𝜑 → (𝐶‘1) ∈ (Unit‘𝑅)) |
| 45 | 24, 44 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (Unit‘𝑅)) |
| 46 | | ply1dg1rt.m |
. . . . . 6
⊢ / =
(/r‘𝑅) |
| 47 | 6, 41, 46 | dvrcl 20404 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁‘𝐵) ∈ (Base‘𝑅) ∧ 𝐴 ∈ (Unit‘𝑅)) → ((𝑁‘𝐵) / 𝐴) ∈ (Base‘𝑅)) |
| 48 | 14, 23, 45, 47 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑁‘𝐵) / 𝐴) ∈ (Base‘𝑅)) |
| 49 | 13, 48 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑍 ∈ (Base‘𝑅)) |
| 50 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → 𝑍 = 𝑍) |
| 51 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑍 → (𝑥 = 𝑍 ↔ 𝑍 = 𝑍)) |
| 52 | 51 | imbi1d 341 |
. . . . 5
⊢ (𝑥 = 𝑍 → ((𝑥 = 𝑍 → ((𝑂‘𝐺)‘𝑍) = 0 ) ↔ (𝑍 = 𝑍 → ((𝑂‘𝐺)‘𝑍) = 0 ))) |
| 53 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑍 → ((𝑂‘𝐺)‘𝑥) = ((𝑂‘𝐺)‘𝑍)) |
| 54 | 53 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑥 = 𝑍) → ((𝑂‘𝐺)‘𝑥) = ((𝑂‘𝐺)‘𝑍)) |
| 55 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Grp) |
| 56 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 57 | 14 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
| 58 | 24, 28 | eqeltrid 2845 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ (Base‘𝑅)) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐴 ∈ (Base‘𝑅)) |
| 60 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
| 61 | 6, 56, 57, 59, 60 | ringcld 20257 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴(.r‘𝑅)𝑥) ∈ (Base‘𝑅)) |
| 62 | 23 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑁‘𝐵) ∈ (Base‘𝑅)) |
| 63 | 22 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐵 ∈ (Base‘𝑅)) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 65 | 6, 64 | grprcan 18991 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Grp ∧ ((𝐴(.r‘𝑅)𝑥) ∈ (Base‘𝑅) ∧ (𝑁‘𝐵) ∈ (Base‘𝑅) ∧ 𝐵 ∈ (Base‘𝑅))) → (((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵) = ((𝑁‘𝐵)(+g‘𝑅)𝐵) ↔ (𝐴(.r‘𝑅)𝑥) = (𝑁‘𝐵))) |
| 66 | 55, 61, 62, 63, 65 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵) = ((𝑁‘𝐵)(+g‘𝑅)𝐵) ↔ (𝐴(.r‘𝑅)𝑥) = (𝑁‘𝐵))) |
| 67 | 5 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing) |
| 68 | 48 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝑁‘𝐵) / 𝐴) ∈ (Base‘𝑅)) |
| 69 | 6, 56, 67, 68, 59 | crngcomd 20252 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝑁‘𝐵) / 𝐴)(.r‘𝑅)𝐴) = (𝐴(.r‘𝑅)((𝑁‘𝐵) / 𝐴))) |
| 70 | 45 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐴 ∈ (Unit‘𝑅)) |
| 71 | 6, 41, 46, 56 | dvrcan1 20409 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ (𝑁‘𝐵) ∈ (Base‘𝑅) ∧ 𝐴 ∈ (Unit‘𝑅)) → (((𝑁‘𝐵) / 𝐴)(.r‘𝑅)𝐴) = (𝑁‘𝐵)) |
| 72 | 57, 62, 70, 71 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝑁‘𝐵) / 𝐴)(.r‘𝑅)𝐴) = (𝑁‘𝐵)) |
| 73 | 69, 72 | eqtr3d 2779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴(.r‘𝑅)((𝑁‘𝐵) / 𝐴)) = (𝑁‘𝐵)) |
| 74 | 73 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐴(.r‘𝑅)𝑥) = (𝐴(.r‘𝑅)((𝑁‘𝐵) / 𝐴)) ↔ (𝐴(.r‘𝑅)𝑥) = (𝑁‘𝐵))) |
| 75 | | drngdomn 20749 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Domn) |
| 76 | 25, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑅 ∈ Domn) |
| 77 | | domnnzr 20706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
| 78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈ NzRing) |
| 79 | 78 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ NzRing) |
| 80 | 41, 37, 79, 70 | unitnz 33243 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐴 ≠ 0 ) |
| 81 | 59, 80 | eldifsnd 4787 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐴 ∈ ((Base‘𝑅) ∖ { 0 })) |
| 82 | 76 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Domn) |
| 83 | 6, 37, 56, 81, 60, 68, 82 | domnlcanb 20720 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐴(.r‘𝑅)𝑥) = (𝐴(.r‘𝑅)((𝑁‘𝐵) / 𝐴)) ↔ 𝑥 = ((𝑁‘𝐵) / 𝐴))) |
| 84 | 66, 74, 83 | 3bitr2rd 308 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 = ((𝑁‘𝐵) / 𝐴) ↔ ((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵) = ((𝑁‘𝐵)(+g‘𝑅)𝐵))) |
| 85 | 6, 64, 37, 15, 55, 63 | grplinvd 19012 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝑁‘𝐵)(+g‘𝑅)𝐵) = 0 ) |
| 86 | 85 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵) = ((𝑁‘𝐵)(+g‘𝑅)𝐵) ↔ ((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵) = 0 )) |
| 87 | 84, 86 | bitr2d 280 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵) = 0 ↔ 𝑥 = ((𝑁‘𝐵) / 𝐴))) |
| 88 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐺 ∈ 𝑈) |
| 89 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐷‘𝐺) = 1) |
| 90 | 2, 1, 6, 3, 56, 64, 19, 32, 24, 17, 67, 88, 89, 60 | evl1deg1 33601 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝑂‘𝐺)‘𝑥) = ((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵)) |
| 91 | 90 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝑂‘𝐺)‘𝑥) = 0 ↔ ((𝐴(.r‘𝑅)𝑥)(+g‘𝑅)𝐵) = 0 )) |
| 92 | 13 | eqeq2i 2750 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑍 ↔ 𝑥 = ((𝑁‘𝐵) / 𝐴)) |
| 93 | 92 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 = 𝑍 ↔ 𝑥 = ((𝑁‘𝐵) / 𝐴))) |
| 94 | 87, 91, 93 | 3bitr4d 311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝑂‘𝐺)‘𝑥) = 0 ↔ 𝑥 = 𝑍)) |
| 95 | 94 | biimpar 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑥 = 𝑍) → ((𝑂‘𝐺)‘𝑥) = 0 ) |
| 96 | 54, 95 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑥 = 𝑍) → ((𝑂‘𝐺)‘𝑍) = 0 ) |
| 97 | 96 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 = 𝑍 → ((𝑂‘𝐺)‘𝑍) = 0 )) |
| 98 | 97 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝑥 = 𝑍 → ((𝑂‘𝐺)‘𝑍) = 0 )) |
| 99 | 52, 98, 49 | rspcdva 3623 |
. . . 4
⊢ (𝜑 → (𝑍 = 𝑍 → ((𝑂‘𝐺)‘𝑍) = 0 )) |
| 100 | 50, 99 | mpd 15 |
. . 3
⊢ (𝜑 → ((𝑂‘𝐺)‘𝑍) = 0 ) |
| 101 | 94 | biimpa 476 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) ∧ ((𝑂‘𝐺)‘𝑥) = 0 ) → 𝑥 = 𝑍) |
| 102 | 12, 49, 100, 101 | rabeqsnd 4669 |
. 2
⊢ (𝜑 → {𝑥 ∈ (Base‘𝑅) ∣ ((𝑂‘𝐺)‘𝑥) = 0 } = {𝑍}) |
| 103 | 11, 102 | eqtrd 2777 |
1
⊢ (𝜑 → (◡(𝑂‘𝐺) “ { 0 }) = {𝑍}) |