subrgid

Description: Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014)

		Ref	Expression
	Hypothesis	subrgss.1	$⊢ B = {Base}_{R}$
	Assertion	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$

Step	Hyp	Ref	Expression
1		subrgss.1	$⊢ B = {Base}_{R}$
2		id	$⊢ R \in Ring \to R \in Ring$
3	1	ressid	$⊢ R \in Ring \to R ↾_{𝑠} B = R$
4	3 2	eqeltrd	$⊢ R \in Ring \to R ↾_{𝑠} B \in Ring$
5		eqid	$⊢ 1_{R} = 1_{R}$
6	1 5	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
7		ssid	$⊢ B \subseteq B$
8	6 7	jctil	$⊢ R \in Ring \to (B \subseteq B \land 1_{R} \in B)$
9	1 5	issubrg	$⊢ B \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} B \in Ring) \land (B \subseteq B \land 1_{R} \in B))$
10	2 4 8 9	syl21anbrc	$⊢ R \in Ring \to B \in SubRing (R)$

Metamath Proof Explorer