Metamath Proof Explorer

Theorem rngqiprngimfo

Description: F is a function from (the base set of) a non-unital ring onto 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, 5-Mar-2025) (Proof shortened by AV, 24-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 rngqiprngimfo 
|- ( ph -> F : B -onto-> ( 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 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimf 
 |-  ( ph -> F : B --> ( C X. I ) )
14 elxpi 
 |-  ( b e. ( C X. I ) -> E. p E. q ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) )
15 10 eleq2i 
 |-  ( p e. C <-> p e. ( Base ` Q ) )
16 vex 
 |-  p e. _V
17 8 9 5 quselbas 
 |-  ( ( R e. Rng /\ p e. _V ) -> ( p e. ( Base ` Q ) <-> E. c e. B p = [ c ] .~ ) )
18 1 16 17 sylancl 
 |-  ( ph -> ( p e. ( Base ` Q ) <-> E. c e. B p = [ c ] .~ ) )
19 15 18 bitrid 
 |-  ( ph -> ( p e. C <-> E. c e. B p = [ c ] .~ ) )
20 eqid 
 |-  ( +g ` R ) = ( +g ` R )
21 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
22 1 21 syl 
 |-  ( ph -> R e. Grp )
23 22 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> R e. Grp )
24 simpr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> c e. B )
25 1 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> R e. Rng )
26 1 2 3 4 5 6 7 rngqiprng1elbas 
 |-  ( ph -> .1. e. B )
27 26 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> .1. e. B )
28 5 6 rngcl 
 |-  ( ( R e. Rng /\ .1. e. B /\ c e. B ) -> ( .1. .x. c ) e. B )
29 25 27 24 28 syl3anc 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( .1. .x. c ) e. B )
30 eqid 
 |-  ( -g ` R ) = ( -g ` R )
31 5 30 grpsubcl 
 |-  ( ( R e. Grp /\ c e. B /\ ( .1. .x. c ) e. B ) -> ( c ( -g ` R ) ( .1. .x. c ) ) e. B )
32 23 24 29 31 syl3anc 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( c ( -g ` R ) ( .1. .x. c ) ) e. B )
33 eqid 
 |-  ( 2Ideal ` R ) = ( 2Ideal ` R )
34 5 33 2idlss 
 |-  ( I e. ( 2Ideal ` R ) -> I C_ B )
35 2 34 syl 
 |-  ( ph -> I C_ B )
36 35 sselda 
 |-  ( ( ph /\ q e. I ) -> q e. B )
37 36 adantr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> q e. B )
38 5 20 23 32 37 grpcld 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) e. B )
39 38 adantr 
 |-  ( ( ( ( ph /\ q e. I ) /\ c e. B ) /\ p = [ c ] .~ ) -> ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) e. B )
40 opeq1 
 |-  ( p = [ c ] .~ -> <. p , q >. = <. [ c ] .~ , q >. )
41 40 adantl 
 |-  ( ( ( ( ph /\ q e. I ) /\ c e. B ) /\ p = [ c ] .~ ) -> <. p , q >. = <. [ c ] .~ , q >. )
42 eceq1 
 |-  ( a = ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) -> [ a ] .~ = [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ )
43 oveq2 
 |-  ( a = ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) -> ( .1. .x. a ) = ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) )
44 42 43 opeq12d 
 |-  ( a = ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) -> <. [ a ] .~ , ( .1. .x. a ) >. = <. [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ , ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) >. )
45 41 44 eqeqan12d 
 |-  ( ( ( ( ( ph /\ q e. I ) /\ c e. B ) /\ p = [ c ] .~ ) /\ a = ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) -> ( <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. <-> <. [ c ] .~ , q >. = <. [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ , ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) >. ) )
46 rngabl 
 |-  ( R e. Rng -> R e. Abel )
47 1 46 syl 
 |-  ( ph -> R e. Abel )
48 47 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> R e. Abel )
49 5 20 30 ablsubaddsub 
 |-  ( ( R e. Abel /\ ( c e. B /\ ( .1. .x. c ) e. B /\ q e. B ) ) -> ( ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ( -g ` R ) c ) = ( q ( -g ` R ) ( .1. .x. c ) ) )
50 48 24 29 37 49 syl13anc 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ( -g ` R ) c ) = ( q ( -g ` R ) ( .1. .x. c ) ) )
51 4 ringgrpd 
 |-  ( ph -> J e. Grp )
52 51 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> J e. Grp )
53 eqid 
 |-  ( Base ` J ) = ( Base ` J )
54 2 3 53 2idlbas 
 |-  ( ph -> ( Base ` J ) = I )
55 54 eqcomd 
 |-  ( ph -> I = ( Base ` J ) )
56 55 eleq2d 
 |-  ( ph -> ( q e. I <-> q e. ( Base ` J ) ) )
57 56 biimpa 
 |-  ( ( ph /\ q e. I ) -> q e. ( Base ` J ) )
58 57 adantr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> q e. ( Base ` J ) )
59 1 2 3 4 5 6 7 rngqiprngghmlem1 
 |-  ( ( ph /\ c e. B ) -> ( .1. .x. c ) e. ( Base ` J ) )
60 59 adantlr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( .1. .x. c ) e. ( Base ` J ) )
61 eqid 
 |-  ( -g ` J ) = ( -g ` J )
62 53 61 grpsubcl 
 |-  ( ( J e. Grp /\ q e. ( Base ` J ) /\ ( .1. .x. c ) e. ( Base ` J ) ) -> ( q ( -g ` J ) ( .1. .x. c ) ) e. ( Base ` J ) )
63 52 58 60 62 syl3anc 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( q ( -g ` J ) ( .1. .x. c ) ) e. ( Base ` J ) )
64 ringrng 
 |-  ( J e. Ring -> J e. Rng )
65 4 64 syl 
 |-  ( ph -> J e. Rng )
66 3 65 eqeltrrid 
 |-  ( ph -> ( R |`s I ) e. Rng )
67 1 2 66 rng2idlnsg 
 |-  ( ph -> I e. ( NrmSGrp ` R ) )
68 nsgsubg 
 |-  ( I e. ( NrmSGrp ` R ) -> I e. ( SubGrp ` R ) )
69 67 68 syl 
 |-  ( ph -> I e. ( SubGrp ` R ) )
70 69 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> I e. ( SubGrp ` R ) )
71 simplr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> q e. I )
72 54 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( Base ` J ) = I )
73 60 72 eleqtrd 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( .1. .x. c ) e. I )
74 30 3 61 subgsub 
 |-  ( ( I e. ( SubGrp ` R ) /\ q e. I /\ ( .1. .x. c ) e. I ) -> ( q ( -g ` R ) ( .1. .x. c ) ) = ( q ( -g ` J ) ( .1. .x. c ) ) )
75 70 71 73 74 syl3anc 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( q ( -g ` R ) ( .1. .x. c ) ) = ( q ( -g ` J ) ( .1. .x. c ) ) )
76 55 ad2antrr 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> I = ( Base ` J ) )
77 63 75 76 3eltr4d 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( q ( -g ` R ) ( .1. .x. c ) ) e. I )
78 50 77 eqeltrd 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ( -g ` R ) c ) e. I )
79 5 30 8 qusecsub 
 |-  ( ( ( R e. Abel /\ I e. ( SubGrp ` R ) ) /\ ( c e. B /\ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) e. B ) ) -> ( [ c ] .~ = [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ <-> ( ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ( -g ` R ) c ) e. I ) )
80 48 70 24 38 79 syl22anc 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( [ c ] .~ = [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ <-> ( ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ( -g ` R ) c ) e. I ) )
81 78 80 mpbird 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> [ c ] .~ = [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ )
82 1 2 3 4 5 6 7 rngqiprngimfolem 
 |-  ( ( ph /\ q e. I /\ c e. B ) -> ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) = q )
83 82 3expa 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) = q )
84 83 eqcomd 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> q = ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) )
85 81 84 opeq12d 
 |-  ( ( ( ph /\ q e. I ) /\ c e. B ) -> <. [ c ] .~ , q >. = <. [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ , ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) >. )
86 85 adantr 
 |-  ( ( ( ( ph /\ q e. I ) /\ c e. B ) /\ p = [ c ] .~ ) -> <. [ c ] .~ , q >. = <. [ ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ] .~ , ( .1. .x. ( ( c ( -g ` R ) ( .1. .x. c ) ) ( +g ` R ) q ) ) >. )
87 39 45 86 rspcedvd 
 |-  ( ( ( ( ph /\ q e. I ) /\ c e. B ) /\ p = [ c ] .~ ) -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. )
88 87 rexlimdva2 
 |-  ( ( ph /\ q e. I ) -> ( E. c e. B p = [ c ] .~ -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) )
89 88 ex 
 |-  ( ph -> ( q e. I -> ( E. c e. B p = [ c ] .~ -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) ) )
90 89 com23 
 |-  ( ph -> ( E. c e. B p = [ c ] .~ -> ( q e. I -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) ) )
91 19 90 sylbid 
 |-  ( ph -> ( p e. C -> ( q e. I -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) ) )
92 91 impd 
 |-  ( ph -> ( ( p e. C /\ q e. I ) -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) )
93 92 com12 
 |-  ( ( p e. C /\ q e. I ) -> ( ph -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) )
94 93 adantl 
 |-  ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) -> ( ph -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) )
95 94 imp 
 |-  ( ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) /\ ph ) -> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. )
96 simplll 
 |-  ( ( ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) /\ ph ) /\ a e. B ) -> b = <. p , q >. )
97 1 2 3 4 5 6 7 8 9 10 11 12 rngqiprngimfv 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) = <. [ a ] .~ , ( .1. .x. a ) >. )
98 97 adantll 
 |-  ( ( ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) /\ ph ) /\ a e. B ) -> ( F ` a ) = <. [ a ] .~ , ( .1. .x. a ) >. )
99 96 98 eqeq12d 
 |-  ( ( ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) /\ ph ) /\ a e. B ) -> ( b = ( F ` a ) <-> <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) )
100 99 rexbidva 
 |-  ( ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) /\ ph ) -> ( E. a e. B b = ( F ` a ) <-> E. a e. B <. p , q >. = <. [ a ] .~ , ( .1. .x. a ) >. ) )
101 95 100 mpbird 
 |-  ( ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) /\ ph ) -> E. a e. B b = ( F ` a ) )
102 101 ex 
 |-  ( ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) -> ( ph -> E. a e. B b = ( F ` a ) ) )
103 102 exlimivv 
 |-  ( E. p E. q ( b = <. p , q >. /\ ( p e. C /\ q e. I ) ) -> ( ph -> E. a e. B b = ( F ` a ) ) )
104 14 103 syl 
 |-  ( b e. ( C X. I ) -> ( ph -> E. a e. B b = ( F ` a ) ) )
105 104 impcom 
 |-  ( ( ph /\ b e. ( C X. I ) ) -> E. a e. B b = ( F ` a ) )
106 105 ralrimiva 
 |-  ( ph -> A. b e. ( C X. I ) E. a e. B b = ( F ` a ) )
107 dffo3 
 |-  ( F : B -onto-> ( C X. I ) <-> ( F : B --> ( C X. I ) /\ A. b e. ( C X. I ) E. a e. B b = ( F ` a ) ) )
108 13 106 107 sylanbrc 
 |-  ( ph -> F : B -onto-> ( C X. I ) )