Theorem sdrgrcl

Description: Reverse closure for a sub-division-ring predicate. (Contributed by SN, 19-Feb-2025)

	Ref	Expression
Assertion	sdrgrcl	$$⊢A\in \mathrm{SubDRing}\left(R\right)\to R\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		issdrg	$$⊢A\in \mathrm{SubDRing}\left(R\right)\leftrightarrow \left(R\in \mathrm{DivRing}\wedge A\in \mathrm{SubRing}\left(R\right)\wedge R{\upharpoonright }_{𝑠}A\in \mathrm{DivRing}\right)$$
2	1	simp1bi	$$⊢A\in \mathrm{SubDRing}\left(R\right)\to R\in \mathrm{DivRing}$$