Theorem sdrgdrng

Description: A sub-division-ring is a division ring. (Contributed by SN, 19-Feb-2025)

	Ref	Expression
Hypothesis	sdrgdrng.1	|- S = ( R |`s A )
Assertion	sdrgdrng	|- ( A e. ( SubDRing ` R ) -> S e. DivRing )

Proof

Step	Hyp	Ref	Expression
1		sdrgdrng.1	|- S = ( R |`s A )
2		issdrg	|- ( A e. ( SubDRing ` R ) <-> ( R e. DivRing /\ A e. ( SubRing ` R ) /\ ( R |`s A ) e. DivRing ) )
3	2	simp3bi	|- ( A e. ( SubDRing ` R ) -> ( R |`s A ) e. DivRing )
4	1 3	eqeltrid	|- ( A e. ( SubDRing ` R ) -> S e. DivRing )