Step |
Hyp |
Ref |
Expression |
1 |
|
idlinsubrg.s |
⊢ 𝑆 = ( 𝑅 ↾s 𝐴 ) |
2 |
|
idlinsubrg.u |
⊢ 𝑈 = ( LIdeal ‘ 𝑅 ) |
3 |
|
idlinsubrg.v |
⊢ 𝑉 = ( LIdeal ‘ 𝑆 ) |
4 |
|
inss2 |
⊢ ( 𝐼 ∩ 𝐴 ) ⊆ 𝐴 |
5 |
1
|
subrgbas |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 = ( Base ‘ 𝑆 ) ) |
6 |
4 5
|
sseqtrid |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝐼 ∩ 𝐴 ) ⊆ ( Base ‘ 𝑆 ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∩ 𝐴 ) ⊆ ( Base ‘ 𝑆 ) ) |
8 |
|
subrgrcl |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring ) |
9 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
10 |
2 9
|
lidl0cl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑅 ) ∈ 𝐼 ) |
11 |
8 10
|
sylan |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑅 ) ∈ 𝐼 ) |
12 |
|
subrgsubg |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ) |
13 |
|
subgsubm |
⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → 𝐴 ∈ ( SubMnd ‘ 𝑅 ) ) |
14 |
9
|
subm0cl |
⊢ ( 𝐴 ∈ ( SubMnd ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝐴 ) |
15 |
12 13 14
|
3syl |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝐴 ) |
16 |
15
|
adantr |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑅 ) ∈ 𝐴 ) |
17 |
11 16
|
elind |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ( 0g ‘ 𝑅 ) ∈ ( 𝐼 ∩ 𝐴 ) ) |
18 |
17
|
ne0d |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∩ 𝐴 ) ≠ ∅ ) |
19 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
20 |
1 19
|
ressplusg |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑆 ) ) |
21 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
22 |
1 21
|
ressmulr |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) ) |
23 |
22
|
oveqd |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) = ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ) |
24 |
|
eqidd |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝑏 = 𝑏 ) |
25 |
20 23 24
|
oveq123d |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) = ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ( +g ‘ 𝑆 ) 𝑏 ) ) |
26 |
25
|
ad4antr |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) = ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ( +g ‘ 𝑆 ) 𝑏 ) ) |
27 |
8
|
ad4antr |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑅 ∈ Ring ) |
28 |
|
simp-4r |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝐼 ∈ 𝑈 ) |
29 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
30 |
29
|
subrgss |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) ) |
31 |
5 30
|
eqsstrrd |
⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) ) |
32 |
31
|
adantr |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑅 ) ) |
33 |
32
|
sselda |
⊢ ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) |
34 |
33
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) ) |
35 |
|
inss1 |
⊢ ( 𝐼 ∩ 𝐴 ) ⊆ 𝐼 |
36 |
35
|
a1i |
⊢ ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐼 ∩ 𝐴 ) ⊆ 𝐼 ) |
37 |
36
|
sselda |
⊢ ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑎 ∈ 𝐼 ) |
38 |
37
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑎 ∈ 𝐼 ) |
39 |
2 29 21
|
lidlmcl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝐼 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐼 ) |
40 |
27 28 34 38 39
|
syl22anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐼 ) |
41 |
35
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐼 ∩ 𝐴 ) ⊆ 𝐼 ) |
42 |
41
|
sselda |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑏 ∈ 𝐼 ) |
43 |
2 19
|
lidlacl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ) ∧ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐼 ∧ 𝑏 ∈ 𝐼 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) |
44 |
27 28 40 42 43
|
syl22anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐼 ) |
45 |
|
simp-4l |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝐴 ∈ ( SubRing ‘ 𝑅 ) ) |
46 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) ) |
47 |
5
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝐴 = ( Base ‘ 𝑆 ) ) |
48 |
46 47
|
eleqtrrd |
⊢ ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ 𝐴 ) |
49 |
48
|
ad2antrr |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ 𝐴 ) |
50 |
4
|
a1i |
⊢ ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐼 ∩ 𝐴 ) ⊆ 𝐴 ) |
51 |
50
|
sselda |
⊢ ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑎 ∈ 𝐴 ) |
52 |
51
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑎 ∈ 𝐴 ) |
53 |
21
|
subrgmcl |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐴 ) |
54 |
45 49 52 53
|
syl3anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐴 ) |
55 |
4
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐼 ∩ 𝐴 ) ⊆ 𝐴 ) |
56 |
55
|
sselda |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑏 ∈ 𝐴 ) |
57 |
19
|
subrgacl |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐴 ) |
58 |
45 54 56 57
|
syl3anc |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐴 ) |
59 |
44 58
|
elind |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑎 ) ( +g ‘ 𝑅 ) 𝑏 ) ∈ ( 𝐼 ∩ 𝐴 ) ) |
60 |
26 59
|
eqeltrrd |
⊢ ( ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( 𝐼 ∩ 𝐴 ) ) |
61 |
60
|
anasss |
⊢ ( ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ∧ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( 𝐼 ∩ 𝐴 ) ) |
62 |
61
|
ralrimivva |
⊢ ( ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ∀ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ∀ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( 𝐼 ∩ 𝐴 ) ) |
63 |
62
|
ralrimiva |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ∀ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( 𝐼 ∩ 𝐴 ) ) |
64 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
65 |
|
eqid |
⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) |
66 |
|
eqid |
⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 ) |
67 |
3 64 65 66
|
islidl |
⊢ ( ( 𝐼 ∩ 𝐴 ) ∈ 𝑉 ↔ ( ( 𝐼 ∩ 𝐴 ) ⊆ ( Base ‘ 𝑆 ) ∧ ( 𝐼 ∩ 𝐴 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑎 ∈ ( 𝐼 ∩ 𝐴 ) ∀ 𝑏 ∈ ( 𝐼 ∩ 𝐴 ) ( ( 𝑥 ( .r ‘ 𝑆 ) 𝑎 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( 𝐼 ∩ 𝐴 ) ) ) |
68 |
7 18 63 67
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼 ∈ 𝑈 ) → ( 𝐼 ∩ 𝐴 ) ∈ 𝑉 ) |