Step | Hyp | Ref
| Expression |
1 | | simplr 769 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑉‘𝐼) = ∅) ∧ 𝐼 ≠ 𝐵) → (𝑉‘𝐼) = ∅) |
2 | | sseq2 3914 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → (𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ 𝑚)) |
3 | | eqid 2759 |
. . . . . . . . . . . 12
⊢
(LSSum‘(mulGrp‘𝑅)) = (LSSum‘(mulGrp‘𝑅)) |
4 | 3 | mxidlprm 31146 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) → 𝑚 ∈ (PrmIdeal‘𝑅)) |
5 | 4 | ad5ant14 758 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → 𝑚 ∈ (PrmIdeal‘𝑅)) |
6 | | simpr 489 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → 𝐼 ⊆ 𝑚) |
7 | 2, 5, 6 | elrabd 3602 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → 𝑚 ∈ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐼 ⊆ 𝑗}) |
8 | | zarclsx.1 |
. . . . . . . . . . 11
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
9 | 8 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
10 | | sseq1 3913 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑖 ⊆ 𝑗 ↔ 𝐼 ⊆ 𝑗)) |
11 | 10 | rabbidv 3390 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐼 ⊆ 𝑗}) |
12 | 11 | adantl 486 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) ∧ 𝑖 = 𝐼) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐼 ⊆ 𝑗}) |
13 | | simp-4r 784 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → 𝐼 ∈ (LIdeal‘𝑅)) |
14 | | fvex 6664 |
. . . . . . . . . . . 12
⊢
(PrmIdeal‘𝑅)
∈ V |
15 | 14 | rabex 5195 |
. . . . . . . . . . 11
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐼 ⊆ 𝑗} ∈ V |
16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐼 ⊆ 𝑗} ∈ V) |
17 | 9, 12, 13, 16 | fvmptd 6759 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → (𝑉‘𝐼) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐼 ⊆ 𝑗}) |
18 | 7, 17 | eleqtrrd 2854 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → 𝑚 ∈ (𝑉‘𝐼)) |
19 | | ne0i 4229 |
. . . . . . . 8
⊢ (𝑚 ∈ (𝑉‘𝐼) → (𝑉‘𝐼) ≠ ∅) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝐼 ∈
(LIdeal‘𝑅)) ∧
𝐼 ≠ 𝐵) ∧ 𝑚 ∈ (MaxIdeal‘𝑅)) ∧ 𝐼 ⊆ 𝑚) → (𝑉‘𝐼) ≠ ∅) |
21 | | crngring 19362 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
22 | | zarcls1.1 |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
23 | 22 | ssmxidl 31148 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝐼 ⊆ 𝑚) |
24 | 23 | 3expa 1116 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝐼 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝐼 ⊆ 𝑚) |
25 | 21, 24 | sylanl1 680 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝐼 ≠ 𝐵) → ∃𝑚 ∈ (MaxIdeal‘𝑅)𝐼 ⊆ 𝑚) |
26 | 20, 25 | r19.29a 3211 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝐼 ≠ 𝐵) → (𝑉‘𝐼) ≠ ∅) |
27 | 26 | adantlr 715 |
. . . . 5
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑉‘𝐼) = ∅) ∧ 𝐼 ≠ 𝐵) → (𝑉‘𝐼) ≠ ∅) |
28 | 27 | neneqd 2954 |
. . . 4
⊢ ((((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑉‘𝐼) = ∅) ∧ 𝐼 ≠ 𝐵) → ¬ (𝑉‘𝐼) = ∅) |
29 | 1, 28 | pm2.65da 817 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑉‘𝐼) = ∅) → ¬ 𝐼 ≠ 𝐵) |
30 | | nne 2953 |
. . 3
⊢ (¬
𝐼 ≠ 𝐵 ↔ 𝐼 = 𝐵) |
31 | 29, 30 | sylib 221 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ (𝑉‘𝐼) = ∅) → 𝐼 = 𝐵) |
32 | | fveq2 6651 |
. . . 4
⊢ (𝐼 = 𝐵 → (𝑉‘𝐼) = (𝑉‘𝐵)) |
33 | 32 | adantl 486 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝐼 = 𝐵) → (𝑉‘𝐼) = (𝑉‘𝐵)) |
34 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
35 | | sseq1 3913 |
. . . . . . . . 9
⊢ (𝑖 = 𝐵 → (𝑖 ⊆ 𝑗 ↔ 𝐵 ⊆ 𝑗)) |
36 | 35 | adantl 486 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑖 = 𝐵) → (𝑖 ⊆ 𝑗 ↔ 𝐵 ⊆ 𝑗)) |
37 | 36 | rabbidv 3390 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑖 = 𝐵) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐵 ⊆ 𝑗}) |
38 | | eqid 2759 |
. . . . . . . 8
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
39 | 38, 22 | lidl1 20046 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝐵 ∈ (LIdeal‘𝑅)) |
40 | 14 | rabex 5195 |
. . . . . . . 8
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐵 ⊆ 𝑗} ∈ V |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐵 ⊆ 𝑗} ∈ V) |
42 | 34, 37, 39, 41 | fvmptd 6759 |
. . . . . 6
⊢ (𝑅 ∈ Ring → (𝑉‘𝐵) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐵 ⊆ 𝑗}) |
43 | | prmidlidl 31125 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) → 𝑗 ∈ (LIdeal‘𝑅)) |
44 | 22, 38 | lidlss 20036 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (LIdeal‘𝑅) → 𝑗 ⊆ 𝐵) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) → 𝑗 ⊆ 𝐵) |
46 | 45 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) ∧ 𝐵 ⊆ 𝑗) → 𝑗 ⊆ 𝐵) |
47 | | simpr 489 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) ∧ 𝐵 ⊆ 𝑗) → 𝐵 ⊆ 𝑗) |
48 | 46, 47 | eqssd 3905 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) ∧ 𝐵 ⊆ 𝑗) → 𝑗 = 𝐵) |
49 | | eqid 2759 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
50 | 22, 49 | prmidlnr 31120 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) → 𝑗 ≠ 𝐵) |
51 | 50 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) ∧ 𝐵 ⊆ 𝑗) → 𝑗 ≠ 𝐵) |
52 | 51 | neneqd 2954 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) ∧ 𝐵 ⊆ 𝑗) → ¬ 𝑗 = 𝐵) |
53 | 48, 52 | pm2.65da 817 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑗 ∈ (PrmIdeal‘𝑅)) → ¬ 𝐵 ⊆ 𝑗) |
54 | 53 | ralrimiva 3111 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
∀𝑗 ∈
(PrmIdeal‘𝑅) ¬
𝐵 ⊆ 𝑗) |
55 | | rabeq0 4274 |
. . . . . . 7
⊢ ({𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐵 ⊆ 𝑗} = ∅ ↔ ∀𝑗 ∈ (PrmIdeal‘𝑅) ¬ 𝐵 ⊆ 𝑗) |
56 | 54, 55 | sylibr 237 |
. . . . . 6
⊢ (𝑅 ∈ Ring → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝐵 ⊆ 𝑗} = ∅) |
57 | 42, 56 | eqtrd 2794 |
. . . . 5
⊢ (𝑅 ∈ Ring → (𝑉‘𝐵) = ∅) |
58 | 21, 57 | syl 17 |
. . . 4
⊢ (𝑅 ∈ CRing → (𝑉‘𝐵) = ∅) |
59 | 58 | ad2antrr 726 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝐼 = 𝐵) → (𝑉‘𝐵) = ∅) |
60 | 33, 59 | eqtrd 2794 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝐼 = 𝐵) → (𝑉‘𝐼) = ∅) |
61 | 31, 60 | impbida 801 |
1
⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ((𝑉‘𝐼) = ∅ ↔ 𝐼 = 𝐵)) |