df2idl2rng

Description: Alternate (the usual textbook) definition of a two-sided ideal of a non-unital 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 AV, 21-Mar-2025)

	Ref	Expression
Hypotheses	df2idl2rng.u	$⊢ U = 2Ideal (R)$
	df2idl2rng.b	$⊢ B = {Base}_{R}$
	df2idl2rng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	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))$

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		eqid	$⊢ LIdeal (R) = LIdeal (R)$
5	4 2 3	dflidl2rng	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in LIdeal (R) \leftrightarrow \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I)$
6		eqid	$⊢ LIdeal ({opp}_{r} (R)) = LIdeal ({opp}_{r} (R))$
7	6 2 3	isridlrng	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in LIdeal ({opp}_{r} (R)) \leftrightarrow \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I)$
8	5 7	anbi12d	$⊢ (R \in Rng \land I \in SubGrp (R)) \to ((I \in LIdeal (R) \land I \in LIdeal ({opp}_{r} (R))) \leftrightarrow (\forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I))$
9		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
10	4 9 6 1	2idlelb	$⊢ I \in U \leftrightarrow (I \in LIdeal (R) \land I \in LIdeal ({opp}_{r} (R)))$
11		r19.26-2	$⊢ \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I) \leftrightarrow (\forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I)$
12	8 10 11	3bitr4g	$⊢ (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))$

Metamath Proof Explorer

Theorem df2idl2rng

Proof