Theorem rng2idl1cntr

Description: The unity of a two-sided ideal of a non-unital ring is central, i.e., an element of the center of the multiplicative semigroup of the non-unital ring. This is part of the proof given in MathOverflow, which seems to be sufficient to show that F given below (see rngqiprngimf ) is an isomorphism. In our proof, however we show that F is linear regarding the multiplication ( rngqiprnglin ) via rngqiprnglinlem1 instead. (Contributed by AV, 13-Feb-2025)

	Ref	Expression
Hypotheses	rng2idl1cntr.r	|- ( ph -> R e. Rng )
	rng2idl1cntr.i	|- ( ph -> I e. ( 2Ideal ` R ) )
	rng2idl1cntr.j	|- J = ( R |`s I )
	rng2idl1cntr.u	|- ( ph -> J e. Ring )
	rng2idl1cntr.1	|- .1. = ( 1r ` J )
	rng2idl1cntr.m	|- M = ( mulGrp ` R )
Assertion	rng2idl1cntr	|- ( ph -> .1. e. ( Cntr ` M ) )

Proof

Step	Hyp	Ref	Expression
1		rng2idl1cntr.r	|- ( ph -> R e. Rng )
2		rng2idl1cntr.i	|- ( ph -> I e. ( 2Ideal ` R ) )
3		rng2idl1cntr.j	|- J = ( R |`s I )
4		rng2idl1cntr.u	|- ( ph -> J e. Ring )
5		rng2idl1cntr.1	|- .1. = ( 1r ` J )
6		rng2idl1cntr.m	|- M = ( mulGrp ` R )
7		eqid	|- ( Base ` R ) = ( Base ` R )
8	3 7	ressbasss	|- ( Base ` J ) C_ ( Base ` R )
9		eqid	|- ( Base ` J ) = ( Base ` J )
10	9 5	ringidcl	|- ( J e. Ring -> .1. e. ( Base ` J ) )
11	4 10	syl	|- ( ph -> .1. e. ( Base ` J ) )
12	8 11	sselid	|- ( ph -> .1. e. ( Base ` R ) )
13	1	adantr	|- ( ( ph /\ x e. ( Base ` R ) ) -> R e. Rng )
14	12	adantr	|- ( ( ph /\ x e. ( Base ` R ) ) -> .1. e. ( Base ` R ) )
15		simpr	|- ( ( ph /\ x e. ( Base ` R ) ) -> x e. ( Base ` R ) )
16		eqid	|- ( .r ` R ) = ( .r ` R )
17	7 16	rngass	|- ( ( R e. Rng /\ ( .1. e. ( Base ` R ) /\ x e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) )
18	13 14 15 14 17	syl13anc	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) )
19		eqid	|- ( .r ` J ) = ( .r ` J )
20	4	adantr	|- ( ( ph /\ x e. ( Base ` R ) ) -> J e. Ring )
21	1 2 3 4 7 16 5	rngqiprngghmlem1	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` R ) x ) e. ( Base ` J ) )
22	9 19 5 20 21	ringridmd	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) = ( .1. ( .r ` R ) x ) )
23	3 16	ressmulr	|- ( I e. ( 2Ideal ` R ) -> ( .r ` R ) = ( .r ` J ) )
24	2 23	syl	|- ( ph -> ( .r ` R ) = ( .r ` J ) )
25	24	oveqd	|- ( ph -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) )
26	25	eqeq1d	|- ( ph -> ( ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) x ) <-> ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) = ( .1. ( .r ` R ) x ) ) )
27	26	adantr	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) x ) <-> ( ( .1. ( .r ` R ) x ) ( .r ` J ) .1. ) = ( .1. ( .r ` R ) x ) ) )
28	22 27	mpbird	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) x ) ( .r ` R ) .1. ) = ( .1. ( .r ` R ) x ) )
29	2	2idllidld	|- ( ph -> I e. ( LIdeal ` R ) )
30		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
31	7 30	lidlss	|- ( I e. ( LIdeal ` R ) -> I C_ ( Base ` R ) )
32	3 7	ressbas2	|- ( I C_ ( Base ` R ) -> I = ( Base ` J ) )
33	32	eqcomd	|- ( I C_ ( Base ` R ) -> ( Base ` J ) = I )
34	29 31 33	3syl	|- ( ph -> ( Base ` J ) = I )
35	34 29	eqeltrd	|- ( ph -> ( Base ` J ) e. ( LIdeal ` R ) )
36	2 3 9	2idlbas	|- ( ph -> ( Base ` J ) = I )
37		ringrng	|- ( J e. Ring -> J e. Rng )
38	4 37	syl	|- ( ph -> J e. Rng )
39	3 38	eqeltrrid	|- ( ph -> ( R |`s I ) e. Rng )
40	1 2 39	rng2idlsubrng	|- ( ph -> I e. ( SubRng ` R ) )
41	36 40	eqeltrd	|- ( ph -> ( Base ` J ) e. ( SubRng ` R ) )
42		subrngsubg	|- ( ( Base ` J ) e. ( SubRng ` R ) -> ( Base ` J ) e. ( SubGrp ` R ) )
43		eqid	|- ( 0g ` R ) = ( 0g ` R )
44	43	subg0cl	|- ( ( Base ` J ) e. ( SubGrp ` R ) -> ( 0g ` R ) e. ( Base ` J ) )
45	41 42 44	3syl	|- ( ph -> ( 0g ` R ) e. ( Base ` J ) )
46	1 35 45	3jca	|- ( ph -> ( R e. Rng /\ ( Base ` J ) e. ( LIdeal ` R ) /\ ( 0g ` R ) e. ( Base ` J ) ) )
47	11	anim1ci	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( x e. ( Base ` R ) /\ .1. e. ( Base ` J ) ) )
48	43 7 16 30	rnglidlmcl	|- ( ( ( R e. Rng /\ ( Base ` J ) e. ( LIdeal ` R ) /\ ( 0g ` R ) e. ( Base ` J ) ) /\ ( x e. ( Base ` R ) /\ .1. e. ( Base ` J ) ) ) -> ( x ( .r ` R ) .1. ) e. ( Base ` J ) )
49	46 47 48	syl2an2r	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) .1. ) e. ( Base ` J ) )
50	9 19 5 20 49	ringlidmd	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) )
51	24	oveqd	|- ( ph -> ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) )
52	51	eqeq1d	|- ( ph -> ( ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) <-> ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) ) )
53	52	adantr	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) <-> ( .1. ( .r ` J ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) ) )
54	50 53	mpbird	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` R ) ( x ( .r ` R ) .1. ) ) = ( x ( .r ` R ) .1. ) )
55	18 28 54	3eqtr3d	|- ( ( ph /\ x e. ( Base ` R ) ) -> ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) )
56	55	ralrimiva	|- ( ph -> A. x e. ( Base ` R ) ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) )
57		ssidd	|- ( ph -> ( Base ` R ) C_ ( Base ` R ) )
58	6 7	mgpbas	|- ( Base ` R ) = ( Base ` M )
59	6 16	mgpplusg	|- ( .r ` R ) = ( +g ` M )
60		eqid	|- ( Cntz ` M ) = ( Cntz ` M )
61	58 59 60	elcntz	|- ( ( Base ` R ) C_ ( Base ` R ) -> ( .1. e. ( ( Cntz ` M ) ` ( Base ` R ) ) <-> ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) ) ) )
62	57 61	syl	|- ( ph -> ( .1. e. ( ( Cntz ` M ) ` ( Base ` R ) ) <-> ( .1. e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( .1. ( .r ` R ) x ) = ( x ( .r ` R ) .1. ) ) ) )
63	12 56 62	mpbir2and	|- ( ph -> .1. e. ( ( Cntz ` M ) ` ( Base ` R ) ) )
64	58 60	cntrval	|- ( ( Cntz ` M ) ` ( Base ` R ) ) = ( Cntr ` M )
65	63 64	eleqtrdi	|- ( ph -> .1. e. ( Cntr ` M ) )