Metamath Proof Explorer

Theorem issubrg3

Description: A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Hypothesis	issubrg3.m	$⊢ M = {mulGrp}_{R}$
	Assertion	issubrg3	$⊢ R \in Ring \to (S \in SubRing (R) \leftrightarrow (S \in SubGrp (R) \land S \in SubMnd (M)))$

Proof

Step	Hyp	Ref	Expression
1		issubrg3.m	$⊢ M = {mulGrp}_{R}$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5	2 3 4	issubrg2	$⊢ R \in Ring \to (S \in SubRing (R) \leftrightarrow (S \in SubGrp (R) \land 1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S))$
6		3anass	$⊢ (S \in SubGrp (R) \land 1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S) \leftrightarrow (S \in SubGrp (R) \land (1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S))$
7	5 6	bitrdi	$⊢ R \in Ring \to (S \in SubRing (R) \leftrightarrow (S \in SubGrp (R) \land (1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S)))$
8	1	ringmgp	$⊢ R \in Ring \to M \in Mnd$
9	2	subgss	$⊢ S \in SubGrp (R) \to S \subseteq {Base}_{R}$
10	1 2	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
11	1 3	ringidval	$⊢ 1_{R} = 0_{M}$
12	1 4	mgpplusg	$⊢ \cdot_{R} = +_{M}$
13	10 11 12	issubm	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{R} \land 1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S))$
14		3anass	$⊢ (S \subseteq {Base}_{R} \land 1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S) \leftrightarrow (S \subseteq {Base}_{R} \land (1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S))$
15	13 14	bitrdi	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{R} \land (1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S)))$
16	15	baibd	$⊢ (M \in Mnd \land S \subseteq {Base}_{R}) \to (S \in SubMnd (M) \leftrightarrow (1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S))$
17	8 9 16	syl2an	$⊢ (R \in Ring \land S \in SubGrp (R)) \to (S \in SubMnd (M) \leftrightarrow (1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S))$
18	17	pm5.32da	$⊢ R \in Ring \to ((S \in SubGrp (R) \land S \in SubMnd (M)) \leftrightarrow (S \in SubGrp (R) \land (1_{R} \in S \land \forall x \in S \forall y \in S x \cdot_{R} y \in S)))$
19	7 18	bitr4d	$⊢ R \in Ring \to (S \in SubRing (R) \leftrightarrow (S \in SubGrp (R) \land S \in SubMnd (M)))$