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	|- U = ( R /s ( R ~QG S ) )
	qusring.i	|- I = ( 2Ideal ` R )
Assertion	qusring	|- ( ( R e. Ring /\ S e. I ) -> U e. Ring )

Proof

Step	Hyp	Ref	Expression
1		qusring.u	|- U = ( R /s ( R ~QG S ) )
2		qusring.i	|- I = ( 2Ideal ` R )
3		eqid	|- ( 1r ` R ) = ( 1r ` R )
4	1 2 3	qus1	|- ( ( R e. Ring /\ S e. I ) -> ( U e. Ring /\ [ ( 1r ` R ) ] ( R ~QG S ) = ( 1r ` U ) ) )
5	4	simpld	|- ( ( R e. Ring /\ S e. I ) -> U e. Ring )