Metamath Proof Explorer

Theorem ring2idlqus1

Description: If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025)

Ref Expression
Hypotheses ring2idlqus1.t ⊢ · = ( .r ‘ 𝑅 )
ring2idlqus1.1 ⊢ 1 = ( 1r ‘ ( 𝑅 ↾s 𝐼 ) )
ring2idlqus1.m ⊢ − = ( -g ‘ 𝑅 )
ring2idlqus1.a ⊢ + = ( +g ‘ 𝑅 )
Assertion ring2idlqus1 ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑈 − ( 1 · 𝑈 ) ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 ring2idlqus1.t ⊢ · = ( .r ‘ 𝑅 )
2 ring2idlqus1.1 ⊢ 1 = ( 1r ‘ ( 𝑅 ↾s 𝐼 ) )
3 ring2idlqus1.m ⊢ − = ( -g ‘ 𝑅 )
4 ring2idlqus1.a ⊢ + = ( +g ‘ 𝑅 )
5 simpr ⊢ ( ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) → ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring )
6 5 adantl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) → ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring )
7 6 ancli ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) → ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) )
8 7 3adant3 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) )
9 simpl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝑅 ∈ Rng )
10 9 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) → 𝑅 ∈ Rng )
11 simpr ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
12 11 adantr ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
13 eqid ⊢ ( 𝑅 ↾s 𝐼 ) = ( 𝑅 ↾s 𝐼 )
14 simpl ⊢ ( ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) → ( 𝑅 ↾s 𝐼 ) ∈ Ring )
15 14 adantl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) → ( 𝑅 ↾s 𝐼 ) ∈ Ring )
16 eqid ⊢ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
17 10 12 13 15 16 rngringbdlem2 ⊢ ( ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ) ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) → 𝑅 ∈ Ring )
18 8 17 syl ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → 𝑅 ∈ Ring )
19 9 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → 𝑅 ∈ Rng )
20 11 3ad2ant1 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
21 simp2l ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → ( 𝑅 ↾s 𝐼 ) ∈ Ring )
22 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23 eqid ⊢ ( 𝑅 ~QG 𝐼 ) = ( 𝑅 ~QG 𝐼 )
24 6 3adant3 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring )
25 simp3 ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) )
26 eqid ⊢ ( ( 𝑈 − ( 1 · 𝑈 ) ) + 1 ) = ( ( 𝑈 − ( 1 · 𝑈 ) ) + 1 )
27 19 20 13 21 22 1 2 23 16 24 25 3 4 26 rngqiprngu ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → ( 1r ‘ 𝑅 ) = ( ( 𝑈 − ( 1 · 𝑈 ) ) + 1 ) )
28 18 27 jca ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ) ∧ ( ( 𝑅 ↾s 𝐼 ) ∈ Ring ∧ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ∈ Ring ) ∧ 𝑈 ∈ ( 1r ‘ ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) ) ) ) → ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) = ( ( 𝑈 − ( 1 · 𝑈 ) ) + 1 ) ) )