Theorem ring2idlqusb

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
Assertion	ring2idlqusb	|- ( R e. Rng -> ( R e. Ring <-> E. i e. ( 2Ideal ` R ) ( ( R |`s i ) e. Ring /\ ( R /s ( R ~QG i ) ) e. Ring ) ) )

Proof

Step	Hyp	Ref	Expression
1		ring2idlqus	|- ( R e. Ring -> E. i e. ( 2Ideal ` R ) ( ( R |`s i ) e. Ring /\ ( R /s ( R ~QG i ) ) e. Ring ) )
2		simpll	|- ( ( ( R e. Rng /\ i e. ( 2Ideal ` R ) ) /\ ( R |`s i ) e. Ring ) -> R e. Rng )
3		simplr	|- ( ( ( R e. Rng /\ i e. ( 2Ideal ` R ) ) /\ ( R |`s i ) e. Ring ) -> i e. ( 2Ideal ` R ) )
4		eqid	|- ( R |`s i ) = ( R |`s i )
5		simpr	|- ( ( ( R e. Rng /\ i e. ( 2Ideal ` R ) ) /\ ( R |`s i ) e. Ring ) -> ( R |`s i ) e. Ring )
6		eqid	|- ( R /s ( R ~QG i ) ) = ( R /s ( R ~QG i ) )
7	2 3 4 5 6	rngringbdlem2	|- ( ( ( ( R e. Rng /\ i e. ( 2Ideal ` R ) ) /\ ( R |`s i ) e. Ring ) /\ ( R /s ( R ~QG i ) ) e. Ring ) -> R e. Ring )
8	7	expl	|- ( ( R e. Rng /\ i e. ( 2Ideal ` R ) ) -> ( ( ( R |`s i ) e. Ring /\ ( R /s ( R ~QG i ) ) e. Ring ) -> R e. Ring ) )
9	8	rexlimdva	|- ( R e. Rng -> ( E. i e. ( 2Ideal ` R ) ( ( R |`s i ) e. Ring /\ ( R /s ( R ~QG i ) ) e. Ring ) -> R e. Ring ) )
10	1 9	impbid2	|- ( R e. Rng -> ( R e. Ring <-> E. i e. ( 2Ideal ` R ) ( ( R |`s i ) e. Ring /\ ( R /s ( R ~QG i ) ) e. Ring ) ) )