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 
|- ( ph -> R e. Rng )
rngringbd.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rngringbd.j 
|- J = ( R |`s I )
rngringbd.u 
|- ( ph -> J e. Ring )
rngringbd.q 
|- Q = ( R /s ( R ~QG I ) )
Assertion rngringbdlem2 
|- ( ( ph /\ Q e. Ring ) -> R e. Ring )

Proof

Step Hyp Ref Expression
1 rngringbd.r 
 |-  ( ph -> R e. Rng )
2 rngringbd.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rngringbd.j 
 |-  J = ( R |`s I )
4 rngringbd.u 
 |-  ( ph -> J e. Ring )
5 rngringbd.q 
 |-  Q = ( R /s ( R ~QG I ) )
6 eqid 
 |-  ( Q Xs. J ) = ( Q Xs. J )
7 simpr 
 |-  ( ( ph /\ Q e. Ring ) -> Q e. Ring )
8 4 adantr 
 |-  ( ( ph /\ Q e. Ring ) -> J e. Ring )
9 6 7 8 xpsringd 
 |-  ( ( ph /\ Q e. Ring ) -> ( Q Xs. J ) e. Ring )
10 1 adantr 
 |-  ( ( ph /\ Q e. Ring ) -> R e. Rng )
11 2 adantr 
 |-  ( ( ph /\ Q e. Ring ) -> I e. ( 2Ideal ` R ) )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( .r ` R ) = ( .r ` R )
14 eqid 
 |-  ( 1r ` J ) = ( 1r ` J )
15 eqid 
 |-  ( R ~QG I ) = ( R ~QG I )
16 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
17 eqid 
 |-  ( x e. ( Base ` R ) |-> <. [ x ] ( R ~QG I ) , ( ( 1r ` J ) ( .r ` R ) x ) >. ) = ( x e. ( Base ` R ) |-> <. [ x ] ( R ~QG I ) , ( ( 1r ` J ) ( .r ` R ) x ) >. )
18 10 11 3 8 12 13 14 15 5 16 6 17 rngqiprngim 
 |-  ( ( ph /\ Q e. Ring ) -> ( x e. ( Base ` R ) |-> <. [ x ] ( R ~QG I ) , ( ( 1r ` J ) ( .r ` R ) x ) >. ) e. ( R RngIso ( Q Xs. J ) ) )
19 rngimcnv 
 |-  ( ( x e. ( Base ` R ) |-> <. [ x ] ( R ~QG I ) , ( ( 1r ` J ) ( .r ` R ) x ) >. ) e. ( R RngIso ( Q Xs. J ) ) -> `' ( x e. ( Base ` R ) |-> <. [ x ] ( R ~QG I ) , ( ( 1r ` J ) ( .r ` R ) x ) >. ) e. ( ( Q Xs. J ) RngIso R ) )
20 18 19 syl 
 |-  ( ( ph /\ Q e. Ring ) -> `' ( x e. ( Base ` R ) |-> <. [ x ] ( R ~QG I ) , ( ( 1r ` J ) ( .r ` R ) x ) >. ) e. ( ( Q Xs. J ) RngIso R ) )
21 rngisomring 
 |-  ( ( ( Q Xs. J ) e. Ring /\ R e. Rng /\ `' ( x e. ( Base ` R ) |-> <. [ x ] ( R ~QG I ) , ( ( 1r ` J ) ( .r ` R ) x ) >. ) e. ( ( Q Xs. J ) RngIso R ) ) -> R e. Ring )
22 9 10 20 21 syl3anc 
 |-  ( ( ph /\ Q e. Ring ) -> R e. Ring )