Theorem dflidl2

Description: Alternate (the usual textbook) definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dflidl2.u	|- U = ( LIdeal ` R )
2		dflidl2.b	|- B = ( Base ` R )
3		dflidl2.t	|- .x. = ( .r ` R )
4	1	lidlsubg	|- ( ( R e. Ring /\ I e. U ) -> I e. ( SubGrp ` R ) )
5	1 2 3	lidlmcl	|- ( ( ( R e. Ring /\ I e. U ) /\ ( x e. B /\ y e. I ) ) -> ( x .x. y ) e. I )
6	5	ralrimivva	|- ( ( R e. Ring /\ I e. U ) -> A. x e. B A. y e. I ( x .x. y ) e. I )
7	4 6	jca	|- ( ( R e. Ring /\ I e. U ) -> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) )
8	1 2 3	dflidl2lem	|- ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I e. U )
9	8	adantl	|- ( ( R e. Ring /\ ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) -> I e. U )
10	7 9	impbida	|- ( R e. Ring -> ( I e. U <-> ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) )