Metamath Proof Explorer

Theorem rngqiprngu

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 rngqiprngfu.r 
|- ( ph -> R e. Rng )
rngqiprngfu.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rngqiprngfu.j 
|- J = ( R |`s I )
rngqiprngfu.u 
|- ( ph -> J e. Ring )
rngqiprngfu.b 
|- B = ( Base ` R )
rngqiprngfu.t 
|- .x. = ( .r ` R )
rngqiprngfu.1 
|- .1. = ( 1r ` J )
rngqiprngfu.g 
|- .~ = ( R ~QG I )
rngqiprngfu.q 
|- Q = ( R /s .~ )
rngqiprngfu.v 
|- ( ph -> Q e. Ring )
rngqiprngfu.e 
|- ( ph -> E e. ( 1r ` Q ) )
rngqiprngfu.m 
|- .- = ( -g ` R )
rngqiprngfu.a 
|- .+ = ( +g ` R )
rngqiprngfu.n 
|- U = ( ( E .- ( .1. .x. E ) ) .+ .1. )
Assertion rngqiprngu 
|- ( ph -> ( 1r ` R ) = U )

Proof

Step Hyp Ref Expression
1 rngqiprngfu.r 
 |-  ( ph -> R e. Rng )
2 rngqiprngfu.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rngqiprngfu.j 
 |-  J = ( R |`s I )
4 rngqiprngfu.u 
 |-  ( ph -> J e. Ring )
5 rngqiprngfu.b 
 |-  B = ( Base ` R )
6 rngqiprngfu.t 
 |-  .x. = ( .r ` R )
7 rngqiprngfu.1 
 |-  .1. = ( 1r ` J )
8 rngqiprngfu.g 
 |-  .~ = ( R ~QG I )
9 rngqiprngfu.q 
 |-  Q = ( R /s .~ )
10 rngqiprngfu.v 
 |-  ( ph -> Q e. Ring )
11 rngqiprngfu.e 
 |-  ( ph -> E e. ( 1r ` Q ) )
12 rngqiprngfu.m 
 |-  .- = ( -g ` R )
13 rngqiprngfu.a 
 |-  .+ = ( +g ` R )
14 rngqiprngfu.n 
 |-  U = ( ( E .- ( .1. .x. E ) ) .+ .1. )
15 eqid 
 |-  ( Q Xs. J ) = ( Q Xs. J )
16 15 10 4 xpsringd 
 |-  ( ph -> ( Q Xs. J ) e. Ring )
17 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
18 eqid 
 |-  ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
19 1 2 3 4 5 6 7 8 9 17 15 18 rngqiprngim 
 |-  ( ph -> ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) e. ( R RngIso ( Q Xs. J ) ) )
20 rngimcnv 
 |-  ( ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) e. ( R RngIso ( Q Xs. J ) ) -> `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) e. ( ( Q Xs. J ) RngIso R ) )
21 19 20 syl 
 |-  ( ph -> `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) e. ( ( Q Xs. J ) RngIso R ) )
22 rngisomring1 
 |-  ( ( ( Q Xs. J ) e. Ring /\ R e. Rng /\ `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) e. ( ( Q Xs. J ) RngIso R ) ) -> ( 1r ` R ) = ( `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` ( 1r ` ( Q Xs. J ) ) ) )
23 16 1 21 22 syl3anc 
 |-  ( ph -> ( 1r ` R ) = ( `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` ( 1r ` ( Q Xs. J ) ) ) )
24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 18 rngqiprngfu 
 |-  ( ph -> ( ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` U ) = <. [ E ] .~ , .1. >. )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 rngqipring1 
 |-  ( ph -> ( 1r ` ( Q Xs. J ) ) = <. [ E ] .~ , .1. >. )
26 24 25 eqtr4d 
 |-  ( ph -> ( ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` U ) = ( 1r ` ( Q Xs. J ) ) )
27 eqid 
 |-  ( Base ` ( Q Xs. J ) ) = ( Base ` ( Q Xs. J ) )
28 5 27 rngimf1o 
 |-  ( ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) e. ( R RngIso ( Q Xs. J ) ) -> ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) : B -1-1-onto-> ( Base ` ( Q Xs. J ) ) )
29 19 28 syl 
 |-  ( ph -> ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) : B -1-1-onto-> ( Base ` ( Q Xs. J ) ) )
30 1 2 3 4 5 6 7 8 9 10 11 12 13 14 rngqiprngfulem3 
 |-  ( ph -> U e. B )
31 eqid 
 |-  ( 1r ` ( Q Xs. J ) ) = ( 1r ` ( Q Xs. J ) )
32 27 31 ringidcl 
 |-  ( ( Q Xs. J ) e. Ring -> ( 1r ` ( Q Xs. J ) ) e. ( Base ` ( Q Xs. J ) ) )
33 16 32 syl 
 |-  ( ph -> ( 1r ` ( Q Xs. J ) ) e. ( Base ` ( Q Xs. J ) ) )
34 f1ocnvfvb 
 |-  ( ( ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) : B -1-1-onto-> ( Base ` ( Q Xs. J ) ) /\ U e. B /\ ( 1r ` ( Q Xs. J ) ) e. ( Base ` ( Q Xs. J ) ) ) -> ( ( ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` U ) = ( 1r ` ( Q Xs. J ) ) <-> ( `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` ( 1r ` ( Q Xs. J ) ) ) = U ) )
35 29 30 33 34 syl3anc 
 |-  ( ph -> ( ( ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` U ) = ( 1r ` ( Q Xs. J ) ) <-> ( `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` ( 1r ` ( Q Xs. J ) ) ) = U ) )
36 26 35 mpbid 
 |-  ( ph -> ( `' ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. ) ` ( 1r ` ( Q Xs. J ) ) ) = U )
37 23 36 eqtrd 
 |-  ( ph -> ( 1r ` R ) = U )