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 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
zrhcntr.2 ⊢ 𝐶 = ( Cntr ‘ 𝑀 )
zrhcntr.3 ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
zrhcntr.4 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
zrhcntr.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion zrhcntr ( 𝜑 → ( 𝐿 ‘ 𝑁 ) ∈ 𝐶 )

Proof

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