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)

	Ref	Expression
Hypotheses	df2idl2.u	|- U = ( 2Ideal ` R )
	df2idl2.b	|- B = ( Base ` R )
	df2idl2.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		df2idl2.u	|- U = ( 2Ideal ` R )
2		df2idl2.b	|- B = ( Base ` R )
3		df2idl2.t	|- .x. = ( .r ` R )
4		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
5		eqid	|- ( oppR ` R ) = ( oppR ` R )
6		eqid	|- ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
7	4 5 6 1	2idlval	|- U = ( ( LIdeal ` R ) i^i ( LIdeal ` ( oppR ` R ) ) )
8	7	elin2	|- ( I e. U <-> ( I e. ( LIdeal ` R ) /\ I e. ( LIdeal ` ( oppR ` R ) ) ) )
9	8	a1i	|- ( R e. Ring -> ( I e. U <-> ( I e. ( LIdeal ` R ) /\ I e. ( LIdeal ` ( oppR ` R ) ) ) ) )
10	4 2 3	dflidl2	|- ( R e. Ring -> ( I e. ( LIdeal ` R ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) )
11	6 2 3	isridl	|- ( R e. Ring -> ( I e. ( LIdeal ` ( oppR ` R ) ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )
12	10 11	anbi12d	|- ( R e. Ring -> ( ( I e. ( LIdeal ` R ) /\ I e. ( LIdeal ` ( oppR ` R ) ) ) <-> ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) /\ ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) ) )
13		anandi	|- ( ( I e. ( SubGrp ` R ) /\ ( A. x e. B A. y e. I ( x .x. y ) e. I /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) <-> ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) /\ ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )
14		r19.26-2	|- ( A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) <-> ( A. x e. B A. y e. I ( x .x. y ) e. I /\ A. x e. B A. y e. I ( y .x. x ) e. I ) )
15	14	bicomi	|- ( ( A. x e. B A. y e. I ( x .x. y ) e. I /\ A. x e. B A. y e. I ( y .x. x ) e. I ) <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) )
16	15	a1i	|- ( R e. Ring -> ( ( A. x e. B A. y e. I ( x .x. y ) e. I /\ A. x e. B A. y e. I ( y .x. x ) e. I ) <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
17	16	anbi2d	|- ( R e. Ring -> ( ( I e. ( SubGrp ` R ) /\ ( A. x e. B A. y e. I ( x .x. y ) e. I /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )
18	13 17	bitr3id	|- ( R e. Ring -> ( ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) /\ ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )
19	9 12 18	3bitrd	|- ( 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 ) ) ) )