Step | Hyp | Ref
| Expression |
1 | | crngring 19362 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
2 | 1 | ad4antr 732 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → 𝑅 ∈ Ring) |
3 | | elpwi 4496 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ 𝒫
(LIdeal‘𝑅) →
𝑟 ⊆
(LIdeal‘𝑅)) |
4 | 3 | adantl 486 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) → 𝑟 ⊆ (LIdeal‘𝑅)) |
5 | 4 | adantr 485 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → 𝑟 ⊆ (LIdeal‘𝑅)) |
6 | 5 | sselda 3888 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑖 ∈ 𝑟) → 𝑖 ∈ (LIdeal‘𝑅)) |
7 | | eqid 2759 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | | eqid 2759 |
. . . . . . . . . 10
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
9 | 7, 8 | lidlss 20036 |
. . . . . . . . 9
⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ (Base‘𝑅)) |
10 | 6, 9 | syl 17 |
. . . . . . . 8
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑖 ∈ 𝑟) → 𝑖 ⊆ (Base‘𝑅)) |
11 | 10 | ralrimiva 3111 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∀𝑖 ∈ 𝑟 𝑖 ⊆ (Base‘𝑅)) |
12 | | unissb 4825 |
. . . . . . 7
⊢ (∪ 𝑟
⊆ (Base‘𝑅)
↔ ∀𝑖 ∈
𝑟 𝑖 ⊆ (Base‘𝑅)) |
13 | 11, 12 | sylibr 237 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∪ 𝑟 ⊆ (Base‘𝑅)) |
14 | | eqid 2759 |
. . . . . . 7
⊢
(RSpan‘𝑅) =
(RSpan‘𝑅) |
15 | 14, 7, 8 | rspcl 20048 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ ∪ 𝑟
⊆ (Base‘𝑅))
→ ((RSpan‘𝑅)‘∪ 𝑟) ∈ (LIdeal‘𝑅)) |
16 | 2, 13, 15 | syl2anc 588 |
. . . . 5
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ((RSpan‘𝑅)‘∪ 𝑟) ∈ (LIdeal‘𝑅)) |
17 | | sseq1 3913 |
. . . . . . . 8
⊢ (𝑖 = ((RSpan‘𝑅)‘∪ 𝑟)
→ (𝑖 ⊆ 𝑗 ↔ ((RSpan‘𝑅)‘∪ 𝑟)
⊆ 𝑗)) |
18 | 17 | rabbidv 3390 |
. . . . . . 7
⊢ (𝑖 = ((RSpan‘𝑅)‘∪ 𝑟)
→ {𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ ((RSpan‘𝑅)‘∪ 𝑟) ⊆ 𝑗}) |
19 | 18 | eqeq2d 2770 |
. . . . . 6
⊢ (𝑖 = ((RSpan‘𝑅)‘∪ 𝑟)
→ (∩ 𝑆 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} ↔ ∩ 𝑆 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ ((RSpan‘𝑅)‘∪ 𝑟) ⊆ 𝑗})) |
20 | 19 | adantl 486 |
. . . . 5
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑖 = ((RSpan‘𝑅)‘∪ 𝑟)) → (∩ 𝑆 =
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗} ↔ ∩ 𝑆 =
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
((RSpan‘𝑅)‘∪ 𝑟) ⊆ 𝑗})) |
21 | | simpr 489 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → 𝑆 = (𝑉 “ 𝑟)) |
22 | 21 | inteqd 4836 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∩ 𝑆 = ∩
(𝑉 “ 𝑟)) |
23 | | zarclsx.1 |
. . . . . . . . . 10
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
24 | 23 | funmpt2 6367 |
. . . . . . . . 9
⊢ Fun 𝑉 |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → Fun 𝑉) |
26 | | fvex 6664 |
. . . . . . . . . . 11
⊢
(PrmIdeal‘𝑅)
∈ V |
27 | 26 | rabex 5195 |
. . . . . . . . . 10
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} ∈ V |
28 | 27, 23 | dmmpti 6468 |
. . . . . . . . 9
⊢ dom 𝑉 = (LIdeal‘𝑅) |
29 | 5, 28 | sseqtrrdi 3939 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → 𝑟 ⊆ dom 𝑉) |
30 | | intimafv 30552 |
. . . . . . . 8
⊢ ((Fun
𝑉 ∧ 𝑟 ⊆ dom 𝑉) → ∩ (𝑉 “ 𝑟) = ∩ 𝑙 ∈ 𝑟 (𝑉‘𝑙)) |
31 | 25, 29, 30 | syl2anc 588 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∩ (𝑉 “ 𝑟) = ∩ 𝑙 ∈ 𝑟 (𝑉‘𝑙)) |
32 | 22, 31 | eqtrd 2794 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∩ 𝑆 = ∩ 𝑙 ∈ 𝑟 (𝑉‘𝑙)) |
33 | | simplr 769 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑟 = ∅) → 𝑆 = (𝑉 “ 𝑟)) |
34 | | simpr 489 |
. . . . . . . . . . . 12
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑟 = ∅) → 𝑟 = ∅) |
35 | 34 | imaeq2d 5894 |
. . . . . . . . . . 11
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑟 = ∅) → (𝑉 “ 𝑟) = (𝑉 “ ∅)) |
36 | | ima0 5910 |
. . . . . . . . . . 11
⊢ (𝑉 “ ∅) =
∅ |
37 | 35, 36 | eqtrdi 2810 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑟 = ∅) → (𝑉 “ 𝑟) = ∅) |
38 | 33, 37 | eqtrd 2794 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑟 = ∅) → 𝑆 = ∅) |
39 | | simp-4r 784 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑟 = ∅) → 𝑆 ≠ ∅) |
40 | 39 | neneqd 2954 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑟 = ∅) → ¬ 𝑆 = ∅) |
41 | 38, 40 | pm2.65da 817 |
. . . . . . . 8
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ¬ 𝑟 = ∅) |
42 | 41 | neqned 2956 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → 𝑟 ≠ ∅) |
43 | 23, 14 | zarclsiin 31327 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑟 ⊆ (LIdeal‘𝑅) ∧ 𝑟 ≠ ∅) → ∩ 𝑙 ∈ 𝑟 (𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ 𝑟))) |
44 | 2, 5, 42, 43 | syl3anc 1369 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∩
𝑙 ∈ 𝑟 (𝑉‘𝑙) = (𝑉‘((RSpan‘𝑅)‘∪ 𝑟))) |
45 | 23 | a1i 11 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
46 | 18 | adantl 486 |
. . . . . . 7
⊢
((((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) ∧ 𝑖 = ((RSpan‘𝑅)‘∪ 𝑟)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗} = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ ((RSpan‘𝑅)‘∪ 𝑟) ⊆ 𝑗}) |
47 | 26 | rabex 5195 |
. . . . . . . 8
⊢ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ ((RSpan‘𝑅)‘∪ 𝑟)
⊆ 𝑗} ∈
V |
48 | 47 | a1i 11 |
. . . . . . 7
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → {𝑗 ∈ (PrmIdeal‘𝑅) ∣ ((RSpan‘𝑅)‘∪ 𝑟) ⊆ 𝑗} ∈ V) |
49 | 45, 46, 16, 48 | fvmptd 6759 |
. . . . . 6
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → (𝑉‘((RSpan‘𝑅)‘∪ 𝑟)) = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ ((RSpan‘𝑅)‘∪ 𝑟) ⊆ 𝑗}) |
50 | 32, 44, 49 | 3eqtrd 2798 |
. . . . 5
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∩ 𝑆 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ ((RSpan‘𝑅)‘∪ 𝑟) ⊆ 𝑗}) |
51 | 16, 20, 50 | rspcedvd 3542 |
. . . 4
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∃𝑖 ∈ (LIdeal‘𝑅)∩ 𝑆 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) |
52 | | intex 5200 |
. . . . . . . 8
⊢ (𝑆 ≠ ∅ ↔ ∩ 𝑆
∈ V) |
53 | 52 | biimpi 219 |
. . . . . . 7
⊢ (𝑆 ≠ ∅ → ∩ 𝑆
∈ V) |
54 | 53 | 3ad2ant3 1133 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ V) |
55 | 23 | elrnmpt 5790 |
. . . . . 6
⊢ (∩ 𝑆
∈ V → (∩ 𝑆 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (LIdeal‘𝑅)∩ 𝑆 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
56 | 54, 55 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅) → (∩ 𝑆
∈ ran 𝑉 ↔
∃𝑖 ∈
(LIdeal‘𝑅)∩ 𝑆 =
{𝑗 ∈
(PrmIdeal‘𝑅) ∣
𝑖 ⊆ 𝑗})) |
57 | 56 | ad5ant123 1362 |
. . . 4
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → (∩ 𝑆 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (LIdeal‘𝑅)∩ 𝑆 = {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})) |
58 | 51, 57 | mpbird 260 |
. . 3
⊢
(((((𝑅 ∈ CRing
∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∩ 𝑆 ∈ ran 𝑉) |
59 | | fvexd 6666 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → (LIdeal‘𝑅) ∈ V) |
60 | 24 | a1i 11 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → Fun 𝑉) |
61 | | simplr 769 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → 𝑆 ⊆ ran 𝑉) |
62 | 27, 23 | fnmpti 6467 |
. . . . . . . 8
⊢ 𝑉 Fn (LIdeal‘𝑅) |
63 | | fnima 6454 |
. . . . . . . 8
⊢ (𝑉 Fn (LIdeal‘𝑅) → (𝑉 “ (LIdeal‘𝑅)) = ran 𝑉) |
64 | 62, 63 | ax-mp 5 |
. . . . . . 7
⊢ (𝑉 “ (LIdeal‘𝑅)) = ran 𝑉 |
65 | 61, 64 | sseqtrrdi 3939 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → 𝑆 ⊆ (𝑉 “ (LIdeal‘𝑅))) |
66 | | ssimaexg 6731 |
. . . . . 6
⊢
(((LIdeal‘𝑅)
∈ V ∧ Fun 𝑉 ∧
𝑆 ⊆ (𝑉 “ (LIdeal‘𝑅))) → ∃𝑟(𝑟 ⊆ (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟))) |
67 | 59, 60, 65, 66 | syl3anc 1369 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → ∃𝑟(𝑟 ⊆ (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟))) |
68 | | vex 3411 |
. . . . . . . . . 10
⊢ 𝑟 ∈ V |
69 | 68 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ⊆ (LIdeal‘𝑅)) → 𝑟 ∈ V) |
70 | | simpr 489 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ⊆ (LIdeal‘𝑅)) → 𝑟 ⊆ (LIdeal‘𝑅)) |
71 | 69, 70 | elpwd 4495 |
. . . . . . . 8
⊢ ((((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ⊆ (LIdeal‘𝑅)) → 𝑟 ∈ 𝒫 (LIdeal‘𝑅)) |
72 | 71 | ex 417 |
. . . . . . 7
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → (𝑟 ⊆ (LIdeal‘𝑅) → 𝑟 ∈ 𝒫 (LIdeal‘𝑅))) |
73 | 72 | anim1d 614 |
. . . . . 6
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → ((𝑟 ⊆ (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟)) → (𝑟 ∈ 𝒫 (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟)))) |
74 | 73 | eximdv 1919 |
. . . . 5
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → (∃𝑟(𝑟 ⊆ (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟)) → ∃𝑟(𝑟 ∈ 𝒫 (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟)))) |
75 | 67, 74 | mpd 15 |
. . . 4
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → ∃𝑟(𝑟 ∈ 𝒫 (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟))) |
76 | | df-rex 3074 |
. . . 4
⊢
(∃𝑟 ∈
𝒫 (LIdeal‘𝑅)𝑆 = (𝑉 “ 𝑟) ↔ ∃𝑟(𝑟 ∈ 𝒫 (LIdeal‘𝑅) ∧ 𝑆 = (𝑉 “ 𝑟))) |
77 | 75, 76 | sylibr 237 |
. . 3
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → ∃𝑟 ∈ 𝒫
(LIdeal‘𝑅)𝑆 = (𝑉 “ 𝑟)) |
78 | 58, 77 | r19.29a 3211 |
. 2
⊢ (((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ ran 𝑉) |
79 | 78 | 3impa 1108 |
1
⊢ ((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ ran 𝑉) |