subrgring

Description: A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014)

		Ref	Expression
	Hypothesis	subrgring.1	$⊢ S = R ↾_{𝑠} A$
	Assertion	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$

Step	Hyp	Ref	Expression
1		subrgring.1	$⊢ S = R ↾_{𝑠} A$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	2 3	issubrg	$⊢ A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq {Base}_{R} \land 1_{R} \in A))$
5	4	simplbi	$⊢ A \in SubRing (R) \to (R \in Ring \land R ↾_{𝑠} A \in Ring)$
6	5	simprd	$⊢ A \in SubRing (R) \to R ↾_{𝑠} A \in Ring$
7	1 6	eqeltrid	$⊢ A \in SubRing (R) \to S \in Ring$

Metamath Proof Explorer