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 ( 𝑅 ∈ Ring → ∃ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ( ( 𝑅 ↾s 𝑖 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) ) ∈ Ring ) )

Proof

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