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) (Proof shortened by AV, 18-Apr-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		ringrng	$⊢ R \in Ring \to R \in Rng$
6	1 2 3	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)$
7	5 6	sylan	$⊢ (R \in Ring \land I \in SubGrp (R)) \to (I \in U \leftrightarrow \forall x \in B \forall y \in I x \underset{˙}{\cdot} y \in I)$
8	4 7	biadanid	$⊢ 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))$

Metamath Proof Explorer

Theorem dflidl2

Proof