Metamath Proof Explorer

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 /_{𝑠} (R ~_{QG} S)$
	qusring.i	$⊢ I = 2Ideal (R)$
Assertion	qusring	$⊢ (R \in Ring \land S \in I) \to U \in Ring$

Proof

Step	Hyp	Ref	Expression
1		qusring.u	$⊢ U = R /_{𝑠} (R ~_{QG} S)$
2		qusring.i	$⊢ I = 2Ideal (R)$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	1 2 3	qus1	$⊢ (R \in Ring \land S \in I) \to (U \in Ring \land [1_{R}] (R ~_{QG} S) = 1_{U})$
5	4	simpld	$⊢ (R \in Ring \land S \in I) \to U \in Ring$