Metamath Proof Explorer

Theorem rng2idlsubg0

Description: The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025)

	Ref	Expression
Hypotheses	rng2idlsubgsubrng.r	$⊢ φ \to R \in Rng$
	rng2idlsubgsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
	rng2idlsubgsubrng.u	$⊢ φ \to I \in SubGrp (R)$
Assertion	rng2idlsubg0	$⊢ φ \to 0_{R} \in I$

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubgsubrng.r	$⊢ φ \to R \in Rng$
2		rng2idlsubgsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
3		rng2idlsubgsubrng.u	$⊢ φ \to I \in SubGrp (R)$
4	1 2 3	rng2idlsubgsubrng	$⊢ φ \to I \in SubRng (R)$
5		subrngsubg	$⊢ I \in SubRng (R) \to I \in SubGrp (R)$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	6	subg0cl	$⊢ I \in SubGrp (R) \to 0_{R} \in I$
8	4 5 7	3syl	$⊢ φ \to 0_{R} \in I$