Metamath Proof Explorer


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