Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢ (𝑅 ∈ UFD → 𝑅 ∈ UFD) |
2 | 1 | ufdidom 33549 |
. . 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 3974 |
. . . . . 6
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ 𝑈)) |
11 | 10 | eldifad 3974 |
. . . . 5
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ∈ 𝐵) |
12 | 10 | eldifbd 3975 |
. . . . 5
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → ¬ 𝑥 ∈ 𝑈) |
13 | | eldifsni 4794 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 }) → 𝑥 ≠ 0 ) |
14 | 13 | adantl 481 |
. . . . 5
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → 𝑥 ≠ 0 ) |
15 | 3, 4, 5, 6, 7, 8, 11, 12, 14 | 1arithufd 33555 |
. . . 4
⊢ ((𝑅 ∈ UFD ∧ 𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) → ∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) |
16 | 15 | ralrimiva 3143 |
. . 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 20744 |
. . . . . . . . . . . . . . 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 3974 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (PrmIdeal‘𝑅)) |
24 | | prmidlidl 33451 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) → 𝑖 ∈ (LIdeal‘𝑅)) |
25 | 21, 23, 24 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (LIdeal‘𝑅)) |
26 | | eqid 2734 |
. . . . . . . . . . . . . 14
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
27 | 3, 26 | lidlss 21239 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ 𝐵) |
28 | 25, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ⊆ 𝐵) |
29 | 28 | sselda 3994 |
. . . . . . . . . . 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 33430 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → 𝑖 = 𝐵) |
35 | | eqid 2734 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑅) = (.r‘𝑅) |
36 | 3, 35 | prmidlnr 33446 |
. . . . . . . . . . . . . . 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 2942 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑦 ∈ 𝑈) → ¬ 𝑖 = 𝐵) |
40 | 34, 39 | pm2.65da 817 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → ¬ 𝑦 ∈ 𝑈) |
41 | 29, 40 | eldifd 3973 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ (𝐵 ∖ 𝑈)) |
42 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ≠ 0 ) |
43 | 41, 42 | eldifsnd 4791 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ IDomn ∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })) |
44 | | eqeq1 2738 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 = (𝑀 Σg 𝑓) ↔ 𝑦 = (𝑀 Σg 𝑓))) |
45 | 44 | rexbidv 3176 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓))) |
46 | 45 | adantl 481 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑥 = 𝑦) → (∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓) ↔ ∃𝑓 ∈ Word 𝑃𝑦 = (𝑀 Σg 𝑓))) |
47 | 43, 46 | rspcdv 3613 |
. . . . . . . 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 2839 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑀 Σg 𝑓) ∈ 𝑖) |
54 | 42 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → 𝑦 ≠ 0 ) |
55 | 51, 54 | eqnetrrd 3006 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑀 Σg 𝑓) ≠ 0 ) |
56 | 3, 4, 5, 6, 7, 48,
49, 50, 53, 55 | dfufd2lem 33556 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ IDomn
∧ 𝑦 ≠ 0 ) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) ∧ 𝑦 ∈ 𝑖) ∧ 𝑓 ∈ Word 𝑃) ∧ 𝑦 = (𝑀 Σg 𝑓)) → (𝑖 ∩ 𝑃) ≠ ∅) |
57 | 56 | rexlimdva2 3154 |
. . . . . . . 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 32479 |
. . . . 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 3974 |
. . . . . . 7
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (PrmIdeal‘𝑅)) |
64 | 61, 63, 24 | syl2anc 584 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ∈ (LIdeal‘𝑅)) |
65 | | eldifsni 4794 |
. . . . . . 7
⊢ (𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }}) → 𝑖 ≠ { 0 }) |
66 | 65 | adantl 481 |
. . . . . 6
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → 𝑖 ≠ { 0 }) |
67 | 26, 4 | lidlnz 21269 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅) ∧ 𝑖 ≠ { 0 }) → ∃𝑦 ∈ 𝑖 𝑦 ≠ 0 ) |
68 | 61, 64, 66, 67 | syl3anc 1370 |
. . . . 5
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → ∃𝑦 ∈ 𝑖 𝑦 ≠ 0 ) |
69 | 60, 68 | r19.29a 3159 |
. . . 4
⊢ (((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})) → (𝑖 ∩ 𝑃) ≠ ∅) |
70 | 69 | ralrimiva 3143 |
. . 3
⊢ ((𝑅 ∈ IDomn ∧
∀𝑥 ∈ ((𝐵 ∖ 𝑈) ∖ { 0 })∃𝑓 ∈ Word 𝑃𝑥 = (𝑀 Σg 𝑓)) → ∀𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅) |
71 | | eqid 2734 |
. . . 4
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) |
72 | 71, 6, 4 | isufd 33547 |
. . 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 𝑓))) |