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 |`s A )
idlinsubrg.u
|- U = ( LIdeal ` R )
idlinsubrg.v
|- V = ( LIdeal ` S )
Assertion idlinsubrg
|- ( ( A e. ( SubRing ` R ) /\ I e. U ) -> ( I i^i A ) e. V )

Proof

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