df2idl2

Description: Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 13-Feb-2025) (Proof shortened by AV, 18-Apr-2025)

	Ref	Expression
Hypotheses	df2idl2rng.u	$⊢ U = 2Ideal (R)$
	df2idl2rng.b	$⊢ B = {Base}_{R}$
	df2idl2rng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	df2idl2	$⊢ R \in Ring \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I)))$

Proof

Step	Hyp	Ref	Expression
1		df2idl2rng.u	$⊢ U = 2Ideal (R)$
2		df2idl2rng.b	$⊢ B = {Base}_{R}$
3		df2idl2rng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4	1	eleq2i	$⊢ I \in U \leftrightarrow I \in 2Ideal (R)$
5	4	biimpi	$⊢ I \in U \to I \in 2Ideal (R)$
6	5	2idllidld	$⊢ I \in U \to I \in LIdeal (R)$
7		eqid	$⊢ LIdeal (R) = LIdeal (R)$
8	7	lidlsubg	$⊢ (R \in Ring \land I \in LIdeal (R)) \to I \in SubGrp (R)$
9	6 8	sylan2	$⊢ (R \in Ring \land I \in U) \to I \in SubGrp (R)$
10		ringrng	$⊢ R \in Ring \to R \in Rng$
11	1 2 3	df2idl2rng	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I))$
12	10 11	sylan	$⊢ (R \in Ring \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I))$
13	9 12	biadanid	$⊢ R \in Ring \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I)))$

Metamath Proof Explorer

Theorem df2idl2

Proof