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	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rngringbd.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rngringbd.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	rngringbd.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
	rngringbd.q	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
Assertion	rngringbdlem1	⊢ ( ( 𝜑 ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		rngringbd.r	⊢ ( 𝜑 → 𝑅 ∈ Rng )
2		rngringbd.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3		rngringbd.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4		rngringbd.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
5		rngringbd.q	⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
6	2	anim1ci	⊢ ( ( 𝜑 ∧ 𝑅 ∈ Ring ) → ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) )
7		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
8	5 7	qusring	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝑄 ∈ Ring )
9	6 8	syl	⊢ ( ( 𝜑 ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )