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 
|- .x. = ( .r ` R )
ring2idlqus1.1 
|- .1. = ( 1r ` ( R |`s I ) )
ring2idlqus1.m 
|- .- = ( -g ` R )
ring2idlqus1.a 
|- .+ = ( +g ` R )
Assertion ring2idlqus1 
|- ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> ( R e. Ring /\ ( 1r ` R ) = ( ( U .- ( .1. .x. U ) ) .+ .1. ) ) )

Proof

Step Hyp Ref Expression
1 ring2idlqus1.t 
 |-  .x. = ( .r ` R )
2 ring2idlqus1.1 
 |-  .1. = ( 1r ` ( R |`s I ) )
3 ring2idlqus1.m 
 |-  .- = ( -g ` R )
4 ring2idlqus1.a 
 |-  .+ = ( +g ` R )
5 simpr 
 |-  ( ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) -> ( R /s ( R ~QG I ) ) e. Ring )
6 5 adantl 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) -> ( R /s ( R ~QG I ) ) e. Ring )
7 6 ancli 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) -> ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) /\ ( R /s ( R ~QG I ) ) e. Ring ) )
8 7 3adant3 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) /\ ( R /s ( R ~QG I ) ) e. Ring ) )
9 simpl 
 |-  ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) -> R e. Rng )
10 9 adantr 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) -> R e. Rng )
11 simpr 
 |-  ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) -> I e. ( 2Ideal ` R ) )
12 11 adantr 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) -> I e. ( 2Ideal ` R ) )
13 eqid 
 |-  ( R |`s I ) = ( R |`s I )
14 simpl 
 |-  ( ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) -> ( R |`s I ) e. Ring )
15 14 adantl 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) -> ( R |`s I ) e. Ring )
16 eqid 
 |-  ( R /s ( R ~QG I ) ) = ( R /s ( R ~QG I ) )
17 10 12 13 15 16 rngringbdlem2 
 |-  ( ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) ) /\ ( R /s ( R ~QG I ) ) e. Ring ) -> R e. Ring )
18 8 17 syl 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> R e. Ring )
19 9 3ad2ant1 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> R e. Rng )
20 11 3ad2ant1 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> I e. ( 2Ideal ` R ) )
21 simp2l 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> ( R |`s I ) e. Ring )
22 eqid 
 |-  ( Base ` R ) = ( Base ` R )
23 eqid 
 |-  ( R ~QG I ) = ( R ~QG I )
24 6 3adant3 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> ( R /s ( R ~QG I ) ) e. Ring )
25 simp3 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> U e. ( 1r ` ( R /s ( R ~QG I ) ) ) )
26 eqid 
 |-  ( ( U .- ( .1. .x. U ) ) .+ .1. ) = ( ( U .- ( .1. .x. U ) ) .+ .1. )
27 19 20 13 21 22 1 2 23 16 24 25 3 4 26 rngqiprngu 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> ( 1r ` R ) = ( ( U .- ( .1. .x. U ) ) .+ .1. ) )
28 18 27 jca 
 |-  ( ( ( R e. Rng /\ I e. ( 2Ideal ` R ) ) /\ ( ( R |`s I ) e. Ring /\ ( R /s ( R ~QG I ) ) e. Ring ) /\ U e. ( 1r ` ( R /s ( R ~QG I ) ) ) ) -> ( R e. Ring /\ ( 1r ` R ) = ( ( U .- ( .1. .x. U ) ) .+ .1. ) ) )