| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 2 | | rprmirred.p |
. . . 4
⊢ 𝑃 = (RPrime‘𝑅) |
| 3 | | rprmirred.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ IDomn) |
| 4 | | rprmirred.q |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝑃) |
| 5 | 1, 2, 3, 4 | rprmcl 33546 |
. . 3
⊢ (𝜑 → 𝑄 ∈ (Base‘𝑅)) |
| 6 | | eqid 2737 |
. . . 4
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 7 | 2, 6, 3, 4 | rprmnunit 33549 |
. . 3
⊢ (𝜑 → ¬ 𝑄 ∈ (Unit‘𝑅)) |
| 8 | 5, 7 | eldifd 3962 |
. 2
⊢ (𝜑 → 𝑄 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) |
| 9 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 10 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 11 | | eqid 2737 |
. . . . . . . . 9
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
| 12 | 3 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑅 ∈ IDomn) |
| 13 | 12 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑅 ∈ IDomn) |
| 14 | 2, 9, 3, 4 | rprmnz 33548 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ≠ (0g‘𝑅)) |
| 15 | 14 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑄 ≠ (0g‘𝑅)) |
| 16 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) |
| 17 | 16 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) |
| 18 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) |
| 19 | 18 | eldifad 3963 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑦 ∈ (Base‘𝑅)) |
| 20 | 19 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑦 ∈ (Base‘𝑅)) |
| 21 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → (𝑥(.r‘𝑅)𝑦) = 𝑄) |
| 22 | 21 | eqcomd 2743 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑄 = (𝑥(.r‘𝑅)𝑦)) |
| 23 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑄(∥r‘𝑅)𝑥) |
| 24 | 1, 6, 9, 10, 11, 13, 15, 17, 20, 22, 23 | rprmirredlem 33558 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑦 ∈ (Unit‘𝑅)) |
| 25 | 18 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) |
| 26 | 25 | eldifbd 3964 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → ¬ 𝑦 ∈ (Unit‘𝑅)) |
| 27 | 24, 26 | pm2.21fal 1562 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑥) → ⊥) |
| 28 | 12 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑅 ∈ IDomn) |
| 29 | 14 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑄 ≠ (0g‘𝑅)) |
| 30 | 18 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) |
| 31 | 16 | eldifad 3963 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑥 ∈ (Base‘𝑅)) |
| 32 | 31 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑥 ∈ (Base‘𝑅)) |
| 33 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → (𝑥(.r‘𝑅)𝑦) = 𝑄) |
| 34 | 28 | idomcringd 20727 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑅 ∈ CRing) |
| 35 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑦 ∈ (Base‘𝑅)) |
| 36 | 1, 10, 34, 32, 35 | crngcomd 20252 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → (𝑥(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑥)) |
| 37 | 33, 36 | eqtr3d 2779 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑄 = (𝑦(.r‘𝑅)𝑥)) |
| 38 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑄(∥r‘𝑅)𝑦) |
| 39 | 1, 6, 9, 10, 11, 28, 29, 30, 32, 37, 38 | rprmirredlem 33558 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑥 ∈ (Unit‘𝑅)) |
| 40 | 16 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) |
| 41 | 40 | eldifbd 3964 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → ¬ 𝑥 ∈ (Unit‘𝑅)) |
| 42 | 39, 41 | pm2.21fal 1562 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) ∧ 𝑄(∥r‘𝑅)𝑦) → ⊥) |
| 43 | 4 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑄 ∈ 𝑃) |
| 44 | 3 | idomringd 20728 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 45 | 1, 11 | dvdsrid 20367 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ (Base‘𝑅)) → 𝑄(∥r‘𝑅)𝑄) |
| 46 | 44, 5, 45 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄(∥r‘𝑅)𝑄) |
| 47 | 46 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑄(∥r‘𝑅)𝑄) |
| 48 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → (𝑥(.r‘𝑅)𝑦) = 𝑄) |
| 49 | 47, 48 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → 𝑄(∥r‘𝑅)(𝑥(.r‘𝑅)𝑦)) |
| 50 | 1, 2, 11, 10, 12, 43, 31, 19, 49 | rprmdvds 33547 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → (𝑄(∥r‘𝑅)𝑥 ∨ 𝑄(∥r‘𝑅)𝑦)) |
| 51 | 27, 42, 50 | mpjaodan 961 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ (𝑥(.r‘𝑅)𝑦) = 𝑄) → ⊥) |
| 52 | 51 | inegd 1560 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) → ¬ (𝑥(.r‘𝑅)𝑦) = 𝑄) |
| 53 | 52 | neqned 2947 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))) → (𝑥(.r‘𝑅)𝑦) ≠ 𝑄) |
| 54 | 53 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅)) ∧ 𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅)))) → (𝑥(.r‘𝑅)𝑦) ≠ 𝑄) |
| 55 | 54 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))∀𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))(𝑥(.r‘𝑅)𝑦) ≠ 𝑄) |
| 56 | | rprmirred.i |
. . 3
⊢ 𝐼 = (Irred‘𝑅) |
| 57 | | eqid 2737 |
. . 3
⊢
((Base‘𝑅)
∖ (Unit‘𝑅)) =
((Base‘𝑅) ∖
(Unit‘𝑅)) |
| 58 | 1, 6, 56, 57, 10 | isirred 20419 |
. 2
⊢ (𝑄 ∈ 𝐼 ↔ (𝑄 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅)) ∧ ∀𝑥 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))∀𝑦 ∈ ((Base‘𝑅) ∖ (Unit‘𝑅))(𝑥(.r‘𝑅)𝑦) ≠ 𝑄)) |
| 59 | 8, 55, 58 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑄 ∈ 𝐼) |