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 ) )