Theorem qusring

Description: If S is a two-sided ideal in R , then U = R / S is a ring, called the quotient ring of R by S . (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	qusring.u	⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
	qusring.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
Assertion	qusring	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑈 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		qusring.u	⊢ 𝑈 = ( 𝑅 /s ( 𝑅 ~QG 𝑆 ) )
2		qusring.i	⊢ 𝐼 = ( 2Ideal ‘ 𝑅 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	1 2 3	qus1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → ( 𝑈 ∈ Ring ∧ [ ( 1r ‘ 𝑅 ) ] ( 𝑅 ~QG 𝑆 ) = ( 1r ‘ 𝑈 ) ) )
5	4	simpld	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐼 ) → 𝑈 ∈ Ring )