Metamath Proof Explorer

Theorem ring2idlqusb

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
Assertion ring2idlqusb ⊢ R ∈ Rng → R ∈ Ring ↔ ∃ i ∈ 2Ideal ⁡ R R ↾ 𝑠 i ∈ Ring ∧ R / 𝑠 R ~ QG i ∈ Ring

Proof

Step Hyp Ref Expression
1 ring2idlqus ⊢ R ∈ Ring → ∃ i ∈ 2Ideal ⁡ R R ↾ 𝑠 i ∈ Ring ∧ R / 𝑠 R ~ QG i ∈ Ring
2 simpll ⊢ R ∈ Rng ∧ i ∈ 2Ideal ⁡ R ∧ R ↾ 𝑠 i ∈ Ring → R ∈ Rng
3 simplr ⊢ R ∈ Rng ∧ i ∈ 2Ideal ⁡ R ∧ R ↾ 𝑠 i ∈ Ring → i ∈ 2Ideal ⁡ R
4 eqid ⊢ R ↾ 𝑠 i = R ↾ 𝑠 i
5 simpr ⊢ R ∈ Rng ∧ i ∈ 2Ideal ⁡ R ∧ R ↾ 𝑠 i ∈ Ring → R ↾ 𝑠 i ∈ Ring
6 eqid ⊢ R / 𝑠 R ~ QG i = R / 𝑠 R ~ QG i
7 2 3 4 5 6 rngringbdlem2 ⊢ R ∈ Rng ∧ i ∈ 2Ideal ⁡ R ∧ R ↾ 𝑠 i ∈ Ring ∧ R / 𝑠 R ~ QG i ∈ Ring → R ∈ Ring
8 7 expl ⊢ R ∈ Rng ∧ i ∈ 2Ideal ⁡ R → R ↾ 𝑠 i ∈ Ring ∧ R / 𝑠 R ~ QG i ∈ Ring → R ∈ Ring
9 8 rexlimdva ⊢ R ∈ Rng → ∃ i ∈ 2Ideal ⁡ R R ↾ 𝑠 i ∈ Ring ∧ R / 𝑠 R ~ QG i ∈ Ring → R ∈ Ring
10 1 9 impbid2 ⊢ R ∈ Rng → R ∈ Ring ↔ ∃ i ∈ 2Ideal ⁡ R R ↾ 𝑠 i ∈ Ring ∧ R / 𝑠 R ~ QG i ∈ Ring