Theorem dflidl2lem

Description: Lemma for dflidl2 : a sufficient condition for a set to be a left ideal. (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	dflidl2lem	|- ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I e. U )

Proof

Step	Hyp	Ref	Expression
1		dflidl2.u	|- U = ( LIdeal ` R )
2		dflidl2.b	|- B = ( Base ` R )
3		dflidl2.t	|- .x. = ( .r ` R )
4	2	subgss	|- ( I e. ( SubGrp ` R ) -> I C_ B )
5	4	adantr	|- ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I C_ B )
6		eqid	|- ( 0g ` R ) = ( 0g ` R )
7	6	subg0cl	|- ( I e. ( SubGrp ` R ) -> ( 0g ` R ) e. I )
8	7	ne0d	|- ( I e. ( SubGrp ` R ) -> I =/= (/) )
9	8	adantr	|- ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I =/= (/) )
10		eqid	|- ( +g ` R ) = ( +g ` R )
11	10	subgcl	|- ( ( I e. ( SubGrp ` R ) /\ ( x .x. y ) e. I /\ z e. I ) -> ( ( x .x. y ) ( +g ` R ) z ) e. I )
12	11	ad4ant134	|- ( ( ( ( I e. ( SubGrp ` R ) /\ ( x e. B /\ y e. I ) ) /\ ( x .x. y ) e. I ) /\ z e. I ) -> ( ( x .x. y ) ( +g ` R ) z ) e. I )
13	12	ralrimiva	|- ( ( ( I e. ( SubGrp ` R ) /\ ( x e. B /\ y e. I ) ) /\ ( x .x. y ) e. I ) -> A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I )
14	13	ex	|- ( ( I e. ( SubGrp ` R ) /\ ( x e. B /\ y e. I ) ) -> ( ( x .x. y ) e. I -> A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I ) )
15	14	ralimdvva	|- ( 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 A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I ) )
16	15	imp	|- ( ( 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 A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I )
17	1 2 10 3	islidl	|- ( I e. U <-> ( I C_ B /\ I =/= (/) /\ A. x e. B A. y e. I A. z e. I ( ( x .x. y ) ( +g ` R ) z ) e. I ) )
18	5 9 16 17	syl3anbrc	|- ( ( I e. ( SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) -> I e. U )