Metamath Proof Explorer

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 ⊢ φ → R ∈ Rng
rngringbd.i ⊢ φ → I ∈ 2Ideal ⁡ R
rngringbd.j ⊢ J = R ↾ 𝑠 I
rngringbd.u ⊢ φ → J ∈ Ring
rngringbd.q ⊢ Q = R / 𝑠 R ~ QG I
Assertion rngringbdlem1 ⊢ φ ∧ R ∈ Ring → Q ∈ Ring

Proof

Step Hyp Ref Expression
1 rngringbd.r ⊢ φ → R ∈ Rng
2 rngringbd.i ⊢ φ → I ∈ 2Ideal ⁡ R
3 rngringbd.j ⊢ J = R ↾ 𝑠 I
4 rngringbd.u ⊢ φ → J ∈ Ring
5 rngringbd.q ⊢ Q = R / 𝑠 R ~ QG I
6 2 anim1ci ⊢ φ ∧ R ∈ Ring → R ∈ Ring ∧ I ∈ 2Ideal ⁡ R
7 eqid ⊢ 2Ideal ⁡ R = 2Ideal ⁡ R
8 5 7 qusring ⊢ R ∈ Ring ∧ I ∈ 2Ideal ⁡ R → Q ∈ Ring
9 6 8 syl ⊢ φ ∧ R ∈ Ring → Q ∈ Ring