Step | Hyp | Ref
| Expression |
1 | | inss2 4130 |
. . . 4
⊢ (𝐼 ∩ 𝐴) ⊆ 𝐴 |
2 | | idlinsubrg.s |
. . . . 5
⊢ 𝑆 = (𝑅 ↾s 𝐴) |
3 | 2 | subrgbas 19597 |
. . . 4
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 = (Base‘𝑆)) |
4 | 1, 3 | sseqtrid 3940 |
. . 3
⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝐼 ∩ 𝐴) ⊆ (Base‘𝑆)) |
5 | 4 | adantr 485 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (𝐼 ∩ 𝐴) ⊆ (Base‘𝑆)) |
6 | | subrgrcl 19593 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑅 ∈ Ring) |
7 | | idlinsubrg.u |
. . . . . 6
⊢ 𝑈 = (LIdeal‘𝑅) |
8 | | eqid 2759 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
9 | 7, 8 | lidl0cl 20038 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (0g‘𝑅) ∈ 𝐼) |
10 | 6, 9 | sylan 584 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (0g‘𝑅) ∈ 𝐼) |
11 | | subrgsubg 19594 |
. . . . . 6
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ∈ (SubGrp‘𝑅)) |
12 | | subgsubm 18353 |
. . . . . 6
⊢ (𝐴 ∈ (SubGrp‘𝑅) → 𝐴 ∈ (SubMnd‘𝑅)) |
13 | 8 | subm0cl 18027 |
. . . . . 6
⊢ (𝐴 ∈ (SubMnd‘𝑅) →
(0g‘𝑅)
∈ 𝐴) |
14 | 11, 12, 13 | 3syl 18 |
. . . . 5
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(0g‘𝑅)
∈ 𝐴) |
15 | 14 | adantr 485 |
. . . 4
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (0g‘𝑅) ∈ 𝐴) |
16 | 10, 15 | elind 4095 |
. . 3
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (0g‘𝑅) ∈ (𝐼 ∩ 𝐴)) |
17 | 16 | ne0d 4230 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (𝐼 ∩ 𝐴) ≠ ∅) |
18 | | eqid 2759 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
19 | 2, 18 | ressplusg 16655 |
. . . . . . . 8
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(+g‘𝑅) =
(+g‘𝑆)) |
20 | | eqid 2759 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
21 | 2, 20 | ressmulr 16668 |
. . . . . . . . 9
⊢ (𝐴 ∈ (SubRing‘𝑅) →
(.r‘𝑅) =
(.r‘𝑆)) |
22 | 21 | oveqd 7160 |
. . . . . . . 8
⊢ (𝐴 ∈ (SubRing‘𝑅) → (𝑥(.r‘𝑅)𝑎) = (𝑥(.r‘𝑆)𝑎)) |
23 | | eqidd 2760 |
. . . . . . . 8
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝑏 = 𝑏) |
24 | 19, 22, 23 | oveq123d 7164 |
. . . . . . 7
⊢ (𝐴 ∈ (SubRing‘𝑅) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) = ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏)) |
25 | 24 | ad4antr 732 |
. . . . . 6
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) = ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏)) |
26 | 6 | ad4antr 732 |
. . . . . . . 8
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝑅 ∈ Ring) |
27 | | simp-4r 784 |
. . . . . . . 8
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝐼 ∈ 𝑈) |
28 | | eqid 2759 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) |
29 | 28 | subrgss 19589 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (SubRing‘𝑅) → 𝐴 ⊆ (Base‘𝑅)) |
30 | 3, 29 | eqsstrrd 3927 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (SubRing‘𝑅) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
31 | 30 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (Base‘𝑆) ⊆ (Base‘𝑅)) |
32 | 31 | sselda 3888 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑥 ∈ (Base‘𝑅)) |
33 | 32 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ (Base‘𝑅)) |
34 | | inss1 4129 |
. . . . . . . . . . . 12
⊢ (𝐼 ∩ 𝐴) ⊆ 𝐼 |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) → (𝐼 ∩ 𝐴) ⊆ 𝐼) |
36 | 35 | sselda 3888 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) → 𝑎 ∈ 𝐼) |
37 | 36 | adantr 485 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝑎 ∈ 𝐼) |
38 | 7, 28, 20 | lidlmcl 20043 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑎 ∈ 𝐼)) → (𝑥(.r‘𝑅)𝑎) ∈ 𝐼) |
39 | 26, 27, 33, 37, 38 | syl22anc 838 |
. . . . . . . 8
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → (𝑥(.r‘𝑅)𝑎) ∈ 𝐼) |
40 | 34 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) → (𝐼 ∩ 𝐴) ⊆ 𝐼) |
41 | 40 | sselda 3888 |
. . . . . . . 8
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝑏 ∈ 𝐼) |
42 | 7, 18 | lidlacl 20039 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ ((𝑥(.r‘𝑅)𝑎) ∈ 𝐼 ∧ 𝑏 ∈ 𝐼)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝐼) |
43 | 26, 27, 39, 41, 42 | syl22anc 838 |
. . . . . . 7
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝐼) |
44 | | simp-4l 783 |
. . . . . . . 8
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝐴 ∈ (SubRing‘𝑅)) |
45 | | simpr 489 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑥 ∈ (Base‘𝑆)) |
46 | 3 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) → 𝐴 = (Base‘𝑆)) |
47 | 45, 46 | eleqtrrd 2854 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) → 𝑥 ∈ 𝐴) |
48 | 47 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝑥 ∈ 𝐴) |
49 | 1 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) → (𝐼 ∩ 𝐴) ⊆ 𝐴) |
50 | 49 | sselda 3888 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) → 𝑎 ∈ 𝐴) |
51 | 50 | adantr 485 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝑎 ∈ 𝐴) |
52 | 20 | subrgmcl 19600 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) → (𝑥(.r‘𝑅)𝑎) ∈ 𝐴) |
53 | 44, 48, 51, 52 | syl3anc 1369 |
. . . . . . . 8
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → (𝑥(.r‘𝑅)𝑎) ∈ 𝐴) |
54 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) → (𝐼 ∩ 𝐴) ⊆ 𝐴) |
55 | 54 | sselda 3888 |
. . . . . . . 8
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → 𝑏 ∈ 𝐴) |
56 | 18 | subrgacl 19599 |
. . . . . . . 8
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ (𝑥(.r‘𝑅)𝑎) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝐴) |
57 | 44, 53, 55, 56 | syl3anc 1369 |
. . . . . . 7
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ 𝐴) |
58 | 43, 57 | elind 4095 |
. . . . . 6
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → ((𝑥(.r‘𝑅)𝑎)(+g‘𝑅)𝑏) ∈ (𝐼 ∩ 𝐴)) |
59 | 25, 58 | eqeltrrd 2852 |
. . . . 5
⊢
(((((𝐴 ∈
(SubRing‘𝑅) ∧
𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ 𝑎 ∈ (𝐼 ∩ 𝐴)) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴)) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐼 ∩ 𝐴)) |
60 | 59 | anasss 471 |
. . . 4
⊢ ((((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) ∧ (𝑎 ∈ (𝐼 ∩ 𝐴) ∧ 𝑏 ∈ (𝐼 ∩ 𝐴))) → ((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐼 ∩ 𝐴)) |
61 | 60 | ralrimivva 3118 |
. . 3
⊢ (((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) ∧ 𝑥 ∈ (Base‘𝑆)) → ∀𝑎 ∈ (𝐼 ∩ 𝐴)∀𝑏 ∈ (𝐼 ∩ 𝐴)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐼 ∩ 𝐴)) |
62 | 61 | ralrimiva 3111 |
. 2
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → ∀𝑥 ∈ (Base‘𝑆)∀𝑎 ∈ (𝐼 ∩ 𝐴)∀𝑏 ∈ (𝐼 ∩ 𝐴)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐼 ∩ 𝐴)) |
63 | | idlinsubrg.v |
. . 3
⊢ 𝑉 = (LIdeal‘𝑆) |
64 | | eqid 2759 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑆) |
65 | | eqid 2759 |
. . 3
⊢
(+g‘𝑆) = (+g‘𝑆) |
66 | | eqid 2759 |
. . 3
⊢
(.r‘𝑆) = (.r‘𝑆) |
67 | 63, 64, 65, 66 | islidl 20037 |
. 2
⊢ ((𝐼 ∩ 𝐴) ∈ 𝑉 ↔ ((𝐼 ∩ 𝐴) ⊆ (Base‘𝑆) ∧ (𝐼 ∩ 𝐴) ≠ ∅ ∧ ∀𝑥 ∈ (Base‘𝑆)∀𝑎 ∈ (𝐼 ∩ 𝐴)∀𝑏 ∈ (𝐼 ∩ 𝐴)((𝑥(.r‘𝑆)𝑎)(+g‘𝑆)𝑏) ∈ (𝐼 ∩ 𝐴))) |
68 | 5, 17, 62, 67 | syl3anbrc 1341 |
1
⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (𝐼 ∩ 𝐴) ∈ 𝑉) |