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 = R 𝑠 A
idlinsubrg.u U = LIdeal R
idlinsubrg.v V = LIdeal S
Assertion idlinsubrg A SubRing R I U I A V

Proof

Step Hyp Ref Expression
1 idlinsubrg.s S = R 𝑠 A
2 idlinsubrg.u U = LIdeal R
3 idlinsubrg.v V = LIdeal S
4 inss2 I A A
5 1 subrgbas A SubRing R A = Base S
6 4 5 sseqtrid A SubRing R I A Base S
7 6 adantr A SubRing R I U I A Base S
8 subrgrcl A SubRing R R Ring
9 eqid 0 R = 0 R
10 2 9 lidl0cl R Ring I U 0 R I
11 8 10 sylan A SubRing R I U 0 R I
12 subrgsubg A SubRing R A SubGrp R
13 subgsubm A SubGrp R A SubMnd R
14 9 subm0cl A SubMnd R 0 R A
15 12 13 14 3syl A SubRing R 0 R A
16 15 adantr A SubRing R I U 0 R A
17 11 16 elind A SubRing R I U 0 R I A
18 17 ne0d A SubRing R I U I A
19 eqid + R = + R
20 1 19 ressplusg A SubRing R + R = + S
21 eqid R = R
22 1 21 ressmulr A SubRing R R = S
23 22 oveqd A SubRing R x R a = x S a
24 eqidd A SubRing R b = b
25 20 23 24 oveq123d A SubRing R x R a + R b = x S a + S b
26 25 ad4antr A SubRing R I U x Base S a I A b I A x R a + R b = x S a + S b
27 8 ad4antr A SubRing R I U x Base S a I A b I A R Ring
28 simp-4r A SubRing R I U x Base S a I A b I A I U
29 eqid Base R = Base R
30 29 subrgss A SubRing R A Base R
31 5 30 eqsstrrd A SubRing R Base S Base R
32 31 adantr A SubRing R I U Base S Base R
33 32 sselda A SubRing R I U x Base S x Base R
34 33 ad2antrr A SubRing R I U x Base S a I A b I A x Base R
35 inss1 I A I
36 35 a1i A SubRing R I U x Base S I A I
37 36 sselda A SubRing R I U x Base S a I A a I
38 37 adantr A SubRing R I U x Base S a I A b I A a I
39 2 29 21 lidlmcl R Ring I U x Base R a I x R a I
40 27 28 34 38 39 syl22anc A SubRing R I U x Base S a I A b I A x R a I
41 35 a1i A SubRing R I U x Base S a I A I A I
42 41 sselda A SubRing R I U x Base S a I A b I A b I
43 2 19 lidlacl R Ring I U x R a I b I x R a + R b I
44 27 28 40 42 43 syl22anc A SubRing R I U x Base S a I A b I A x R a + R b I
45 simp-4l A SubRing R I U x Base S a I A b I A A SubRing R
46 simpr A SubRing R I U x Base S x Base S
47 5 ad2antrr A SubRing R I U x Base S A = Base S
48 46 47 eleqtrrd A SubRing R I U x Base S x A
49 48 ad2antrr A SubRing R I U x Base S a I A b I A x A
50 4 a1i A SubRing R I U x Base S I A A
51 50 sselda A SubRing R I U x Base S a I A a A
52 51 adantr A SubRing R I U x Base S a I A b I A a A
53 21 subrgmcl A SubRing R x A a A x R a A
54 45 49 52 53 syl3anc A SubRing R I U x Base S a I A b I A x R a A
55 4 a1i A SubRing R I U x Base S a I A I A A
56 55 sselda A SubRing R I U x Base S a I A b I A b A
57 19 subrgacl A SubRing R x R a A b A x R a + R b A
58 45 54 56 57 syl3anc A SubRing R I U x Base S a I A b I A x R a + R b A
59 44 58 elind A SubRing R I U x Base S a I A b I A x R a + R b I A
60 26 59 eqeltrrd A SubRing R I U x Base S a I A b I A x S a + S b I A
61 60 anasss A SubRing R I U x Base S a I A b I A x S a + S b I A
62 61 ralrimivva A SubRing R I U x Base S a I A b I A x S a + S b I A
63 62 ralrimiva A SubRing R I U x Base S a I A b I A x S a + S b I A
64 eqid Base S = Base S
65 eqid + S = + S
66 eqid S = S
67 3 64 65 66 islidl I A V I A Base S I A x Base S a I A b I A x S a + S b I A
68 7 18 63 67 syl3anbrc A SubRing R I U I A V