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