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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rngringbd.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rngringbd.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rngringbd.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rngringbd.q	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
Assertion	rngringbdlem1	$$⊢\left(\phi \wedge R\in \mathrm{Ring}\right)\to Q\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		rngringbd.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rngringbd.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rngringbd.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rngringbd.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rngringbd.q	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
6	2	anim1ci	$$⊢\left(\phi \wedge R\in \mathrm{Ring}\right)\to \left(R\in \mathrm{Ring}\wedge I\in \mathrm{2Ideal}\left(R\right)\right)$$
7		eqid	$$⊢\mathrm{2Ideal}\left(R\right)=\mathrm{2Ideal}\left(R\right)$$
8	5 7	qusring	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{2Ideal}\left(R\right)\right)\to Q\in \mathrm{Ring}$$
9	6 8	syl	$$⊢\left(\phi \wedge R\in \mathrm{Ring}\right)\to Q\in \mathrm{Ring}$$