Theorem rngqiprng

Description: The product of the quotient with a two-sided ideal and the two-sided ideal is a non-unital ring. (Contributed by AV, 23-Feb-2025)

	Ref	Expression
Hypotheses	rng2idlring.r	|- ( ph -> R e. Rng )
	rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idlring.j	|- J = ( R |`s I )
	rng2idlring.u	|- ( ph -> J e. Ring )
	rng2idlring.b	|- B = ( Base ` R )
	rng2idlring.t	|- .x. = ( .r ` R )
	rng2idlring.1	|- .1. = ( 1r ` J )
	rngqiprngim.g	|- .~ = ( R ~QG I )
	rngqiprngim.q	|- Q = ( R /s .~ )
	rngqiprngim.c	|- C = ( Base ` Q )
	rngqiprngim.p	|- P = ( Q Xs. J )
Assertion	rngqiprng	|- ( ph -> P e. Rng )

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	|- ( ph -> R e. Rng )
2		rng2idlring.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rng2idlring.j	|- J = ( R |`s I )
4		rng2idlring.u	|- ( ph -> J e. Ring )
5		rng2idlring.b	|- B = ( Base ` R )
6		rng2idlring.t	|- .x. = ( .r ` R )
7		rng2idlring.1	|- .1. = ( 1r ` J )
8		rngqiprngim.g	|- .~ = ( R ~QG I )
9		rngqiprngim.q	|- Q = ( R /s .~ )
10		rngqiprngim.c	|- C = ( Base ` Q )
11		rngqiprngim.p	|- P = ( Q Xs. J )
12		ringrng	|- ( J e. Ring -> J e. Rng )
13	4 12	syl	|- ( ph -> J e. Rng )
14	3 13	eqeltrrid	|- ( ph -> ( R |`s I ) e. Rng )
15	1 2 14	rng2idlsubrng	|- ( ph -> I e. ( SubRng ` R ) )
16		subrngsubg	|- ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) )
17	15 16	syl	|- ( ph -> I e. ( SubGrp ` R ) )
18	8	oveq2i	|- ( R /s .~ ) = ( R /s ( R ~QG I ) )
19	9 18	eqtri	|- Q = ( R /s ( R ~QG I ) )
20		eqid	|- ( 2Ideal ` R ) = ( 2Ideal ` R )
21	19 20	qus2idrng	|- ( ( R e. Rng /\ I e. ( 2Ideal ` R ) /\ I e. ( SubGrp ` R ) ) -> Q e. Rng )
22	1 2 17 21	syl3anc	|- ( ph -> Q e. Rng )
23	11 22 13	xpsrngd	|- ( ph -> P e. Rng )