Theorem 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) (Proof shortened by AV, 18-Apr-2025)

	Ref	Expression
Hypotheses	df2idl2rng.u	|- U = ( 2Ideal ` R )
	df2idl2rng.b	|- B = ( Base ` R )
	df2idl2rng.t	|- .x. = ( .r ` R )
Assertion	df2idl2	|- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df2idl2rng.u	|- U = ( 2Ideal ` R )
2		df2idl2rng.b	|- B = ( Base ` R )
3		df2idl2rng.t	|- .x. = ( .r ` R )
4	1	eleq2i	|- ( I e. U <-> I e. ( 2Ideal ` R ) )
5	4	biimpi	|- ( I e. U -> I e. ( 2Ideal ` R ) )
6	5	2idllidld	|- ( I e. U -> I e. ( LIdeal ` R ) )
7		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
8	7	lidlsubg	|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) -> I e. ( SubGrp ` R ) )
9	6 8	sylan2	|- ( ( R e. Ring /\ I e. U ) -> I e. ( SubGrp ` R ) )
10		ringrng	|- ( R e. Ring -> R e. Rng )
11	1 2 3	df2idl2rng	|- ( ( R e. Rng /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
12	10 11	sylan	|- ( ( R e. Ring /\ I e. ( SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
13	9 12	biadanid	|- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )