Metamath Proof Explorer

Theorem subsdrg

Description: A subring of a sub-division-ring is a sub-division-ring. See also subsubrg . (Contributed by Thierry Arnoux, 26-Oct-2025)

Ref Expression
Hypotheses subsdrg.s 
|- S = ( R |`s A )
subsdrg.a 
|- ( ph -> A e. ( SubDRing ` R ) )
Assertion subsdrg 
|- ( ph -> ( B e. ( SubDRing ` S ) <-> ( B e. ( SubDRing ` R ) /\ B C_ A ) ) )

Proof

Step Hyp Ref Expression
1 subsdrg.s 
 |-  S = ( R |`s A )
2 subsdrg.a 
 |-  ( ph -> A e. ( SubDRing ` R ) )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 3 sdrgss 
 |-  ( B e. ( SubDRing ` S ) -> B C_ ( Base ` S ) )
5 4 adantl 
 |-  ( ( ph /\ B e. ( SubDRing ` S ) ) -> B C_ ( Base ` S ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 6 sdrgss 
 |-  ( A e. ( SubDRing ` R ) -> A C_ ( Base ` R ) )
8 1 6 ressbas2 
 |-  ( A C_ ( Base ` R ) -> A = ( Base ` S ) )
9 2 7 8 3syl 
 |-  ( ph -> A = ( Base ` S ) )
10 9 adantr 
 |-  ( ( ph /\ B e. ( SubDRing ` S ) ) -> A = ( Base ` S ) )
11 5 10 sseqtrrd 
 |-  ( ( ph /\ B e. ( SubDRing ` S ) ) -> B C_ A )
12 11 ex 
 |-  ( ph -> ( B e. ( SubDRing ` S ) -> B C_ A ) )
13 12 pm4.71d 
 |-  ( ph -> ( B e. ( SubDRing ` S ) <-> ( B e. ( SubDRing ` S ) /\ B C_ A ) ) )
14 1 sdrgdrng 
 |-  ( A e. ( SubDRing ` R ) -> S e. DivRing )
15 2 14 syl 
 |-  ( ph -> S e. DivRing )
16 sdrgrcl 
 |-  ( A e. ( SubDRing ` R ) -> R e. DivRing )
17 2 16 syl 
 |-  ( ph -> R e. DivRing )
18 15 17 2thd 
 |-  ( ph -> ( S e. DivRing <-> R e. DivRing ) )
19 18 adantr 
 |-  ( ( ph /\ B C_ A ) -> ( S e. DivRing <-> R e. DivRing ) )
20 sdrgsubrg 
 |-  ( A e. ( SubDRing ` R ) -> A e. ( SubRing ` R ) )
21 1 subsubrg 
 |-  ( A e. ( SubRing ` R ) -> ( B e. ( SubRing ` S ) <-> ( B e. ( SubRing ` R ) /\ B C_ A ) ) )
22 2 20 21 3syl 
 |-  ( ph -> ( B e. ( SubRing ` S ) <-> ( B e. ( SubRing ` R ) /\ B C_ A ) ) )
23 22 rbaibd 
 |-  ( ( ph /\ B C_ A ) -> ( B e. ( SubRing ` S ) <-> B e. ( SubRing ` R ) ) )
24 1 oveq1i 
 |-  ( S |`s B ) = ( ( R |`s A ) |`s B )
25 ressabs 
 |-  ( ( A e. ( SubDRing ` R ) /\ B C_ A ) -> ( ( R |`s A ) |`s B ) = ( R |`s B ) )
26 2 25 sylan 
 |-  ( ( ph /\ B C_ A ) -> ( ( R |`s A ) |`s B ) = ( R |`s B ) )
27 24 26 eqtrid 
 |-  ( ( ph /\ B C_ A ) -> ( S |`s B ) = ( R |`s B ) )
28 27 eleq1d 
 |-  ( ( ph /\ B C_ A ) -> ( ( S |`s B ) e. DivRing <-> ( R |`s B ) e. DivRing ) )
29 19 23 28 3anbi123d 
 |-  ( ( ph /\ B C_ A ) -> ( ( S e. DivRing /\ B e. ( SubRing ` S ) /\ ( S |`s B ) e. DivRing ) <-> ( R e. DivRing /\ B e. ( SubRing ` R ) /\ ( R |`s B ) e. DivRing ) ) )
30 issdrg 
 |-  ( B e. ( SubDRing ` S ) <-> ( S e. DivRing /\ B e. ( SubRing ` S ) /\ ( S |`s B ) e. DivRing ) )
31 issdrg 
 |-  ( B e. ( SubDRing ` R ) <-> ( R e. DivRing /\ B e. ( SubRing ` R ) /\ ( R |`s B ) e. DivRing ) )
32 29 30 31 3bitr4g 
 |-  ( ( ph /\ B C_ A ) -> ( B e. ( SubDRing ` S ) <-> B e. ( SubDRing ` R ) ) )
33 32 ex 
 |-  ( ph -> ( B C_ A -> ( B e. ( SubDRing ` S ) <-> B e. ( SubDRing ` R ) ) ) )
34 33 pm5.32rd 
 |-  ( ph -> ( ( B e. ( SubDRing ` S ) /\ B C_ A ) <-> ( B e. ( SubDRing ` R ) /\ B C_ A ) ) )
35 13 34 bitrd 
 |-  ( ph -> ( B e. ( SubDRing ` S ) <-> ( B e. ( SubDRing ` R ) /\ B C_ A ) ) )