Metamath Proof Explorer

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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	dflidl2lem	$⊢ (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \in U$

Proof

Step	Hyp	Ref	Expression
1		dflidl2.u	$⊢ U = LIdeal (R)$
2		dflidl2.b	$⊢ B = {Base}_{R}$
3		dflidl2.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4	2	subgss	$⊢ I \in SubGrp (R) \to I \subseteq B$
5	4	adantr	$⊢ (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \subseteq B$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	6	subg0cl	$⊢ I \in SubGrp (R) \to 0_{R} \in I$
8	7	ne0d	$⊢ I \in SubGrp (R) \to I \neq \emptyset$
9	8	adantr	$⊢ (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \neq \emptyset$
10		eqid	$⊢ +_{R} = +_{R}$
11	10	subgcl	$⊢ (I \in SubGrp (R) \land x \underset{˙}{\cdot} y \in I \land z \in I) \to (x \underset{˙}{\cdot} y) +_{R} z \in I$
12	11	ad4ant134	$⊢ (((I \in SubGrp (R) \land (x \in B \land y \in I)) \land x \underset{˙}{\cdot} y \in I) \land z \in I) \to (x \underset{˙}{\cdot} y) +_{R} z \in I$
13	12	ralrimiva	$⊢ ((I \in SubGrp (R) \land (x \in B \land y \in I)) \land x \underset{˙}{\cdot} y \in I) \to \forall z \in I (x \underset{˙}{\cdot} y) +_{R} z \in I$
14	13	ex	$⊢ (I \in SubGrp (R) \land (x \in B \land y \in I)) \to (x \underset{˙}{\cdot} y \in I \to \forall z \in I (x \underset{˙}{\cdot} y) +_{R} z \in I)$
15	14	ralimdvva	$⊢ I \in SubGrp (R) \to (\forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I \to \forall x \in B \forall y \in I \forall z \in I (x \underset{˙}{\cdot} y) +_{R} z \in I)$
16	15	imp	$⊢ (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to \forall x \in B \forall y \in I \forall z \in I (x \underset{˙}{\cdot} y) +_{R} z \in I$
17	1 2 10 3	islidl	$⊢ I \in U \leftrightarrow (I \subseteq B \land I \neq \emptyset \land \forall x \in B \forall y \in I \forall z \in I (x \underset{˙}{\cdot} y) +_{R} z \in I)$
18	5 9 16 17	syl3anbrc	$⊢ (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \in U$