Metamath Proof Explorer

Theorem rngringbd

Description: A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (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 rngringbd ⊢ φ → 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 1 2 3 4 5 rngringbdlem1 ⊢ φ ∧ R ∈ Ring → Q ∈ Ring
7 1 2 3 4 5 rngringbdlem2 ⊢ φ ∧ Q ∈ Ring → R ∈ Ring
8 6 7 impbida ⊢ φ → R ∈ Ring ↔ Q ∈ Ring