Metamath Proof Explorer

Theorem rngringbdlem2

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, 14-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 rngringbdlem2 ⊢ φ ∧ Q ∈ Ring → R ∈ 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 eqid ⊢ Q × 𝑠 J = Q × 𝑠 J
7 simpr ⊢ φ ∧ Q ∈ Ring → Q ∈ Ring
8 4 adantr ⊢ φ ∧ Q ∈ Ring → J ∈ Ring
9 6 7 8 xpsringd ⊢ φ ∧ Q ∈ Ring → Q × 𝑠 J ∈ Ring
10 1 adantr ⊢ φ ∧ Q ∈ Ring → R ∈ Rng
11 2 adantr ⊢ φ ∧ Q ∈ Ring → I ∈ 2Ideal ⁡ R
12 eqid ⊢ Base R = Base R
13 eqid ⊢ ⋅ R = ⋅ R
14 eqid ⊢ 1 J = 1 J
15 eqid ⊢ R ~ QG I = R ~ QG I
16 eqid ⊢ Base Q = Base Q
17 eqid ⊢ x ∈ Base R ⟼ x R ~ QG I 1 J ⋅ R x = x ∈ Base R ⟼ x R ~ QG I 1 J ⋅ R x
18 10 11 3 8 12 13 14 15 5 16 6 17 rngqiprngim ⊢ φ ∧ Q ∈ Ring → x ∈ Base R ⟼ x R ~ QG I 1 J ⋅ R x ∈ R RngIso Q × 𝑠 J
19 rngimcnv ⊢ x ∈ Base R ⟼ x R ~ QG I 1 J ⋅ R x ∈ R RngIso Q × 𝑠 J → x ∈ Base R ⟼ x R ~ QG I 1 J ⋅ R x -1 ∈ Q × 𝑠 J RngIso R
20 18 19 syl ⊢ φ ∧ Q ∈ Ring → x ∈ Base R ⟼ x R ~ QG I 1 J ⋅ R x -1 ∈ Q × 𝑠 J RngIso R
21 rngisomring ⊢ Q × 𝑠 J ∈ Ring ∧ R ∈ Rng ∧ x ∈ Base R ⟼ x R ~ QG I 1 J ⋅ R x -1 ∈ Q × 𝑠 J RngIso R → R ∈ Ring
22 9 10 20 21 syl3anc ⊢ φ ∧ Q ∈ Ring → R ∈ Ring