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	⊢ ( 𝜑 → 𝑅 ∈ Rng )
	rng2idl1cntr.i	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
	rng2idl1cntr.j	⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
	rng2idl1cntr.u	⊢ ( 𝜑 → 𝐽 ∈ Ring )
	rng2idl1cntr.1	⊢ 1 = ( 1r ‘ 𝐽 )
	rng2idl1cntr.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	rng2idl1cntr	⊢ ( 𝜑 → 1 ∈ ( Cntr ‘ 𝑀 ) )

Proof

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