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 = ( ZRHom ` R )
zrhcntr.4 
|- ( ph -> R e. Ring )
zrhcntr.5 
|- ( ph -> N e. ZZ )
Assertion zrhcntr 
|- ( ph -> ( L ` N ) e. C )

Proof

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