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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
	rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
	rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
	rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
	rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
Assertion	rngqiprng	$$⊢\phi \to P\in \mathrm{Rng}$$

Proof

Step	Hyp	Ref	Expression
1		rng2idlring.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idlring.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idlring.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rng2idlring.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rng2idlring.b	$$⊢B={\mathrm{Base}}_R$$
6		rng2idlring.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
7		rng2idlring.1	$$⊢\underset{\dot{}}{1}=1_J$$
8		rngqiprngim.g	$$⊢\underset{\dot{}}{\sim }=R{~}_{\mathit{QG}}I$$
9		rngqiprngim.q	$$⊢Q=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
10		rngqiprngim.c	$$⊢C={\mathrm{Base}}_Q$$
11		rngqiprngim.p	$$⊢P=Q{\times }_{𝑠}J$$
12		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
13	4 12	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
14	3 13	eqeltrrid	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
15	1 2 14	rng2idlsubrng	Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-
16		subrngsubg	Could not format ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) with typecode |-
17	15 16	syl	$$⊢\phi \to I\in \mathrm{SubGrp}\left(R\right)$$
18	8	oveq2i	$$⊢R{/}_{𝑠}\underset{\dot{}}{\sim }=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
19	9 18	eqtri	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
20		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
21	19 20	qus2idrng	$$⊢\left(R\in \mathrm{Rng}\wedge I\in \mathrm{2Ideal}\left(R\right)\wedge I\in \mathrm{SubGrp}\left(R\right)\right)\to Q\in \mathrm{Rng}$$
22	1 2 17 21	syl3anc	$$⊢\phi \to Q\in \mathrm{Rng}$$
23	11 22 13	xpsrngd	$$⊢\phi \to P\in \mathrm{Rng}$$