This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )