Step | Hyp | Ref
| Expression |
1 | | simp3 1136 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → 𝐶 ⊆ (LIdeal‘𝑅)) |
2 | 1 | sselda 3888 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (LIdeal‘𝑅)) |
3 | | eqid 2759 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | | eqid 2759 |
. . . . . . 7
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
5 | 3, 4 | lidlss 20036 |
. . . . . 6
⊢ (𝑖 ∈ (LIdeal‘𝑅) → 𝑖 ⊆ (Base‘𝑅)) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) ∧ 𝑖 ∈ 𝐶) → 𝑖 ⊆ (Base‘𝑅)) |
7 | 6 | ralrimiva 3111 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ (Base‘𝑅)) |
8 | | pwssb 4981 |
. . . 4
⊢ (𝐶 ⊆ 𝒫
(Base‘𝑅) ↔
∀𝑖 ∈ 𝐶 𝑖 ⊆ (Base‘𝑅)) |
9 | 7, 8 | sylibr 237 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → 𝐶 ⊆ 𝒫 (Base‘𝑅)) |
10 | | simp2 1135 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → 𝐶 ≠ ∅) |
11 | | intss2 4988 |
. . . 4
⊢ (𝐶 ⊆ 𝒫
(Base‘𝑅) →
(𝐶 ≠ ∅ →
∩ 𝐶 ⊆ (Base‘𝑅))) |
12 | 11 | imp 411 |
. . 3
⊢ ((𝐶 ⊆ 𝒫
(Base‘𝑅) ∧ 𝐶 ≠ ∅) → ∩ 𝐶
⊆ (Base‘𝑅)) |
13 | 9, 10, 12 | syl2anc 588 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶
⊆ (Base‘𝑅)) |
14 | | simpl1 1189 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) ∧ 𝑖 ∈ 𝐶) → 𝑅 ∈ Ring) |
15 | | eqid 2759 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
16 | 4, 15 | lidl0cl 20038 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) →
(0g‘𝑅)
∈ 𝑖) |
17 | 14, 2, 16 | syl2anc 588 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) ∧ 𝑖 ∈ 𝐶) → (0g‘𝑅) ∈ 𝑖) |
18 | 17 | ralrimiva 3111 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∀𝑖 ∈ 𝐶 (0g‘𝑅) ∈ 𝑖) |
19 | | fvex 6664 |
. . . . 5
⊢
(0g‘𝑅) ∈ V |
20 | 19 | elint2 4838 |
. . . 4
⊢
((0g‘𝑅) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 (0g‘𝑅) ∈ 𝑖) |
21 | 18, 20 | sylibr 237 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) →
(0g‘𝑅)
∈ ∩ 𝐶) |
22 | 21 | ne0d 4230 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶
≠ ∅) |
23 | 14 | ad5ant15 759 |
. . . . . . . 8
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → 𝑅 ∈ Ring) |
24 | 2 | ad5ant15 759 |
. . . . . . . 8
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (LIdeal‘𝑅)) |
25 | | simp-4r 784 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → 𝑥 ∈ (Base‘𝑅)) |
26 | | simpllr 776 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → 𝑎 ∈ ∩ 𝐶) |
27 | | simpr 489 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ 𝐶) |
28 | | elinti 4840 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ∩ 𝐶
→ (𝑖 ∈ 𝐶 → 𝑎 ∈ 𝑖)) |
29 | 28 | imp 411 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ∩ 𝐶
∧ 𝑖 ∈ 𝐶) → 𝑎 ∈ 𝑖) |
30 | 26, 27, 29 | syl2anc 588 |
. . . . . . . . 9
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → 𝑎 ∈ 𝑖) |
31 | | eqid 2759 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
32 | 4, 3, 31 | lidlmcl 20043 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝑖)) → (𝑥(.r‘𝑅)𝑎) ∈ 𝑖) |
33 | 23, 24, 25, 30, 32 | syl22anc 838 |
. . . . . . . 8
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → (𝑥(.r‘𝑅)𝑎) ∈ 𝑖) |
34 | | elinti 4840 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ∩ 𝐶
→ (𝑖 ∈ 𝐶 → 𝑏 ∈ 𝑖)) |
35 | 34 | imp 411 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ∩ 𝐶
∧ 𝑖 ∈ 𝐶) → 𝑏 ∈ 𝑖) |
36 | 35 | adantll 714 |
. . . . . . . 8
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → 𝑏 ∈ 𝑖) |
37 | | eqid 2759 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
38 | 4, 37 | lidlacl 20039 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝑖 ∈ (LIdeal‘𝑅)) ∧ ((𝑥(.r‘𝑅)𝑎) ∈ 𝑖 ∧ 𝑏 ∈ 𝑖)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑖) |
39 | 23, 24, 33, 36, 38 | syl22anc 838 |
. . . . . . 7
⊢
((((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) ∧ 𝑖 ∈ 𝐶) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑖) |
40 | 39 | ralrimiva 3111 |
. . . . . 6
⊢
(((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) → ∀𝑖 ∈ 𝐶 ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑖) |
41 | | ovex 7176 |
. . . . . . 7
⊢ ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ V |
42 | 41 | elint2 4838 |
. . . . . 6
⊢ (((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∩ 𝐶 ↔ ∀𝑖 ∈ 𝐶 ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝑖) |
43 | 40, 42 | sylibr 237 |
. . . . 5
⊢
(((((𝑅 ∈ Ring
∧ 𝐶 ≠ ∅ ∧
𝐶 ⊆
(LIdeal‘𝑅)) ∧
𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) ∧ 𝑏 ∈ ∩ 𝐶) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∩ 𝐶) |
44 | 43 | ralrimiva 3111 |
. . . 4
⊢ ((((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) ∧ 𝑥 ∈ (Base‘𝑅)) ∧ 𝑎 ∈ ∩ 𝐶) → ∀𝑏 ∈ ∩ 𝐶((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∩ 𝐶) |
45 | 44 | anasss 471 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ ∩ 𝐶)) → ∀𝑏 ∈ ∩ 𝐶((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∩ 𝐶) |
46 | 45 | ralrimivva 3118 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∀𝑥 ∈ (Base‘𝑅)∀𝑎 ∈ ∩ 𝐶∀𝑏 ∈ ∩ 𝐶((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∩ 𝐶) |
47 | 4, 3, 37, 31 | islidl 20037 |
. 2
⊢ (∩ 𝐶
∈ (LIdeal‘𝑅)
↔ (∩ 𝐶 ⊆ (Base‘𝑅) ∧ ∩ 𝐶 ≠ ∅ ∧
∀𝑥 ∈
(Base‘𝑅)∀𝑎 ∈ ∩ 𝐶∀𝑏 ∈ ∩ 𝐶((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ ∩ 𝐶)) |
48 | 13, 22, 46, 47 | syl3anbrc 1341 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶
∈ (LIdeal‘𝑅)) |