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

Proof

Step	Hyp	Ref	Expression
1		ring2idlqus	⊢ ( 𝑅 ∈ Ring → ∃ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ( ( 𝑅 ↾s 𝑖 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) ) ∈ Ring ) )
2		simpll	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s 𝑖 ) ∈ Ring ) → 𝑅 ∈ Rng )
3		simplr	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s 𝑖 ) ∈ Ring ) → 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) )
4		eqid	⊢ ( 𝑅 ↾s 𝑖 ) = ( 𝑅 ↾s 𝑖 )
5		simpr	⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s 𝑖 ) ∈ Ring ) → ( 𝑅 ↾s 𝑖 ) ∈ Ring )
6		eqid	⊢ ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) ) = ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) )
7	2 3 4 5 6	rngringbdlem2	⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s 𝑖 ) ∈ Ring ) ∧ ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) ) ∈ Ring ) → 𝑅 ∈ Ring )
8	7	expl	⊢ ( ( 𝑅 ∈ Rng ∧ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ) → ( ( ( 𝑅 ↾s 𝑖 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) ) ∈ Ring ) → 𝑅 ∈ Ring ) )
9	8	rexlimdva	⊢ ( 𝑅 ∈ Rng → ( ∃ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ( ( 𝑅 ↾s 𝑖 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) ) ∈ Ring ) → 𝑅 ∈ Ring ) )
10	1 9	impbid2	⊢ ( 𝑅 ∈ Rng → ( 𝑅 ∈ Ring ↔ ∃ 𝑖 ∈ ( 2Ideal ‘ 𝑅 ) ( ( 𝑅 ↾s 𝑖 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝑖 ) ) ∈ Ring ) ) )