Metamath Proof Explorer

Theorem rngqiprngimf1

Description: F is a one-to-one function from (the base set of) a non-unital ring to the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (Contributed by AV, 7-Mar-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 rngqiprngimf1 
|- ( ph -> F : B -1-1-> ( 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 ringrng 
 |-  ( J e. Ring -> J e. Rng )
14 4 13 syl 
 |-  ( ph -> J e. Rng )
15 3 14 eqeltrrid 
 |-  ( ph -> ( R |`s I ) e. Rng )
16 1 2 15 rng2idlnsg 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
17 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
18 16 17 syl 
 |-  ( ph -> I e. ( SubGrp ` R ) )
19 8 oveq2i 
 |-  ( R /s .~ ) = ( R /s ( R ~QG I ) )
20 9 19 eqtri 
 |-  Q = ( R /s ( R ~QG I ) )
21 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
22 20 21 qus2idrng 
 |-  ( ( R e. Rng /\ I e. ( 2Ideal ` R ) /\ I e. ( SubGrp ` R ) ) -> Q e. Rng )
23 1 2 18 22 syl3anc 
 |-  ( ph -> Q e. Rng )
24 rnggrp 
 |-  ( Q e. Rng -> Q e. Grp )
25 24 grpmndd 
 |-  ( Q e. Rng -> Q e. Mnd )
26 23 25 syl 
 |-  ( ph -> Q e. Mnd )
27 ringmnd 
 |-  ( J e. Ring -> J e. Mnd )
28 4 27 syl 
 |-  ( ph -> J e. Mnd )
29 11 xpsmnd0 
 |-  ( ( Q e. Mnd /\ J e. Mnd ) -> ( 0g ` P ) = <. ( 0g ` Q ) , ( 0g ` J ) >. )
30 26 28 29 syl2anc 
 |-  ( ph -> ( 0g ` P ) = <. ( 0g ` Q ) , ( 0g ` J ) >. )
31 30 sneqd 
 |-  ( ph -> { ( 0g ` P ) } = { <. ( 0g ` Q ) , ( 0g ` J ) >. } )
32 31 imaeq2d 
 |-  ( ph -> ( `' F " { ( 0g ` P ) } ) = ( `' F " { <. ( 0g ` Q ) , ( 0g ` J ) >. } ) )
33 nfv 
 |-  F/ x ph
34 opex 
 |-  <. [ x ] .~ , ( .1. .x. x ) >. e. _V
35 34 a1i 
 |-  ( ( ph /\ x e. B ) -> <. [ x ] .~ , ( .1. .x. x ) >. e. _V )
36 33 35 12 fnmptd 
 |-  ( ph -> F Fn B )
37 fncnvima2 
 |-  ( F Fn B -> ( `' F " { <. ( 0g ` Q ) , ( 0g ` J ) >. } ) = { a e. B | ( F ` a ) e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } } )
38 36 37 syl 
 |-  ( ph -> ( `' F " { <. ( 0g ` Q ) , ( 0g ` J ) >. } ) = { a e. B | ( F ` a ) e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } } )
39 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) = <. [ a ] .~ , ( .1. .x. a ) >. )
40 39 eleq1d 
 |-  ( ( ph /\ a e. B ) -> ( ( F ` a ) e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } <-> <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } ) )
41 40 rabbidva 
 |-  ( ph -> { a e. B | ( F ` a ) e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } } = { a e. B | <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } } )
42 eceq1 
 |-  ( a = ( 0g ` R ) -> [ a ] .~ = [ ( 0g ` R ) ] .~ )
43 oveq2 
 |-  ( a = ( 0g ` R ) -> ( .1. .x. a ) = ( .1. .x. ( 0g ` R ) ) )
44 42 43 opeq12d 
 |-  ( a = ( 0g ` R ) -> <. [ a ] .~ , ( .1. .x. a ) >. = <. [ ( 0g ` R ) ] .~ , ( .1. .x. ( 0g ` R ) ) >. )
45 44 eleq1d 
 |-  ( a = ( 0g ` R ) -> ( <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } <-> <. [ ( 0g ` R ) ] .~ , ( .1. .x. ( 0g ` R ) ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } ) )
46 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
47 1 46 syl 
 |-  ( ph -> R e. Grp )
48 47 grpmndd 
 |-  ( ph -> R e. Mnd )
49 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
50 5 49 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. B )
51 48 50 syl 
 |-  ( ph -> ( 0g ` R ) e. B )
52 8 eceq2i 
 |-  [ ( 0g ` R ) ] .~ = [ ( 0g ` R ) ] ( R ~QG I )
53 20 49 qus0 
 |-  ( I e. ( NrmSGrp ` R ) -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
54 16 53 syl 
 |-  ( ph -> [ ( 0g ` R ) ] ( R ~QG I ) = ( 0g ` Q ) )
55 52 54 eqtrid 
 |-  ( ph -> [ ( 0g ` R ) ] .~ = ( 0g ` Q ) )
56 1 2 15 rng2idl0 
 |-  ( ph -> ( 0g ` R ) e. I )
57 5 21 2idlss 
 |-  ( I e. ( 2Ideal ` R ) -> I C_ B )
58 2 57 syl 
 |-  ( ph -> I C_ B )
59 3 5 49 ress0g 
 |-  ( ( R e. Mnd /\ ( 0g ` R ) e. I /\ I C_ B ) -> ( 0g ` R ) = ( 0g ` J ) )
60 48 56 58 59 syl3anc 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` J ) )
61 60 oveq2d 
 |-  ( ph -> ( .1. .x. ( 0g ` R ) ) = ( .1. .x. ( 0g ` J ) ) )
62 3 6 ressmulr 
 |-  ( I e. ( 2Ideal ` R ) -> .x. = ( .r ` J ) )
63 2 62 syl 
 |-  ( ph -> .x. = ( .r ` J ) )
64 63 oveqd 
 |-  ( ph -> ( .1. .x. ( 0g ` J ) ) = ( .1. ( .r ` J ) ( 0g ` J ) ) )
65 eqid 
 |-  ( Base ` J ) = ( Base ` J )
66 65 7 ringidcl 
 |-  ( J e. Ring -> .1. e. ( Base ` J ) )
67 eqid 
 |-  ( .r ` J ) = ( .r ` J )
68 eqid 
 |-  ( 0g ` J ) = ( 0g ` J )
69 65 67 68 ringrz 
 |-  ( ( J e. Ring /\ .1. e. ( Base ` J ) ) -> ( .1. ( .r ` J ) ( 0g ` J ) ) = ( 0g ` J ) )
70 4 66 69 syl2anc2 
 |-  ( ph -> ( .1. ( .r ` J ) ( 0g ` J ) ) = ( 0g ` J ) )
71 61 64 70 3eqtrd 
 |-  ( ph -> ( .1. .x. ( 0g ` R ) ) = ( 0g ` J ) )
72 55 71 opeq12d 
 |-  ( ph -> <. [ ( 0g ` R ) ] .~ , ( .1. .x. ( 0g ` R ) ) >. = <. ( 0g ` Q ) , ( 0g ` J ) >. )
73 opex 
 |-  <. [ ( 0g ` R ) ] .~ , ( .1. .x. ( 0g ` R ) ) >. e. _V
74 73 elsn 
 |-  ( <. [ ( 0g ` R ) ] .~ , ( .1. .x. ( 0g ` R ) ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } <-> <. [ ( 0g ` R ) ] .~ , ( .1. .x. ( 0g ` R ) ) >. = <. ( 0g ` Q ) , ( 0g ` J ) >. )
75 72 74 sylibr 
 |-  ( ph -> <. [ ( 0g ` R ) ] .~ , ( .1. .x. ( 0g ` R ) ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } )
76 opex 
 |-  <. [ a ] .~ , ( .1. .x. a ) >. e. _V
77 76 elsn 
 |-  ( <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } <-> <. [ a ] .~ , ( .1. .x. a ) >. = <. ( 0g ` Q ) , ( 0g ` J ) >. )
78 8 ovexi 
 |-  .~ e. _V
79 ecexg 
 |-  ( .~ e. _V -> [ a ] .~ e. _V )
80 78 79 ax-mp 
 |-  [ a ] .~ e. _V
81 ovex 
 |-  ( .1. .x. a ) e. _V
82 80 81 opth 
 |-  ( <. [ a ] .~ , ( .1. .x. a ) >. = <. ( 0g ` Q ) , ( 0g ` J ) >. <-> ( [ a ] .~ = ( 0g ` Q ) /\ ( .1. .x. a ) = ( 0g ` J ) ) )
83 77 82 bitri 
 |-  ( <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } <-> ( [ a ] .~ = ( 0g ` Q ) /\ ( .1. .x. a ) = ( 0g ` J ) ) )
84 1 2 3 4 5 6 7 8 9 rngqiprngimf1lem 
 |-  ( ( ph /\ a e. B ) -> ( ( [ a ] .~ = ( 0g ` Q ) /\ ( .1. .x. a ) = ( 0g ` J ) ) -> a = ( 0g ` R ) ) )
85 83 84 biimtrid 
 |-  ( ( ph /\ a e. B ) -> ( <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } -> a = ( 0g ` R ) ) )
86 85 imp 
 |-  ( ( ( ph /\ a e. B ) /\ <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } ) -> a = ( 0g ` R ) )
87 45 51 75 86 rabeqsnd 
 |-  ( ph -> { a e. B | <. [ a ] .~ , ( .1. .x. a ) >. e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } } = { ( 0g ` R ) } )
88 41 87 eqtrd 
 |-  ( ph -> { a e. B | ( F ` a ) e. { <. ( 0g ` Q ) , ( 0g ` J ) >. } } = { ( 0g ` R ) } )
89 32 38 88 3eqtrd 
 |-  ( ph -> ( `' F " { ( 0g ` P ) } ) = { ( 0g ` R ) } )
90 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngghm 
 |-  ( ph -> F e. ( R GrpHom P ) )
91 eqid 
 |-  ( Base ` P ) = ( Base ` P )
92 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
93 5 91 49 92 kerf1ghm 
 |-  ( F e. ( R GrpHom P ) -> ( F : B -1-1-> ( Base ` P ) <-> ( `' F " { ( 0g ` P ) } ) = { ( 0g ` R ) } ) )
94 90 93 syl 
 |-  ( ph -> ( F : B -1-1-> ( Base ` P ) <-> ( `' F " { ( 0g ` P ) } ) = { ( 0g ` R ) } ) )
95 89 94 mpbird 
 |-  ( ph -> F : B -1-1-> ( Base ` P ) )
96 eqidd 
 |-  ( ph -> F = F )
97 eqidd 
 |-  ( ph -> B = B )
98 1 2 3 4 5 6 7 8 9 10 11 rngqipbas 
 |-  ( ph -> ( Base ` P ) = ( C X. I ) )
99 96 97 98 f1eq123d 
 |-  ( ph -> ( F : B -1-1-> ( Base ` P ) <-> F : B -1-1-> ( C X. I ) ) )
100 95 99 mpbid 
 |-  ( ph -> F : B -1-1-> ( C X. I ) )