Theorem rngringbdlem1

Description: In a unital ring, the quotient of the ring and a two-sided ideal is unital. (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	rngringbdlem1	|- ( ( 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	2	anim1ci	|- ( ( ph /\ R e. Ring ) -> ( R e. Ring /\ I e. ( 2Ideal ` R ) ) )
7		eqid	|- ( 2Ideal ` R ) = ( 2Ideal ` R )
8	5 7	qusring	|- ( ( R e. Ring /\ I e. ( 2Ideal ` R ) ) -> Q e. Ring )
9	6 8	syl	|- ( ( ph /\ R e. Ring ) -> Q e. Ring )