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 ⁡ R R ↾ 𝑠 i ∈ Ring ∧ R / 𝑠 R ~ QG i ∈ Ring

Proof

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