Theorem rngringbd

Description: A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 20-Feb-2025)

	Ref	Expression
Hypotheses	rngringbd.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rngringbd.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rngringbd.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	rngringbd.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
	rngringbd.q	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
Assertion	rngringbd	⊢ ( 𝜑 → ( 𝑅 ∈ Ring ↔ 𝑄 ∈ Ring ) )

Proof

Step	Hyp	Ref	Expression
1		rngringbd.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rngringbd.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rngringbd.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4		rngringbd.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
5		rngringbd.q	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
6	1 2 3 4 5	rngringbdlem1	⊢ ( ( 𝜑 ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
7	1 2 3 4 5	rngringbdlem2	⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → 𝑅 ∈ Ring )
8	6 7	impbida	⊢ ( 𝜑 → ( 𝑅 ∈ Ring ↔ 𝑄 ∈ Ring ) )