Step | Hyp | Ref
| Expression |
1 | | subrgsubg 20028 |
. . . . 5
⊢ (𝑟 ∈ (SubRing‘𝑅) → 𝑟 ∈ (SubGrp‘𝑅)) |
2 | 1 | ssriv 3930 |
. . . 4
⊢
(SubRing‘𝑅)
⊆ (SubGrp‘𝑅) |
3 | | sstr 3934 |
. . . 4
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ (SubRing‘𝑅) ⊆ (SubGrp‘𝑅)) → 𝑆 ⊆ (SubGrp‘𝑅)) |
4 | 2, 3 | mpan2 688 |
. . 3
⊢ (𝑆 ⊆ (SubRing‘𝑅) → 𝑆 ⊆ (SubGrp‘𝑅)) |
5 | | subgint 18777 |
. . 3
⊢ ((𝑆 ⊆ (SubGrp‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ (SubGrp‘𝑅)) |
6 | 4, 5 | sylan 580 |
. 2
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ (SubGrp‘𝑅)) |
7 | | ssel2 3921 |
. . . . . 6
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑟 ∈ 𝑆) → 𝑟 ∈ (SubRing‘𝑅)) |
8 | 7 | adantlr 712 |
. . . . 5
⊢ (((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝑆) → 𝑟 ∈ (SubRing‘𝑅)) |
9 | | eqid 2740 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
10 | 9 | subrg1cl 20030 |
. . . . 5
⊢ (𝑟 ∈ (SubRing‘𝑅) →
(1r‘𝑅)
∈ 𝑟) |
11 | 8, 10 | syl 17 |
. . . 4
⊢ (((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ 𝑟 ∈ 𝑆) → (1r‘𝑅) ∈ 𝑟) |
12 | 11 | ralrimiva 3110 |
. . 3
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∀𝑟 ∈ 𝑆 (1r‘𝑅) ∈ 𝑟) |
13 | | fvex 6784 |
. . . 4
⊢
(1r‘𝑅) ∈ V |
14 | 13 | elint2 4892 |
. . 3
⊢
((1r‘𝑅) ∈ ∩ 𝑆 ↔ ∀𝑟 ∈ 𝑆 (1r‘𝑅) ∈ 𝑟) |
15 | 12, 14 | sylibr 233 |
. 2
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) →
(1r‘𝑅)
∈ ∩ 𝑆) |
16 | 8 | adantlr 712 |
. . . . . 6
⊢ ((((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑟 ∈ 𝑆) → 𝑟 ∈ (SubRing‘𝑅)) |
17 | | simprl 768 |
. . . . . . 7
⊢ (((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → 𝑥 ∈ ∩ 𝑆) |
18 | | elinti 4894 |
. . . . . . . 8
⊢ (𝑥 ∈ ∩ 𝑆
→ (𝑟 ∈ 𝑆 → 𝑥 ∈ 𝑟)) |
19 | 18 | imp 407 |
. . . . . . 7
⊢ ((𝑥 ∈ ∩ 𝑆
∧ 𝑟 ∈ 𝑆) → 𝑥 ∈ 𝑟) |
20 | 17, 19 | sylan 580 |
. . . . . 6
⊢ ((((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑟 ∈ 𝑆) → 𝑥 ∈ 𝑟) |
21 | | simprr 770 |
. . . . . . 7
⊢ (((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → 𝑦 ∈ ∩ 𝑆) |
22 | | elinti 4894 |
. . . . . . . 8
⊢ (𝑦 ∈ ∩ 𝑆
→ (𝑟 ∈ 𝑆 → 𝑦 ∈ 𝑟)) |
23 | 22 | imp 407 |
. . . . . . 7
⊢ ((𝑦 ∈ ∩ 𝑆
∧ 𝑟 ∈ 𝑆) → 𝑦 ∈ 𝑟) |
24 | 21, 23 | sylan 580 |
. . . . . 6
⊢ ((((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑟 ∈ 𝑆) → 𝑦 ∈ 𝑟) |
25 | | eqid 2740 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
26 | 25 | subrgmcl 20034 |
. . . . . 6
⊢ ((𝑟 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑟) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑟) |
27 | 16, 20, 24, 26 | syl3anc 1370 |
. . . . 5
⊢ ((((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) ∧ 𝑟 ∈ 𝑆) → (𝑥(.r‘𝑅)𝑦) ∈ 𝑟) |
28 | 27 | ralrimiva 3110 |
. . . 4
⊢ (((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → ∀𝑟 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑟) |
29 | | ovex 7304 |
. . . . 5
⊢ (𝑥(.r‘𝑅)𝑦) ∈ V |
30 | 29 | elint2 4892 |
. . . 4
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ ∩ 𝑆 ↔ ∀𝑟 ∈ 𝑆 (𝑥(.r‘𝑅)𝑦) ∈ 𝑟) |
31 | 28, 30 | sylibr 233 |
. . 3
⊢ (((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) ∧ (𝑥 ∈ ∩ 𝑆 ∧ 𝑦 ∈ ∩ 𝑆)) → (𝑥(.r‘𝑅)𝑦) ∈ ∩ 𝑆) |
32 | 31 | ralrimivva 3117 |
. 2
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ ∩ 𝑆∀𝑦 ∈ ∩ 𝑆(𝑥(.r‘𝑅)𝑦) ∈ ∩ 𝑆) |
33 | | ssn0 4340 |
. . 3
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → (SubRing‘𝑅) ≠ ∅) |
34 | | n0 4286 |
. . . 4
⊢
((SubRing‘𝑅)
≠ ∅ ↔ ∃𝑟 𝑟 ∈ (SubRing‘𝑅)) |
35 | | subrgrcl 20027 |
. . . . 5
⊢ (𝑟 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
36 | 35 | exlimiv 1937 |
. . . 4
⊢
(∃𝑟 𝑟 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
37 | 34, 36 | sylbi 216 |
. . 3
⊢
((SubRing‘𝑅)
≠ ∅ → 𝑅
∈ Ring) |
38 | | eqid 2740 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) |
39 | 38, 9, 25 | issubrg2 20042 |
. . 3
⊢ (𝑅 ∈ Ring → (∩ 𝑆
∈ (SubRing‘𝑅)
↔ (∩ 𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ ∩ 𝑆
∧ ∀𝑥 ∈
∩ 𝑆∀𝑦 ∈ ∩ 𝑆(𝑥(.r‘𝑅)𝑦) ∈ ∩ 𝑆))) |
40 | 33, 37, 39 | 3syl 18 |
. 2
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → (∩ 𝑆
∈ (SubRing‘𝑅)
↔ (∩ 𝑆 ∈ (SubGrp‘𝑅) ∧ (1r‘𝑅) ∈ ∩ 𝑆
∧ ∀𝑥 ∈
∩ 𝑆∀𝑦 ∈ ∩ 𝑆(𝑥(.r‘𝑅)𝑦) ∈ ∩ 𝑆))) |
41 | 6, 15, 32, 40 | mpbir3and 1341 |
1
⊢ ((𝑆 ⊆ (SubRing‘𝑅) ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ (SubRing‘𝑅)) |