This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rng2idl0

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

	Ref	Expression
Hypotheses	rng2idlsubrng.r	$⊢ φ \to R \in Rng$
	rng2idlsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
	rng2idlsubrng.u	$⊢ φ \to R ↾_{𝑠} I \in Rng$
Assertion	rng2idl0	$⊢ φ \to 0_{R} \in I$

Proof

Step	Hyp	Ref	Expression
1		rng2idlsubrng.r	$⊢ φ \to R \in Rng$
2		rng2idlsubrng.i	$⊢ φ \to I \in 2Ideal (R)$
3		rng2idlsubrng.u	$⊢ φ \to R ↾_{𝑠} I \in Rng$
4	1 2 3	rng2idlsubrng	$⊢ φ \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$