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

Metamath Proof Explorer

Theorem sdrgss

Description: A division subring is a subset of the base set. (Contributed by Thierry Arnoux, 21-Aug-2023)

		Ref	Expression
	Hypothesis	sdrgid.1	$⊢ B = {Base}_{R}$
	Assertion	sdrgss	$⊢ S \in SubDRing (R) \to S \subseteq B$

Step	Hyp	Ref	Expression
1		sdrgid.1	$⊢ B = {Base}_{R}$
2		issdrg	$⊢ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing)$
3	1	subrgss	$⊢ S \in SubRing (R) \to S \subseteq B$
4	3	3ad2ant2	$⊢ (R \in DivRing \land S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing) \to S \subseteq B$
5	2 4	sylbi	$⊢ S \in SubDRing (R) \to S \subseteq B$