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 \in DivRing \to B \in SubDRing (R)$

Step	Hyp	Ref	Expression
1		sdrgid.1	$⊢ B = {Base}_{R}$
2		id	$⊢ R \in DivRing \to R \in DivRing$
3		drngring	$⊢ R \in DivRing \to R \in Ring$
4	1	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
5	3 4	syl	$⊢ R \in DivRing \to B \in SubRing (R)$
6	1	ressid	$⊢ R \in DivRing \to R ↾_{𝑠} B = R$
7	6 2	eqeltrd	$⊢ R \in DivRing \to R ↾_{𝑠} B \in DivRing$
8		issdrg	$⊢ B \in SubDRing (R) \leftrightarrow (R \in DivRing \land B \in SubRing (R) \land R ↾_{𝑠} B \in DivRing)$
9	2 5 7 8	syl3anbrc	$⊢ R \in DivRing \to B \in SubDRing (R)$

Metamath Proof Explorer