subrgsubm

Description: A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015)

		Ref	Expression
	Hypothesis	subrgsubm.1	$⊢ M = {mulGrp}_{R}$
	Assertion	subrgsubm	$⊢ A \in SubRing (R) \to A \in SubMnd (M)$

Step	Hyp	Ref	Expression
1		subrgsubm.1	$⊢ M = {mulGrp}_{R}$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	2	subrgss	$⊢ A \in SubRing (R) \to A \subseteq {Base}_{R}$
4		eqid	$⊢ 1_{R} = 1_{R}$
5	4	subrg1cl	$⊢ A \in SubRing (R) \to 1_{R} \in A$
6		subrgrcl	$⊢ A \in SubRing (R) \to R \in Ring$
7		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
8	7 1	mgpress	$⊢ (R \in Ring \land A \in SubRing (R)) \to M ↾_{𝑠} A = {mulGrp}_{(R ↾_{𝑠} A)}$
9	6 8	mpancom	$⊢ A \in SubRing (R) \to M ↾_{𝑠} A = {mulGrp}_{(R ↾_{𝑠} A)}$
10	7	subrgring	$⊢ A \in SubRing (R) \to R ↾_{𝑠} A \in Ring$
11		eqid	$⊢ {mulGrp}_{(R ↾_{𝑠} A)} = {mulGrp}_{(R ↾_{𝑠} A)}$
12	11	ringmgp	$⊢ R ↾_{𝑠} A \in Ring \to {mulGrp}_{(R ↾_{𝑠} A)} \in Mnd$
13	10 12	syl	$⊢ A \in SubRing (R) \to {mulGrp}_{(R ↾_{𝑠} A)} \in Mnd$
14	9 13	eqeltrd	$⊢ A \in SubRing (R) \to M ↾_{𝑠} A \in Mnd$
15	1	ringmgp	$⊢ R \in Ring \to M \in Mnd$
16	1 2	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
17	1 4	ringidval	$⊢ 1_{R} = 0_{M}$
18		eqid	$⊢ M ↾_{𝑠} A = M ↾_{𝑠} A$
19	16 17 18	issubm2	$⊢ M \in Mnd \to (A \in SubMnd (M) \leftrightarrow (A \subseteq {Base}_{R} \land 1_{R} \in A \land M ↾_{𝑠} A \in Mnd))$
20	6 15 19	3syl	$⊢ A \in SubRing (R) \to (A \in SubMnd (M) \leftrightarrow (A \subseteq {Base}_{R} \land 1_{R} \in A \land M ↾_{𝑠} A \in Mnd))$
21	3 5 14 20	mpbir3and	$⊢ A \in SubRing (R) \to A \in SubMnd (M)$

Metamath Proof Explorer