Step | Hyp | Ref
| Expression |
1 | | pidufd.1 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ PID) |
2 | | df-pid 21365 |
. . . 4
⊢ PID =
(IDomn ∩ LPIR) |
3 | 1, 2 | eleqtrdi 2849 |
. . 3
⊢ (𝜑 → 𝑅 ∈ (IDomn ∩ LPIR)) |
4 | 3 | elin1d 4214 |
. 2
⊢ (𝜑 → 𝑅 ∈ IDomn) |
5 | 4 | idomringd 20745 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | 5 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑅 ∈ Ring) |
7 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑥 ∈ (Base‘𝑅)) |
8 | | eqid 2735 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
9 | | eqid 2735 |
. . . . . . . . 9
⊢
(RSpan‘𝑅) =
(RSpan‘𝑅) |
10 | 8, 9 | rspsnid 33379 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ ((RSpan‘𝑅)‘{𝑥})) |
11 | 6, 7, 10 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑥 ∈ ((RSpan‘𝑅)‘{𝑥})) |
12 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑖 = ((RSpan‘𝑅)‘{𝑥})) |
13 | 11, 12 | eleqtrrd 2842 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑥 ∈ 𝑖) |
14 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) → 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) |
15 | 14 | eldifad 3975 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) → 𝑖 ∈ (PrmIdeal‘𝑅)) |
16 | 15 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑖 ∈ (PrmIdeal‘𝑅)) |
17 | 12, 16 | eqeltrrd 2840 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → ((RSpan‘𝑅)‘{𝑥}) ∈ (PrmIdeal‘𝑅)) |
18 | | eqid 2735 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
19 | | eqid 2735 |
. . . . . . . 8
⊢
(RPrime‘𝑅) =
(RPrime‘𝑅) |
20 | 4 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑅 ∈ IDomn) |
21 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → 𝑖 = ((RSpan‘𝑅)‘{𝑥})) |
22 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → 𝑥 = (0g‘𝑅)) |
23 | 22 | sneqd 4643 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → {𝑥} = {(0g‘𝑅)}) |
24 | 23 | fveq2d 6911 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → ((RSpan‘𝑅)‘{𝑥}) = ((RSpan‘𝑅)‘{(0g‘𝑅)})) |
25 | 9, 18 | rsp0 21266 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
((RSpan‘𝑅)‘{(0g‘𝑅)}) =
{(0g‘𝑅)}) |
26 | 5, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((RSpan‘𝑅)‘{(0g‘𝑅)}) =
{(0g‘𝑅)}) |
27 | 26 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → ((RSpan‘𝑅)‘{(0g‘𝑅)}) =
{(0g‘𝑅)}) |
28 | 21, 24, 27 | 3eqtrd 2779 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → 𝑖 = {(0g‘𝑅)}) |
29 | | eldifsni 4795 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}}) → 𝑖 ≠ {(0g‘𝑅)}) |
30 | 29 | ad4antlr 733 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → 𝑖 ≠ {(0g‘𝑅)}) |
31 | 30 | neneqd 2943 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) ∧ 𝑥 = (0g‘𝑅)) → ¬ 𝑖 = {(0g‘𝑅)}) |
32 | 28, 31 | pm2.65da 817 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → ¬ 𝑥 = (0g‘𝑅)) |
33 | 32 | neqned 2945 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑥 ≠ (0g‘𝑅)) |
34 | 18, 8, 19, 9, 20, 7, 33 | rsprprmprmidlb 33531 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → (𝑥 ∈ (RPrime‘𝑅) ↔ ((RSpan‘𝑅)‘{𝑥}) ∈ (PrmIdeal‘𝑅))) |
35 | 17, 34 | mpbird 257 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑥 ∈ (RPrime‘𝑅)) |
36 | 13, 35 | elind 4210 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → 𝑥 ∈ (𝑖 ∩ (RPrime‘𝑅))) |
37 | 36 | ne0d 4348 |
. . . 4
⊢ ((((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑖 = ((RSpan‘𝑅)‘{𝑥})) → (𝑖 ∩ (RPrime‘𝑅)) ≠ ∅) |
38 | | eqid 2735 |
. . . . 5
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
39 | 3 | elin2d 4215 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ LPIR) |
40 | 39 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) → 𝑅 ∈ LPIR) |
41 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) → 𝑅 ∈ Ring) |
42 | | prmidlidl 33452 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (PrmIdeal‘𝑅)) → 𝑖 ∈ (LIdeal‘𝑅)) |
43 | 41, 15, 42 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) → 𝑖 ∈ (LIdeal‘𝑅)) |
44 | 8, 38, 9, 40, 43 | lpirlidllpi 33382 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) → ∃𝑥 ∈ (Base‘𝑅)𝑖 = ((RSpan‘𝑅)‘{𝑥})) |
45 | 37, 44 | r19.29a 3160 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})) → (𝑖 ∩ (RPrime‘𝑅)) ≠ ∅) |
46 | 45 | ralrimiva 3144 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ ((PrmIdeal‘𝑅) ∖ {{(0g‘𝑅)}})(𝑖 ∩ (RPrime‘𝑅)) ≠ ∅) |
47 | | eqid 2735 |
. . 3
⊢
(PrmIdeal‘𝑅) =
(PrmIdeal‘𝑅) |
48 | 47, 19, 18 | isufd 33548 |
. 2
⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧
∀𝑖 ∈
((PrmIdeal‘𝑅) ∖
{{(0g‘𝑅)}})(𝑖 ∩ (RPrime‘𝑅)) ≠ ∅)) |
49 | 4, 46, 48 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑅 ∈ UFD) |