subrngsubg

		Ref	Expression
	Assertion	subrngsubg	$⊢ A \in SubRng (R) \to A \in SubGrp (R)$

Step	Hyp	Ref	Expression
1		subrngrcl	$⊢ A \in SubRng (R) \to R \in Rng$
2		rnggrp	$⊢ R \in Rng \to R \in Grp$
3	1 2	syl	$⊢ A \in SubRng (R) \to R \in Grp$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4	subrngss	$⊢ A \in SubRng (R) \to A \subseteq {Base}_{R}$
6		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
7	6	subrngrng	$⊢ A \in SubRng (R) \to R ↾_{𝑠} A \in Rng$
8		rnggrp	$⊢ R ↾_{𝑠} A \in Rng \to R ↾_{𝑠} A \in Grp$
9	7 8	syl	$⊢ A \in SubRng (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 SubRng (R) \to A \in SubGrp (R)$

Metamath Proof Explorer