Metamath Proof Explorer

Theorem rngqiprngimf

Description: F is a function from (the base set of) a non-unital ring to the product of the (base set C of the) quotient with a two-sided ideal and the (base set I of the) two-sided ideal (because of 2idlbas , ( BaseJ ) = I !) (Contributed by AV, 21-Feb-2025)

Ref Expression
Hypotheses rng2idlring.r 
|- ( ph -> R e. Rng )
rng2idlring.i 
|- ( ph -> I e. ( 2Ideal ` R ) )
rng2idlring.j 
|- J = ( R |`s I )
rng2idlring.u 
|- ( ph -> J e. Ring )
rng2idlring.b 
|- B = ( Base ` R )
rng2idlring.t 
|- .x. = ( .r ` R )
rng2idlring.1 
|- .1. = ( 1r ` J )
rngqiprngim.g 
|- .~ = ( R ~QG I )
rngqiprngim.q 
|- Q = ( R /s .~ )
rngqiprngim.c 
|- C = ( Base ` Q )
rngqiprngim.p 
|- P = ( Q Xs. J )
rngqiprngim.f 
|- F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
Assertion rngqiprngimf 
|- ( ph -> F : B --> ( C X. I ) )

Proof

Step Hyp Ref Expression
1 rng2idlring.r 
 |-  ( ph -> R e. Rng )
2 rng2idlring.i 
 |-  ( ph -> I e. ( 2Ideal ` R ) )
3 rng2idlring.j 
 |-  J = ( R |`s I )
4 rng2idlring.u 
 |-  ( ph -> J e. Ring )
5 rng2idlring.b 
 |-  B = ( Base ` R )
6 rng2idlring.t 
 |-  .x. = ( .r ` R )
7 rng2idlring.1 
 |-  .1. = ( 1r ` J )
8 rngqiprngim.g 
 |-  .~ = ( R ~QG I )
9 rngqiprngim.q 
 |-  Q = ( R /s .~ )
10 rngqiprngim.c 
 |-  C = ( Base ` Q )
11 rngqiprngim.p 
 |-  P = ( Q Xs. J )
12 rngqiprngim.f 
 |-  F = ( x e. B |-> <. [ x ] .~ , ( .1. .x. x ) >. )
13 8 ovexi 
 |-  .~ e. _V
14 13 ecelqsi 
 |-  ( x e. B -> [ x ] .~ e. ( B /. .~ ) )
15 14 adantl 
 |-  ( ( ph /\ x e. B ) -> [ x ] .~ e. ( B /. .~ ) )
16 9 a1i 
 |-  ( ( ph /\ x e. B ) -> Q = ( R /s .~ ) )
17 5 a1i 
 |-  ( ( ph /\ x e. B ) -> B = ( Base ` R ) )
18 13 a1i 
 |-  ( ( ph /\ x e. B ) -> .~ e. _V )
19 1 adantr 
 |-  ( ( ph /\ x e. B ) -> R e. Rng )
20 16 17 18 19 qusbas 
 |-  ( ( ph /\ x e. B ) -> ( B /. .~ ) = ( Base ` Q ) )
21 20 10 eqtr4di 
 |-  ( ( ph /\ x e. B ) -> ( B /. .~ ) = C )
22 15 21 eleqtrd 
 |-  ( ( ph /\ x e. B ) -> [ x ] .~ e. C )
23 eqid 
 |-  ( Base ` J ) = ( Base ` J )
24 2 3 23 2idlbas 
 |-  ( ph -> ( Base ` J ) = I )
25 2 3 23 2idlelbas 
 |-  ( ph -> ( ( Base ` J ) e. ( LIdeal ` R ) /\ ( Base ` J ) e. ( LIdeal ` ( oppR ` R ) ) ) )
26 25 simprd 
 |-  ( ph -> ( Base ` J ) e. ( LIdeal ` ( oppR ` R ) ) )
27 24 26 eqeltrrd 
 |-  ( ph -> I e. ( LIdeal ` ( oppR ` R ) ) )
28 ringrng 
 |-  ( J e. Ring -> J e. Rng )
29 4 28 syl 
 |-  ( ph -> J e. Rng )
30 3 29 eqeltrrid 
 |-  ( ph -> ( R |`s I ) e. Rng )
31 1 2 30 rng2idl0 
 |-  ( ph -> ( 0g ` R ) e. I )
32 1 27 31 3jca 
 |-  ( ph -> ( R e. Rng /\ I e. ( LIdeal ` ( oppR ` R ) ) /\ ( 0g ` R ) e. I ) )
33 23 7 ringidcl 
 |-  ( J e. Ring -> .1. e. ( Base ` J ) )
34 4 33 syl 
 |-  ( ph -> .1. e. ( Base ` J ) )
35 34 24 eleqtrd 
 |-  ( ph -> .1. e. I )
36 35 anim1ci 
 |-  ( ( ph /\ x e. B ) -> ( x e. B /\ .1. e. I ) )
37 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
38 eqid 
 |-  ( LIdeal ` ( oppR ` R ) ) = ( LIdeal ` ( oppR ` R ) )
39 37 5 6 38 rngridlmcl 
 |-  ( ( ( R e. Rng /\ I e. ( LIdeal ` ( oppR ` R ) ) /\ ( 0g ` R ) e. I ) /\ ( x e. B /\ .1. e. I ) ) -> ( .1. .x. x ) e. I )
40 32 36 39 syl2an2r 
 |-  ( ( ph /\ x e. B ) -> ( .1. .x. x ) e. I )
41 22 40 opelxpd 
 |-  ( ( ph /\ x e. B ) -> <. [ x ] .~ , ( .1. .x. x ) >. e. ( C X. I ) )
42 41 12 fmptd 
 |-  ( ph -> F : B --> ( C X. I ) )