Metamath Proof Explorer

Theorem subsubrng

Description: A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 subsubrng.s 
 |-  S = ( R |`s A )
2 subrngrcl 
 |-  ( A e. ( SubRng ` R ) -> R e. Rng )
3 2 adantr 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> R e. Rng )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 4 subrngss 
 |-  ( B e. ( SubRng ` S ) -> B C_ ( Base ` S ) )
6 5 adantl 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ ( Base ` S ) )
7 1 subrngbas 
 |-  ( A e. ( SubRng ` R ) -> A = ( Base ` S ) )
8 7 adantr 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> A = ( Base ` S ) )
9 6 8 sseqtrrd 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ A )
10 1 oveq1i 
 |-  ( S |`s B ) = ( ( R |`s A ) |`s B )
11 ressabs 
 |-  ( ( A e. ( SubRng ` R ) /\ B C_ A ) -> ( ( R |`s A ) |`s B ) = ( R |`s B ) )
12 10 11 eqtrid 
 |-  ( ( A e. ( SubRng ` R ) /\ B C_ A ) -> ( S |`s B ) = ( R |`s B ) )
13 9 12 syldan 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( S |`s B ) = ( R |`s B ) )
14 eqid 
 |-  ( S |`s B ) = ( S |`s B )
15 14 subrngrng 
 |-  ( B e. ( SubRng ` S ) -> ( S |`s B ) e. Rng )
16 15 adantl 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( S |`s B ) e. Rng )
17 13 16 eqeltrrd 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( R |`s B ) e. Rng )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 18 subrngss 
 |-  ( A e. ( SubRng ` R ) -> A C_ ( Base ` R ) )
20 19 adantr 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> A C_ ( Base ` R ) )
21 9 20 sstrd 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B C_ ( Base ` R ) )
22 18 issubrng 
 |-  ( B e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s B ) e. Rng /\ B C_ ( Base ` R ) ) )
23 3 17 21 22 syl3anbrc 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> B e. ( SubRng ` R ) )
24 23 9 jca 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` S ) ) -> ( B e. ( SubRng ` R ) /\ B C_ A ) )
25 1 subrngrng 
 |-  ( A e. ( SubRng ` R ) -> S e. Rng )
26 25 adantr 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> S e. Rng )
27 12 adantrl 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( S |`s B ) = ( R |`s B ) )
28 eqid 
 |-  ( R |`s B ) = ( R |`s B )
29 28 subrngrng 
 |-  ( B e. ( SubRng ` R ) -> ( R |`s B ) e. Rng )
30 29 ad2antrl 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( R |`s B ) e. Rng )
31 27 30 eqeltrd 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> ( S |`s B ) e. Rng )
32 simprr 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B C_ A )
33 7 adantr 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> A = ( Base ` S ) )
34 32 33 sseqtrd 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B C_ ( Base ` S ) )
35 4 issubrng 
 |-  ( B e. ( SubRng ` S ) <-> ( S e. Rng /\ ( S |`s B ) e. Rng /\ B C_ ( Base ` S ) ) )
36 26 31 34 35 syl3anbrc 
 |-  ( ( A e. ( SubRng ` R ) /\ ( B e. ( SubRng ` R ) /\ B C_ A ) ) -> B e. ( SubRng ` S ) )
37 24 36 impbida 
 |-  ( A e. ( SubRng ` R ) -> ( B e. ( SubRng ` S ) <-> ( B e. ( SubRng ` R ) /\ B C_ A ) ) )