This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑈 = ( 𝑅 /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 )