Metamath Proof Explorer


Theorem idlinsubrg

Description: The intersection between an ideal and a subring is an ideal of the subring. (Contributed by Thierry Arnoux, 6-Jul-2024)

Ref Expression
Hypotheses idlinsubrg.s 𝑆 = ( 𝑅s 𝐴 )
idlinsubrg.u 𝑈 = ( LIdeal ‘ 𝑅 )
idlinsubrg.v 𝑉 = ( LIdeal ‘ 𝑆 )
Assertion idlinsubrg ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐼𝑈 ) → ( 𝐼𝐴 ) ∈ 𝑉 )

Proof

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 ‘ 𝑅 ) ∧ 𝐼𝑈 ) → ( 𝐼𝐴 ) ∈ 𝑉 )