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 AV, 13-Feb-2025)

	Ref	Expression
Hypotheses	df2idl2.u	$⊢ U = 2Ideal (R)$
	df2idl2.b	$⊢ B = {Base}_{R}$
	df2idl2.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		df2idl2.u	$⊢ U = 2Ideal (R)$
2		df2idl2.b	$⊢ B = {Base}_{R}$
3		df2idl2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ LIdeal (R) = LIdeal (R)$
5		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
6		eqid	$⊢ LIdeal ({opp}_{r} (R)) = LIdeal ({opp}_{r} (R))$
7	4 5 6 1	2idlval	$⊢ U = LIdeal (R) \cap LIdeal ({opp}_{r} (R))$
8	7	elin2	$⊢ I \in U \leftrightarrow (I \in LIdeal (R) \land I \in LIdeal ({opp}_{r} (R)))$
9	8	a1i	$⊢ R \in Ring \to (I \in U \leftrightarrow (I \in LIdeal (R) \land I \in LIdeal ({opp}_{r} (R))))$
10	4 2 3	dflidl2	$⊢ R \in Ring \to (I \in LIdeal (R) \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I))$
11	6 2 3	isridl	$⊢ R \in Ring \to (I \in LIdeal ({opp}_{r} (R)) \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I))$
12	10 11	anbi12d	$⊢ R \in Ring \to ((I \in LIdeal (R) \land I \in LIdeal ({opp}_{r} (R))) \leftrightarrow ((I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \land (I \in SubGrp (R) \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I)))$
13		anandi	$⊢ (I \in SubGrp (R) \land (\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)) \leftrightarrow ((I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \land (I \in SubGrp (R) \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I))$
14		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)$
15	14	bicomi	$⊢ (\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) \leftrightarrow \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I)$
16	15	a1i	$⊢ R \in Ring \to ((\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) \leftrightarrow \forall x \in B \forall y \in I (x \underset{˙}{\cdot} y \in I \land y \underset{˙}{\cdot} x \in I))$
17	16	anbi2d	$⊢ R \in Ring \to ((I \in SubGrp (R) \land (\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)) \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)))$
18	13 17	bitr3id	$⊢ R \in Ring \to (((I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \land (I \in SubGrp (R) \land \forall x \in B \forall y \in I y \underset{˙}{\cdot} x \in I)) \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)))$
19	9 12 18	3bitrd	$⊢ 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