zrhcntr

Description: The canonical representation of an integer N in a ring R is in the centralizer of the ring's multiplicative monoid. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	zrhcntr.1	$⊢ M = {mulGrp}_{R}$
	zrhcntr.2	$⊢ C = Cntr (M)$
	zrhcntr.3	$⊢ L = ℤRHom (R)$
	zrhcntr.4	$⊢ φ \to R \in Ring$
	zrhcntr.5	$⊢ φ \to N \in ℤ$
Assertion	zrhcntr	$⊢ φ \to L (N) \in C$

Proof

Step	Hyp	Ref	Expression
1		zrhcntr.1	$⊢ M = {mulGrp}_{R}$
2		zrhcntr.2	$⊢ C = Cntr (M)$
3		zrhcntr.3	$⊢ L = ℤRHom (R)$
4		zrhcntr.4	$⊢ φ \to R \in Ring$
5		zrhcntr.5	$⊢ φ \to N \in ℤ$
6		fveq2	$⊢ m = N \to L (m) = L (N)$
7	6	eleq1d	$⊢ m = N \to (L (m) \in C \leftrightarrow L (N) \in C)$
8		fveq2	$⊢ i = 0 \to L (i) = L (0)$
9	8	eleq1d	$⊢ i = 0 \to (L (i) \in C \leftrightarrow L (0) \in C)$
10		fveq2	$⊢ i = n \to L (i) = L (n)$
11	10	eleq1d	$⊢ i = n \to (L (i) \in C \leftrightarrow L (n) \in C)$
12		fveq2	$⊢ i = n + 1 \to L (i) = L (n + 1)$
13	12	eleq1d	$⊢ i = n + 1 \to (L (i) \in C \leftrightarrow L (n + 1) \in C)$
14		fveq2	$⊢ i = m \to L (i) = L (m)$
15	14	eleq1d	$⊢ i = m \to (L (i) \in C \leftrightarrow L (m) \in C)$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	3 16	zrh0	$⊢ R \in Ring \to L (0) = 0_{R}$
18	4 17	syl	$⊢ φ \to L (0) = 0_{R}$
19		eqid	$⊢ {Base}_{R} = {Base}_{R}$
20	19 16	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
21	4 20	syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
22	18 21	eqeltrd	$⊢ φ \to L (0) \in {Base}_{R}$
23		eqid	$⊢ \cdot_{R} = \cdot_{R}$
24	4	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in Ring$
25		simpr	$⊢ (φ \land x \in {Base}_{R}) \to x \in {Base}_{R}$
26	19 23 16 24 25	ringlzd	$⊢ (φ \land x \in {Base}_{R}) \to 0_{R} \cdot_{R} x = 0_{R}$
27	19 23 16 24 25	ringrzd	$⊢ (φ \land x \in {Base}_{R}) \to x \cdot_{R} 0_{R} = 0_{R}$
28	26 27	eqtr4d	$⊢ (φ \land x \in {Base}_{R}) \to 0_{R} \cdot_{R} x = x \cdot_{R} 0_{R}$
29	18	oveq1d	$⊢ φ \to L (0) \cdot_{R} x = 0_{R} \cdot_{R} x$
30	29	adantr	$⊢ (φ \land x \in {Base}_{R}) \to L (0) \cdot_{R} x = 0_{R} \cdot_{R} x$
31	18	oveq2d	$⊢ φ \to x \cdot_{R} L (0) = x \cdot_{R} 0_{R}$
32	31	adantr	$⊢ (φ \land x \in {Base}_{R}) \to x \cdot_{R} L (0) = x \cdot_{R} 0_{R}$
33	28 30 32	3eqtr4d	$⊢ (φ \land x \in {Base}_{R}) \to L (0) \cdot_{R} x = x \cdot_{R} L (0)$
34	33	ralrimiva	$⊢ φ \to \forall x \in {Base}_{R} L (0) \cdot_{R} x = x \cdot_{R} L (0)$
35	1 19	mgpbas	$⊢ {Base}_{R} = {Base}_{M}$
36	1 23	mgpplusg	$⊢ \cdot_{R} = +_{M}$
37	35 36 2	elcntr	$⊢ L (0) \in C \leftrightarrow (L (0) \in {Base}_{R} \land \forall x \in {Base}_{R} L (0) \cdot_{R} x = x \cdot_{R} L (0))$
38	22 34 37	sylanbrc	$⊢ φ \to L (0) \in C$
39	3	zrhrhm	$⊢ R \in Ring \to L \in (ℤ_{ring} RingHom R)$
40		rhmghm	$⊢ L \in (ℤ_{ring} RingHom R) \to L \in (ℤ_{ring} GrpHom R)$
41	4 39 40	3syl	$⊢ φ \to L \in (ℤ_{ring} GrpHom R)$
42	41	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L \in (ℤ_{ring} GrpHom R)$
43		simplr	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to n \in ℕ_{0}$
44	43	nn0zd	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to n \in ℤ$
45		1zzd	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to 1 \in ℤ$
46		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
47		zringplusg	$⊢ + = +_{ℤ_{ring}}$
48		eqid	$⊢ +_{R} = +_{R}$
49	46 47 48	ghmlin	$⊢ (L \in (ℤ_{ring} GrpHom R) \land n \in ℤ \land 1 \in ℤ) \to L (n + 1) = L (n) +_{R} L (1)$
50	42 44 45 49	syl3anc	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (n + 1) = L (n) +_{R} L (1)$
51		eqid	$⊢ 1_{R} = 1_{R}$
52	3 51	zrh1	$⊢ R \in Ring \to L (1) = 1_{R}$
53	4 52	syl	$⊢ φ \to L (1) = 1_{R}$
54	53	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (1) = 1_{R}$
55	54	oveq2d	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (n) +_{R} L (1) = L (n) +_{R} 1_{R}$
56	50 55	eqtrd	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (n + 1) = L (n) +_{R} 1_{R}$
57	4	ringgrpd	$⊢ φ \to R \in Grp$
58	57	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to R \in Grp$
59	35	cntrss	$⊢ Cntr (M) \subseteq {Base}_{R}$
60	2 59	eqsstri	$⊢ C \subseteq {Base}_{R}$
61	60	a1i	$⊢ (φ \land n \in ℕ_{0}) \to C \subseteq {Base}_{R}$
62	61	sselda	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (n) \in {Base}_{R}$
63	19 51	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
64	4 63	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
65	64	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to 1_{R} \in {Base}_{R}$
66	19 48 58 62 65	grpcld	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (n) +_{R} 1_{R} \in {Base}_{R}$
67	35 36 2	cntri	$⊢ (L (n) \in C \land x \in {Base}_{R}) \to L (n) \cdot_{R} x = x \cdot_{R} L (n)$
68	67	adantll	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to L (n) \cdot_{R} x = x \cdot_{R} L (n)$
69	4	ad3antrrr	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to R \in Ring$
70		simpr	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to x \in {Base}_{R}$
71	19 23 51 69 70	ringlidmd	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to 1_{R} \cdot_{R} x = x$
72	19 23 51 69 70	ringridmd	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to x \cdot_{R} 1_{R} = x$
73	71 72	eqtr4d	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to 1_{R} \cdot_{R} x = x \cdot_{R} 1_{R}$
74	68 73	oveq12d	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to (L (n) \cdot_{R} x) +_{R} (1_{R} \cdot_{R} x) = (x \cdot_{R} L (n)) +_{R} (x \cdot_{R} 1_{R})$
75	62	adantr	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to L (n) \in {Base}_{R}$
76	69 63	syl	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to 1_{R} \in {Base}_{R}$
77	19 48 23 69 75 76 70	ringdird	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to (L (n) +_{R} 1_{R}) \cdot_{R} x = (L (n) \cdot_{R} x) +_{R} (1_{R} \cdot_{R} x)$
78	19 48 23 69 70 75 76	ringdid	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to x \cdot_{R} (L (n) +_{R} 1_{R}) = (x \cdot_{R} L (n)) +_{R} (x \cdot_{R} 1_{R})$
79	74 77 78	3eqtr4d	$⊢ (((φ \land n \in ℕ_{0}) \land L (n) \in C) \land x \in {Base}_{R}) \to (L (n) +_{R} 1_{R}) \cdot_{R} x = x \cdot_{R} (L (n) +_{R} 1_{R})$
80	79	ralrimiva	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to \forall x \in {Base}_{R} (L (n) +_{R} 1_{R}) \cdot_{R} x = x \cdot_{R} (L (n) +_{R} 1_{R})$
81	35 36 2	elcntr	$⊢ L (n) +_{R} 1_{R} \in C \leftrightarrow (L (n) +_{R} 1_{R} \in {Base}_{R} \land \forall x \in {Base}_{R} (L (n) +_{R} 1_{R}) \cdot_{R} x = x \cdot_{R} (L (n) +_{R} 1_{R}))$
82	66 80 81	sylanbrc	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (n) +_{R} 1_{R} \in C$
83	56 82	eqeltrd	$⊢ ((φ \land n \in ℕ_{0}) \land L (n) \in C) \to L (n + 1) \in C$
84	9 11 13 15 38 83	nn0indd	$⊢ (φ \land m \in ℕ_{0}) \to L (m) \in C$
85	84	ralrimiva	$⊢ φ \to \forall m \in ℕ_{0} L (m) \in C$
86	85	adantr	$⊢ (φ \land N \in ℕ_{0}) \to \forall m \in ℕ_{0} L (m) \in C$
87		simpr	$⊢ (φ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
88	7 86 87	rspcdva	$⊢ (φ \land N \in ℕ_{0}) \to L (N) \in C$
89	46 19	rhmf	$⊢ L \in (ℤ_{ring} RingHom R) \to L : ℤ ⟶ {Base}_{R}$
90	4 39 89	3syl	$⊢ φ \to L : ℤ ⟶ {Base}_{R}$
91	90	adantr	$⊢ (φ \land - N \in ℕ_{0}) \to L : ℤ ⟶ {Base}_{R}$
92	5	adantr	$⊢ (φ \land - N \in ℕ_{0}) \to N \in ℤ$
93	91 92	ffvelcdmd	$⊢ (φ \land - N \in ℕ_{0}) \to L (N) \in {Base}_{R}$
94		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
95	4	ad2antrr	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to R \in Ring$
96		fveq2	$⊢ m = - N \to L (m) = L (- N)$
97	96	eleq1d	$⊢ m = - N \to (L (m) \in C \leftrightarrow L (- N) \in C)$
98	85	adantr	$⊢ (φ \land - N \in ℕ_{0}) \to \forall m \in ℕ_{0} L (m) \in C$
99		simpr	$⊢ (φ \land - N \in ℕ_{0}) \to - N \in ℕ_{0}$
100	97 98 99	rspcdva	$⊢ (φ \land - N \in ℕ_{0}) \to L (- N) \in C$
101	35 36 2	elcntr	$⊢ L (- N) \in C \leftrightarrow (L (- N) \in {Base}_{R} \land \forall x \in {Base}_{R} L (- N) \cdot_{R} x = x \cdot_{R} L (- N))$
102	100 101	sylib	$⊢ (φ \land - N \in ℕ_{0}) \to (L (- N) \in {Base}_{R} \land \forall x \in {Base}_{R} L (- N) \cdot_{R} x = x \cdot_{R} L (- N))$
103	102	simpld	$⊢ (φ \land - N \in ℕ_{0}) \to L (- N) \in {Base}_{R}$
104	103	adantr	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L (- N) \in {Base}_{R}$
105		simpr	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to x \in {Base}_{R}$
106	19 23 94 95 104 105	ringmneg1	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to {inv}_{g} (R) (L (- N)) \cdot_{R} x = {inv}_{g} (R) (L (- N) \cdot_{R} x)$
107	5	zcnd	$⊢ φ \to N \in ℂ$
108	107	ad2antrr	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to N \in ℂ$
109	108	negnegd	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to - -N = N$
110	5	znegcld	$⊢ φ \to - N \in ℤ$
111		zringinvg	$⊢ - N \in ℤ \to - -N = {inv}_{g} (ℤ_{ring}) (- N)$
112	110 111	syl	$⊢ φ \to - -N = {inv}_{g} (ℤ_{ring}) (- N)$
113	112	ad2antrr	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to - -N = {inv}_{g} (ℤ_{ring}) (- N)$
114	109 113	eqtr3d	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to N = {inv}_{g} (ℤ_{ring}) (- N)$
115	114	fveq2d	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L (N) = L ({inv}_{g} (ℤ_{ring}) (- N))$
116	95 39 40	3syl	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L \in (ℤ_{ring} GrpHom R)$
117	110	ad2antrr	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to - N \in ℤ$
118		eqid	$⊢ {inv}_{g} (ℤ_{ring}) = {inv}_{g} (ℤ_{ring})$
119	46 118 94	ghminv	$⊢ (L \in (ℤ_{ring} GrpHom R) \land - N \in ℤ) \to L ({inv}_{g} (ℤ_{ring}) (- N)) = {inv}_{g} (R) (L (- N))$
120	116 117 119	syl2anc	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L ({inv}_{g} (ℤ_{ring}) (- N)) = {inv}_{g} (R) (L (- N))$
121	115 120	eqtrd	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L (N) = {inv}_{g} (R) (L (- N))$
122	121	oveq1d	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L (N) \cdot_{R} x = {inv}_{g} (R) (L (- N)) \cdot_{R} x$
123	19 23 94 95 105 104	ringmneg2	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to x \cdot_{R} {inv}_{g} (R) (L (- N)) = {inv}_{g} (R) (x \cdot_{R} L (- N))$
124	121	oveq2d	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to x \cdot_{R} L (N) = x \cdot_{R} {inv}_{g} (R) (L (- N))$
125	102	simprd	$⊢ (φ \land - N \in ℕ_{0}) \to \forall x \in {Base}_{R} L (- N) \cdot_{R} x = x \cdot_{R} L (- N)$
126	125	r19.21bi	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L (- N) \cdot_{R} x = x \cdot_{R} L (- N)$
127	126	fveq2d	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to {inv}_{g} (R) (L (- N) \cdot_{R} x) = {inv}_{g} (R) (x \cdot_{R} L (- N))$
128	123 124 127	3eqtr4d	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to x \cdot_{R} L (N) = {inv}_{g} (R) (L (- N) \cdot_{R} x)$
129	106 122 128	3eqtr4d	$⊢ ((φ \land - N \in ℕ_{0}) \land x \in {Base}_{R}) \to L (N) \cdot_{R} x = x \cdot_{R} L (N)$
130	129	ralrimiva	$⊢ (φ \land - N \in ℕ_{0}) \to \forall x \in {Base}_{R} L (N) \cdot_{R} x = x \cdot_{R} L (N)$
131	35 36 2	elcntr	$⊢ L (N) \in C \leftrightarrow (L (N) \in {Base}_{R} \land \forall x \in {Base}_{R} L (N) \cdot_{R} x = x \cdot_{R} L (N))$
132	93 130 131	sylanbrc	$⊢ (φ \land - N \in ℕ_{0}) \to L (N) \in C$
133		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
134	5 133	sylib	$⊢ φ \to (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
135	134	simprd	$⊢ φ \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
136	88 132 135	mpjaodan	$⊢ φ \to L (N) \in C$

Metamath Proof Explorer

Theorem zrhcntr

Proof