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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rngringbd.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rngringbd.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rngringbd.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rngringbd.q	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
Assertion	rngringbd	$$⊢\phi \to \left(R\in \mathrm{Ring}\leftrightarrow Q\in \mathrm{Ring}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rngringbd.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rngringbd.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rngringbd.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rngringbd.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rngringbd.q	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
6	1 2 3 4 5	rngringbdlem1	$$⊢\left(\phi \wedge R\in \mathrm{Ring}\right)\to Q\in \mathrm{Ring}$$
7	1 2 3 4 5	rngringbdlem2	$$⊢\left(\phi \wedge Q\in \mathrm{Ring}\right)\to R\in \mathrm{Ring}$$
8	6 7	impbida	$$⊢\phi \to \left(R\in \mathrm{Ring}\leftrightarrow Q\in \mathrm{Ring}\right)$$