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	|- ( ph -> R e. Rng )
	rngringbd.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rngringbd.j	|- J = ( R |`s I )
	rngringbd.u	|- ( ph -> J e. Ring )
	rngringbd.q	|- Q = ( R /s ( R ~QG I ) )
Assertion	rngringbd	|- ( ph -> ( R e. Ring <-> Q e. Ring ) )

Proof

Step	Hyp	Ref	Expression
1		rngringbd.r	|- ( ph -> R e. Rng )
2		rngringbd.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rngringbd.j	|- J = ( R |`s I )
4		rngringbd.u	|- ( ph -> J e. Ring )
5		rngringbd.q	|- Q = ( R /s ( R ~QG I ) )
6	1 2 3 4 5	rngringbdlem1	|- ( ( ph /\ R e. Ring ) -> Q e. Ring )
7	1 2 3 4 5	rngringbdlem2	|- ( ( ph /\ Q e. Ring ) -> R e. Ring )
8	6 7	impbida	|- ( ph -> ( R e. Ring <-> Q e. Ring ) )