dflidl2rng

Description: Alternate (the usual textbook) definition of a (left) ideal of a non-unital 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, 21-Mar-2025)

	Ref	Expression
Hypotheses	dflidl2rng.u	$⊢ U = LIdeal (R)$
	dflidl2rng.b	$⊢ B = {Base}_{R}$
	dflidl2rng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	dflidl2rng	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I)$

Proof

Step	Hyp	Ref	Expression
1		dflidl2rng.u	$⊢ U = LIdeal (R)$
2		dflidl2rng.b	$⊢ B = {Base}_{R}$
3		dflidl2rng.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		simpll	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land I \in U) \to R \in Rng$
5		simpr	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land I \in U) \to I \in U$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	6	subg0cl	$⊢ I \in SubGrp (R) \to 0_{R} \in I$
8	7	ad2antlr	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land I \in U) \to 0_{R} \in I$
9	4 5 8	3jca	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land I \in U) \to (R \in Rng \land I \in U \land 0_{R} \in I)$
10	6 2 3 1	rnglidlmcl	$⊢ ((R \in Rng \land I \in U \land 0_{R} \in I) \land (x \in B \land y \in I)) \to x \underset{˙}{\cdot} y \in I$
11	9 10	sylan	$⊢ (((R \in Rng \land I \in SubGrp (R)) \land I \in U) \land (x \in B \land y \in I)) \to x \underset{˙}{\cdot} y \in I$
12	11	ralrimivva	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land I \in U) \to \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I$
13	2	subgss	$⊢ I \in SubGrp (R) \to I \subseteq B$
14	13	ad2antlr	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \subseteq B$
15	7	ne0d	$⊢ I \in SubGrp (R) \to I \neq \emptyset$
16	15	ad2antlr	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \neq \emptyset$
17		eqid	$⊢ +_{R} = +_{R}$
18	17	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$
19	18	ad5ant245	$⊢ ((((R \in Rng \land 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$
20	19	ralrimiva	$⊢ (((R \in Rng \land 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$
21	20	ex	$⊢ ((R \in Rng \land 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)$
22	21	ralimdvva	$⊢ (R \in Rng \land 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)$
23	22	imp	$⊢ ((R \in Rng \land 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$
24	1 2 17 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)$
25	14 16 23 24	syl3anbrc	$⊢ ((R \in Rng \land I \in SubGrp (R)) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \in U$
26	12 25	impbida	$⊢ (R \in Rng \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I)$

Metamath Proof Explorer

Theorem dflidl2rng

Proof