Metamath Proof Explorer

Theorem ring2idlqus

Description: For every unital ring there is a (two-sided) ideal of the ring (in fact the base set of the ring itself) which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 13-Feb-2025)

Ref Expression
Assertion ring2idlqus ⊢R∈Ring→∃i∈2Ideal⁡RR↾𝑠i∈Ring∧R/𝑠R~QGi∈Ring

Proof

Step Hyp Ref Expression
1 eqid ⊢2Ideal⁡R=2Ideal⁡R
2 eqid ⊢BaseR=BaseR
3 1 2 2idl1 ⊢R∈Ring→BaseR∈2Ideal⁡R
4 oveq2 ⊢i=BaseR→R↾𝑠i=R↾𝑠BaseR
5 4 eleq1d ⊢i=BaseR→R↾𝑠i∈Ring↔R↾𝑠BaseR∈Ring
6 oveq2 ⊢i=BaseR→R~QGi=R~QGBaseR
7 6 oveq2d ⊢i=BaseR→R/𝑠R~QGi=R/𝑠R~QGBaseR
8 7 eleq1d ⊢i=BaseR→R/𝑠R~QGi∈Ring↔R/𝑠R~QGBaseR∈Ring
9 5 8 anbi12d ⊢i=BaseR→R↾𝑠i∈Ring∧R/𝑠R~QGi∈Ring↔R↾𝑠BaseR∈Ring∧R/𝑠R~QGBaseR∈Ring
10 9 adantl ⊢R∈Ring∧i=BaseR→R↾𝑠i∈Ring∧R/𝑠R~QGi∈Ring↔R↾𝑠BaseR∈Ring∧R/𝑠R~QGBaseR∈Ring
11 2 subrgid ⊢R∈Ring→BaseR∈SubRing⁡R
12 eqid ⊢R↾𝑠BaseR=R↾𝑠BaseR
13 12 subrgring ⊢BaseR∈SubRing⁡R→R↾𝑠BaseR∈Ring
14 11 13 syl ⊢R∈Ring→R↾𝑠BaseR∈Ring
15 eqid ⊢R/𝑠R~QGBaseR=R/𝑠R~QGBaseR
16 15 1 qusring ⊢R∈Ring∧BaseR∈2Ideal⁡R→R/𝑠R~QGBaseR∈Ring
17 3 16 mpdan ⊢R∈Ring→R/𝑠R~QGBaseR∈Ring
18 14 17 jca ⊢R∈Ring→R↾𝑠BaseR∈Ring∧R/𝑠R~QGBaseR∈Ring
19 3 10 18 rspcedvd ⊢R∈Ring→∃i∈2Ideal⁡RR↾𝑠i∈Ring∧R/𝑠R~QGi∈Ring