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 ⊢ ( 𝜑 → 𝑅 ∈ Rng )
rngringbd.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
rngringbd.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
rngringbd.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
rngringbd.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
Assertion rngringbdlem2 ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → 𝑅 ∈ Ring )

Proof

Step Hyp Ref Expression
1 rngringbd.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
2 rngringbd.i ⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
3 rngringbd.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 rngringbd.u ⊢ ( 𝜑 → 𝐽 ∈ Ring )
5 rngringbd.q ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
6 eqid ⊢ ( 𝑄 ×s 𝐽 ) = ( 𝑄 ×s 𝐽 )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → 𝑄 ∈ Ring )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → 𝐽 ∈ Ring )
9 6 7 8 xpsringd ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → ( 𝑄 ×s 𝐽 ) ∈ Ring )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → 𝑅 ∈ Rng )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
14 eqid ⊢ ( 1r ‘ 𝐽 ) = ( 1r ‘ 𝐽 )
15 eqid ⊢ ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG 𝐼 )
16 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
17 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ⟨ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) , ( ( 1r ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝑥 ) ⟩ ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ⟨ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) , ( ( 1r ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝑥 ) ⟩ )
18 10 11 3 8 12 13 14 15 5 16 6 17 rngqiprngim ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ⟨ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) , ( ( 1r ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝑥 ) ⟩ ) ∈ ( 𝑅 RngIso ( 𝑄 ×s 𝐽 ) ) )
19 rngimcnv ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ⟨ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) , ( ( 1r ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝑥 ) ⟩ ) ∈ ( 𝑅 RngIso ( 𝑄 ×s 𝐽 ) ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ⟨ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) , ( ( 1r ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝑥 ) ⟩ ) ∈ ( ( 𝑄 ×s 𝐽 ) RngIso 𝑅 ) )
20 18 19 syl ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ⟨ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) , ( ( 1r ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝑥 ) ⟩ ) ∈ ( ( 𝑄 ×s 𝐽 ) RngIso 𝑅 ) )
21 rngisomring ⊢ ( ( ( 𝑄 ×s 𝐽 ) ∈ Ring ∧ 𝑅 ∈ Rng ∧ ◡ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ⟨ [ 𝑥 ] ( 𝑅 ~QG 𝐼 ) , ( ( 1r ‘ 𝐽 ) ( .r ‘ 𝑅 ) 𝑥 ) ⟩ ) ∈ ( ( 𝑄 ×s 𝐽 ) RngIso 𝑅 ) ) → 𝑅 ∈ Ring )
22 9 10 20 21 syl3anc ⊢ ( ( 𝜑 ∧ 𝑄 ∈ Ring ) → 𝑅 ∈ Ring )