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

Metamath Proof Explorer

Theorem sdrgid

Description: Every division ring is a division subring of itself. (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Hypothesis sdrgid.1 
|- B = ( Base ` R )
Assertion sdrgid 
|- ( R e. DivRing -> B e. ( SubDRing ` R ) )

Proof

Step Hyp Ref Expression
1 sdrgid.1 
 |-  B = ( Base ` R )
2 id 
 |-  ( R e. DivRing -> R e. DivRing )
3 drngring 
 |-  ( R e. DivRing -> R e. Ring )
4 1 subrgid 
 |-  ( R e. Ring -> B e. ( SubRing ` R ) )
5 3 4 syl 
 |-  ( R e. DivRing -> B e. ( SubRing ` R ) )
6 1 ressid 
 |-  ( R e. DivRing -> ( R |`s B ) = R )
7 6 2 eqeltrd 
 |-  ( R e. DivRing -> ( R |`s B ) e. DivRing )
8 issdrg 
 |-  ( B e. ( SubDRing ` R ) <-> ( R e. DivRing /\ B e. ( SubRing ` R ) /\ ( R |`s B ) e. DivRing ) )
9 2 5 7 8 syl3anbrc 
 |-  ( R e. DivRing -> B e. ( SubDRing ` R ) )