subrgcrng

Description: A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015)

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

Step	Hyp	Ref	Expression
1		subrgring.1	$⊢ S = R ↾_{𝑠} A$
2	1	subrgring	$⊢ A \in SubRing (R) \to S \in Ring$
3	2	adantl	$⊢ (R \in CRing \land A \in SubRing (R)) \to S \in Ring$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5	1 4	mgpress	$⊢ (R \in CRing \land A \in SubRing (R)) \to {mulGrp}_{R} ↾_{𝑠} A = {mulGrp}_{S}$
6	4	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
7		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
8	7	ringmgp	$⊢ S \in Ring \to {mulGrp}_{S} \in Mnd$
9	3 8	syl	$⊢ (R \in CRing \land A \in SubRing (R)) \to {mulGrp}_{S} \in Mnd$
10	5 9	eqeltrd	$⊢ (R \in CRing \land A \in SubRing (R)) \to {mulGrp}_{R} ↾_{𝑠} A \in Mnd$
11		eqid	$⊢ {mulGrp}_{R} ↾_{𝑠} A = {mulGrp}_{R} ↾_{𝑠} A$
12	11	subcmn	$⊢ ({mulGrp}_{R} \in CMnd \land {mulGrp}_{R} ↾_{𝑠} A \in Mnd) \to {mulGrp}_{R} ↾_{𝑠} A \in CMnd$
13	6 10 12	syl2an2r	$⊢ (R \in CRing \land A \in SubRing (R)) \to {mulGrp}_{R} ↾_{𝑠} A \in CMnd$
14	5 13	eqeltrrd	$⊢ (R \in CRing \land A \in SubRing (R)) \to {mulGrp}_{S} \in CMnd$
15	7	iscrng	$⊢ S \in CRing \leftrightarrow (S \in Ring \land {mulGrp}_{S} \in CMnd)$
16	3 14 15	sylanbrc	$⊢ (R \in CRing \land A \in SubRing (R)) \to S \in CRing$

Metamath Proof Explorer