Metamath Proof Explorer

Theorem subsubrg

Description: A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypothesis subsubrg.s 
|- S = ( R |`s A )
Assertion subsubrg 
|- ( A e. ( SubRing ` R ) -> ( B e. ( SubRing ` S ) <-> ( B e. ( SubRing ` R ) /\ B C_ A ) ) )

Proof

Step Hyp Ref Expression
1 subsubrg.s 
 |-  S = ( R |`s A )
2 subrgrcl 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )
3 2 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> R e. Ring )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 4 subrgss 
 |-  ( B e. ( SubRing ` S ) -> B C_ ( Base ` S ) )
6 5 adantl 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> B C_ ( Base ` S ) )
7 1 subrgbas 
 |-  ( A e. ( SubRing ` R ) -> A = ( Base ` S ) )
8 7 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> A = ( Base ` S ) )
9 6 8 sseqtrrd 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> B C_ A )
10 1 oveq1i 
 |-  ( S |`s B ) = ( ( R |`s A ) |`s B )
11 ressabs 
 |-  ( ( A e. ( SubRing ` R ) /\ B C_ A ) -> ( ( R |`s A ) |`s B ) = ( R |`s B ) )
12 10 11 syl5eq 
 |-  ( ( A e. ( SubRing ` R ) /\ B C_ A ) -> ( S |`s B ) = ( R |`s B ) )
13 9 12 syldan 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( S |`s B ) = ( R |`s B ) )
14 eqid 
 |-  ( S |`s B ) = ( S |`s B )
15 14 subrgring 
 |-  ( B e. ( SubRing ` S ) -> ( S |`s B ) e. Ring )
16 15 adantl 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( S |`s B ) e. Ring )
17 13 16 eqeltrrd 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( R |`s B ) e. Ring )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 18 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
20 19 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> A C_ ( Base ` R ) )
21 9 20 sstrd 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> B C_ ( Base ` R ) )
22 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
23 1 22 subrg1 
 |-  ( A e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` S ) )
24 23 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( 1r ` R ) = ( 1r ` S ) )
25 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
26 25 subrg1cl 
 |-  ( B e. ( SubRing ` S ) -> ( 1r ` S ) e. B )
27 26 adantl 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( 1r ` S ) e. B )
28 24 27 eqeltrd 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( 1r ` R ) e. B )
29 21 28 jca 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( B C_ ( Base ` R ) /\ ( 1r ` R ) e. B ) )
30 18 22 issubrg 
 |-  ( B e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s B ) e. Ring ) /\ ( B C_ ( Base ` R ) /\ ( 1r ` R ) e. B ) ) )
31 3 17 29 30 syl21anbrc 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> B e. ( SubRing ` R ) )
32 31 9 jca 
 |-  ( ( A e. ( SubRing ` R ) /\ B e. ( SubRing ` S ) ) -> ( B e. ( SubRing ` R ) /\ B C_ A ) )
33 1 subrgring 
 |-  ( A e. ( SubRing ` R ) -> S e. Ring )
34 33 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> S e. Ring )
35 12 adantrl 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> ( S |`s B ) = ( R |`s B ) )
36 eqid 
 |-  ( R |`s B ) = ( R |`s B )
37 36 subrgring 
 |-  ( B e. ( SubRing ` R ) -> ( R |`s B ) e. Ring )
38 37 ad2antrl 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> ( R |`s B ) e. Ring )
39 35 38 eqeltrd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> ( S |`s B ) e. Ring )
40 simprr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> B C_ A )
41 7 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> A = ( Base ` S ) )
42 40 41 sseqtrd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> B C_ ( Base ` S ) )
43 23 adantr 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> ( 1r ` R ) = ( 1r ` S ) )
44 22 subrg1cl 
 |-  ( B e. ( SubRing ` R ) -> ( 1r ` R ) e. B )
45 44 ad2antrl 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> ( 1r ` R ) e. B )
46 43 45 eqeltrrd 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> ( 1r ` S ) e. B )
47 42 46 jca 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> ( B C_ ( Base ` S ) /\ ( 1r ` S ) e. B ) )
48 4 25 issubrg 
 |-  ( B e. ( SubRing ` S ) <-> ( ( S e. Ring /\ ( S |`s B ) e. Ring ) /\ ( B C_ ( Base ` S ) /\ ( 1r ` S ) e. B ) ) )
49 34 39 47 48 syl21anbrc 
 |-  ( ( A e. ( SubRing ` R ) /\ ( B e. ( SubRing ` R ) /\ B C_ A ) ) -> B e. ( SubRing ` S ) )
50 32 49 impbida 
 |-  ( A e. ( SubRing ` R ) -> ( B e. ( SubRing ` S ) <-> ( B e. ( SubRing ` R ) /\ B C_ A ) ) )