Metamath Proof Explorer

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

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	1	lidlsubg	$⊢ (R \in Ring \land I \in U) \to I \in SubGrp (R)$
5	1 2 3	lidlmcl	$⊢ ((R \in Ring \land I \in U) \land (x \in B \land y \in I)) \to x \underset{˙}{\cdot} y \in I$
6	5	ralrimivva	$⊢ (R \in Ring \land I \in U) \to \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I$
7	4 6	jca	$⊢ (R \in Ring \land I \in U) \to (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I)$
8	1 2 3	dflidl2lem	$⊢ (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I) \to I \in U$
9	8	adantl	$⊢ (R \in Ring \land (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I)) \to I \in U$
10	7 9	impbida	$⊢ R \in Ring \to (I \in U \leftrightarrow (I \in SubGrp (R) \land \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I))$