subrgsubg

Description: A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014)

		Ref	Expression
	Assertion	subrgsubg	$⊢ A \in SubRing (R) \to A \in SubGrp (R)$

Step	Hyp	Ref	Expression
1		subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$
2		ringgrp	$⊢ R \in Ring \to R \in Grp$
3	1 2	syl	$⊢ A \in SubRing (R) \to R \in Grp$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
6		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
7	6	subrgring	$⊢ A \in SubRing (R) \to R ↾_{𝑠} A \in Ring$
8		ringgrp	$⊢ R ↾_{𝑠} A \in Ring \to R ↾_{𝑠} A \in Grp$
9	7 8	syl	$⊢ A \in SubRing (R) \to R ↾_{𝑠} A \in Grp$
10	4	issubg	$⊢ A \in SubGrp (R) \leftrightarrow (R \in Grp \land A \subseteq {Base}_{R} \land R ↾_{𝑠} A \in Grp)$
11	3 5 9 10	syl3anbrc	$⊢ A \in SubRing (R) \to A \in SubGrp (R)$

Metamath Proof Explorer