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	$$⊢\phi \to R\in \mathrm{Rng}$$
	rng2idl1cntr.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
	rng2idl1cntr.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
	rng2idl1cntr.u	$$⊢\phi \to J\in \mathrm{Ring}$$
	rng2idl1cntr.1	$$⊢\underset{\dot{}}{1}=1_J$$
	rng2idl1cntr.m	$$⊢M={\mathrm{mulGrp}}_R$$
Assertion	rng2idl1cntr	$$⊢\phi \to \underset{\dot{}}{1}\in \mathrm{Cntr}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		rng2idl1cntr.r	$$⊢\phi \to R\in \mathrm{Rng}$$
2		rng2idl1cntr.i	$$⊢\phi \to I\in \mathrm{2Ideal}\left(R\right)$$
3		rng2idl1cntr.j	$$⊢J=R{\upharpoonright }_{𝑠}I$$
4		rng2idl1cntr.u	$$⊢\phi \to J\in \mathrm{Ring}$$
5		rng2idl1cntr.1	$$⊢\underset{\dot{}}{1}=1_J$$
6		rng2idl1cntr.m	$$⊢M={\mathrm{mulGrp}}_R$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8	3 7	ressbasss	$$⊢{\mathrm{Base}}_J\subseteq {\mathrm{Base}}_R$$
9		eqid	$$⊢{\mathrm{Base}}_J={\mathrm{Base}}_J$$
10	9 5	ringidcl	$$⊢J\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
11	4 10	syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
12	8 11	sselid	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
13	1	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to R\in \mathrm{Rng}$$
14	12	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
15		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to x\in {\mathrm{Base}}_R$$
16		eqid	$$⊢{\cdot }_R={\cdot }_R$$
17	7 16	rngass	$$⊢\left(R\in \mathrm{Rng}\wedge \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge x\in {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\right)\to \left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_R\left(x{\cdot }_R\underset{\dot{}}{1}\right)$$
18	13 14 15 14 17	syl13anc	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_R\left(x{\cdot }_R\underset{\dot{}}{1}\right)$$
19		eqid	$$⊢{\cdot }_J={\cdot }_J$$
20	4	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to J\in \mathrm{Ring}$$
21	1 2 3 4 7 16 5	rngqiprngghmlem1	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\cdot }_{R}x\in {\mathrm{Base}}_J$$
22	9 19 5 20 21	ringridmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_J\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_{R}x$$
23	3 16	ressmulr	$$⊢I\in \mathrm{2Ideal}\left(R\right)\to {\cdot }_R={\cdot }_J$$
24	2 23	syl	$$⊢\phi \to {\cdot }_R={\cdot }_J$$
25	24	oveqd	$$⊢\phi \to \left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_R\underset{\dot{}}{1}=\left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_J\underset{\dot{}}{1}$$
26	25	eqeq1d	$$⊢\phi \to \left(\left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_{R}x\leftrightarrow \left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_J\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_{R}x\right)$$
27	26	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \left(\left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_{R}x\leftrightarrow \left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_J\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_{R}x\right)$$
28	22 27	mpbird	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \left(\underset{\dot{}}{1}{\cdot }_{R}x\right){\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}{\cdot }_{R}x$$
29	2	2idllidld	$$⊢\phi \to I\in \mathrm{LIdeal}\left(R\right)$$
30		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
31	7 30	lidlss	$$⊢I\in \mathrm{LIdeal}\left(R\right)\to I\subseteq {\mathrm{Base}}_R$$
32	3 7	ressbas2	$$⊢I\subseteq {\mathrm{Base}}_R\to I={\mathrm{Base}}_J$$
33	32	eqcomd	$$⊢I\subseteq {\mathrm{Base}}_R\to {\mathrm{Base}}_J=I$$
34	29 31 33	3syl	$$⊢\phi \to {\mathrm{Base}}_J=I$$
35	34 29	eqeltrd	$$⊢\phi \to {\mathrm{Base}}_J\in \mathrm{LIdeal}\left(R\right)$$
36	2 3 9	2idlbas	$$⊢\phi \to {\mathrm{Base}}_J=I$$
37		ringrng	$$⊢J\in \mathrm{Ring}\to J\in \mathrm{Rng}$$
38	4 37	syl	$$⊢\phi \to J\in \mathrm{Rng}$$
39	3 38	eqeltrrid	$$⊢\phi \to R{\upharpoonright }_{𝑠}I\in \mathrm{Rng}$$
40	1 2 39	rng2idlsubrng	Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |-
41	36 40	eqeltrd	Could not format ( ph -> ( Base ` J ) e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> ( Base ` J ) e. ( SubRng ` R ) ) with typecode |-
42		subrngsubg	Could not format ( ( Base ` J ) e. ( SubRng ` R ) -> ( Base ` J ) e. ( SubGrp ` R ) ) : No typesetting found for |- ( ( Base ` J ) e. ( SubRng ` R ) -> ( Base ` J ) e. ( SubGrp ` R ) ) with typecode |-
43		eqid	$$⊢0_R=0_R$$
44	43	subg0cl	$$⊢{\mathrm{Base}}_J\in \mathrm{SubGrp}\left(R\right)\to 0_R\in {\mathrm{Base}}_J$$
45	41 42 44	3syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_J$$
46	1 35 45	3jca	$$⊢\phi \to \left(R\in \mathrm{Rng}\wedge {\mathrm{Base}}_J\in \mathrm{LIdeal}\left(R\right)\wedge 0_R\in {\mathrm{Base}}_J\right)$$
47	11	anim1ci	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \left(x\in {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_J\right)$$
48	43 7 16 30	rnglidlmcl	$$⊢\left(\left(R\in \mathrm{Rng}\wedge {\mathrm{Base}}_J\in \mathrm{LIdeal}\left(R\right)\wedge 0_R\in {\mathrm{Base}}_J\right)\wedge \left(x\in {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_J\right)\right)\to x{\cdot }_R\underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
49	46 47 48	syl2an2r	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to x{\cdot }_R\underset{\dot{}}{1}\in {\mathrm{Base}}_J$$
50	9 19 5 20 49	ringlidmd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\cdot }_J\left(x{\cdot }_R\underset{\dot{}}{1}\right)=x{\cdot }_R\underset{\dot{}}{1}$$
51	24	oveqd	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_R\left(x{\cdot }_R\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}{\cdot }_J\left(x{\cdot }_R\underset{\dot{}}{1}\right)$$
52	51	eqeq1d	$$⊢\phi \to \left(\underset{\dot{}}{1}{\cdot }_R\left(x{\cdot }_R\underset{\dot{}}{1}\right)=x{\cdot }_R\underset{\dot{}}{1}\leftrightarrow \underset{\dot{}}{1}{\cdot }_J\left(x{\cdot }_R\underset{\dot{}}{1}\right)=x{\cdot }_R\underset{\dot{}}{1}\right)$$
53	52	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \left(\underset{\dot{}}{1}{\cdot }_R\left(x{\cdot }_R\underset{\dot{}}{1}\right)=x{\cdot }_R\underset{\dot{}}{1}\leftrightarrow \underset{\dot{}}{1}{\cdot }_J\left(x{\cdot }_R\underset{\dot{}}{1}\right)=x{\cdot }_R\underset{\dot{}}{1}\right)$$
54	50 53	mpbird	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\cdot }_R\left(x{\cdot }_R\underset{\dot{}}{1}\right)=x{\cdot }_R\underset{\dot{}}{1}$$
55	18 28 54	3eqtr3d	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\cdot }_{R}x=x{\cdot }_R\underset{\dot{}}{1}$$
56	55	ralrimiva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_R\underset{\dot{}}{1}{\cdot }_{R}x=x{\cdot }_R\underset{\dot{}}{1}$$
57		ssidd	$$⊢\phi \to {\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R$$
58	6 7	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_M$$
59	6 16	mgpplusg	$$⊢{\cdot }_R={+}_M$$
60		eqid	$$⊢\mathrm{Cntz}\left(M\right)=\mathrm{Cntz}\left(M\right)$$
61	58 59 60	elcntz	$$⊢{\mathrm{Base}}_R\subseteq {\mathrm{Base}}_R\to \left(\underset{\dot{}}{1}\in \mathrm{Cntz}\left(M\right)\left({\mathrm{Base}}_R\right)\leftrightarrow \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\underset{\dot{}}{1}{\cdot }_{R}x=x{\cdot }_R\underset{\dot{}}{1}\right)\right)$$
62	57 61	syl	$$⊢\phi \to \left(\underset{\dot{}}{1}\in \mathrm{Cntz}\left(M\right)\left({\mathrm{Base}}_R\right)\leftrightarrow \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\underset{\dot{}}{1}{\cdot }_{R}x=x{\cdot }_R\underset{\dot{}}{1}\right)\right)$$
63	12 56 62	mpbir2and	$$⊢\phi \to \underset{\dot{}}{1}\in \mathrm{Cntz}\left(M\right)\left({\mathrm{Base}}_R\right)$$
64	58 60	cntrval	$$⊢\mathrm{Cntz}\left(M\right)\left({\mathrm{Base}}_R\right)=\mathrm{Cntr}\left(M\right)$$
65	63 64	eleqtrdi	$$⊢\phi \to \underset{\dot{}}{1}\in \mathrm{Cntr}\left(M\right)$$