| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . 4
⊢ (𝑅 ∈ UFD → 𝑅 ∈ UFD) |
| 2 | 1 | ufdidom 33570 |
. . 3
⊢ (𝑅 ∈ UFD → 𝑅 ∈ IDomn) |
| 3 | | dfufd2.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
| 4 | | dfufd2.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
| 5 | | dfufd2.u |
. . . . 5
⊢ 𝑈 = (Unit‘𝑅) |
| 6 | | dfufd2.p |
. . . . 5
⊢ 𝑃 = (RPrime‘𝑅) |
| 7 | | dfufd2.m |
. . . . 5
⊢ 𝑀 = (mulGrp‘𝑅) |
| 8 | | simpl 482 |
. . . . 5
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑅 ∈ UFD) |
| 9 | | simpr 484 |
. . . . . . 7
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) |
| 10 | 9 | eldifad 3963 |
. . . . . 6
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ 𝑈)) |
| 11 | 10 | eldifad 3963 |
. . . . 5
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ 𝐵) |
| 12 | 10 | eldifbd 3964 |
. . . . 5
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → ¬ 𝑥 ∈ 𝑈) |
| 13 | | eldifsni 4790 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑥 ≠ 0 ) |
| 14 | 13 | adantl 481 |
. . . . 5
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ≠ 0 ) |
| 15 | 3, 4, 5, 6, 7, 8, 11, 12, 14 | 1arithufd 33576 |
. . . 4
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) |
| 16 | 15 | ralrimiva 3146 |
. . 3
⊢ (𝑅 ∈ UFD → ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) |
| 17 | 2, 16 | jca 511 |
. 2
⊢ (𝑅 ∈ UFD → (𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓))) |
| 18 | | simpl 482 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → 𝑅 ∈ IDomn) |
| 19 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ IDomn) |
| 20 | 19 | idomringd 20728 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Ring) |
| 21 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑅 ∈ Ring) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) |
| 23 | 22 | eldifad 3963 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (PrmIdeal‘𝑅)) |
| 24 | | prmidlidl 33472 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) → 𝑖 ∈ (LIdeal‘𝑅)) |
| 25 | 21, 23, 24 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (LIdeal‘𝑅)) |
| 26 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
| 27 | 3, 26 | lidlss 21222 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵) |
| 28 | 25, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ⊆ 𝐵) |
| 29 | 28 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ 𝐵) |
| 30 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ 𝑈) |
| 31 | | simplr 769 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ 𝑖) |
| 32 | 21 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑅 ∈ Ring) |
| 33 | 25 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑖 ∈ (LIdeal‘𝑅)) |
| 34 | 3, 5, 30, 31, 32, 33 | lidlunitel 33451 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑖 = 𝐵) |
| 35 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 36 | 3, 35 | prmidlnr 33467 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) → 𝑖 ≠ 𝐵) |
| 37 | 21, 23, 36 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ≠ 𝐵) |
| 38 | 37 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑖 ≠ 𝐵) |
| 39 | 38 | neneqd 2945 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → ¬ 𝑖 = 𝐵) |
| 40 | 34, 39 | pm2.65da 817 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → ¬ 𝑦 ∈ 𝑈) |
| 41 | 29, 40 | eldifd 3962 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ (𝐵 ∖ 𝑈)) |
| 42 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ≠ 0 ) |
| 43 | 41, 42 | eldifsnd 4787 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) |
| 44 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 = (𝑀 Σg 𝑓) ↔ 𝑦 = (𝑀 Σg 𝑓))) |
| 45 | 44 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓))) |
| 46 | 45 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑥 = 𝑦) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓))) |
| 47 | 43, 46 | rspcdv 3614 |
. . . . . . . 8
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → (∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) → ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓))) |
| 48 | | simp-5l 785 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑅 ∈ IDomn) |
| 49 | 23 | ad3antrrr 730 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑖 ∈ (PrmIdeal‘𝑅)) |
| 50 | | simplr 769 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑓 ∈ Word 𝑃) |
| 51 | | simpr 484 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑦 = (𝑀 Σg 𝑓)) |
| 52 | | simpllr 776 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑦 ∈ 𝑖) |
| 53 | 51, 52 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑀 Σg 𝑓) ∈ 𝑖) |
| 54 | 42 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑦 ≠ 0 ) |
| 55 | 51, 54 | eqnetrrd 3009 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑀 Σg 𝑓) ≠ 0 ) |
| 56 | 3, 4, 5, 6, 7, 48,
49, 50, 53, 55 | dfufd2lem 33577 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑖 ∩ 𝑃) ≠ ∅) |
| 57 | 56 | rexlimdva2 3157 |
. . . . . . . 8
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → (∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓) → (𝑖 ∩ 𝑃) ≠ ∅)) |
| 58 | 47, 57 | syld 47 |
. . . . . . 7
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → (∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) → (𝑖 ∩ 𝑃) ≠ ∅)) |
| 59 | 58 | imp 406 |
. . . . . 6
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ ∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → (𝑖 ∩ 𝑃) ≠ ∅) |
| 60 | 59 | an52ds 32470 |
. . . . 5
⊢
(((((𝑅 ∈ IDomn
∧ ∀𝑥 ∈
((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ≠ 0 ) → (𝑖 ∩ 𝑃) ≠ ∅) |
| 61 | 20 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑅 ∈ Ring) |
| 62 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) |
| 63 | 62 | eldifad 3963 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (PrmIdeal‘𝑅)) |
| 64 | 61, 63, 24 | syl2anc 584 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (LIdeal‘𝑅)) |
| 65 | | eldifsni 4790 |
. . . . . . 7
⊢ (𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }}) → 𝑖 ≠ { 0 }) |
| 66 | 65 | adantl 481 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ≠ { 0 }) |
| 67 | 26, 4 | lidlnz 21252 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ { 0 }) → ∃𝑦 ∈ 𝑖 𝑦 ≠ 0 ) |
| 68 | 61, 64, 66, 67 | syl3anc 1373 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → ∃𝑦 ∈ 𝑖 𝑦 ≠ 0 ) |
| 69 | 60, 68 | r19.29a 3162 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → (𝑖 ∩ 𝑃) ≠ ∅) |
| 70 | 69 | ralrimiva 3146 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → ∀𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅) |
| 71 | | eqid 2737 |
. . . 4
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) |
| 72 | 71, 6, 4 | isufd 33568 |
. . 3
⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧
∀𝑖 ∈
((PrmIdeal‘𝑅) ∖
{{ 0
}})(𝑖 ∩ 𝑃) ≠
∅)) |
| 73 | 18, 70, 72 | sylanbrc 583 |
. 2
⊢ ((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → 𝑅 ∈ UFD) |
| 74 | 17, 73 | impbii 209 |
1
⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓))) |