Metamath Proof Explorer

Theorem rhmzrhval

Description: Evaluation of integers across a ring homomorphism. (Contributed by metakunt, 4-Jun-2025)

Ref Expression
Hypotheses rhmzrhval.1 
|- ( ph -> F e. ( R RingHom S ) )
rhmzrhval.2 
|- ( ph -> X e. ZZ )
rhmzrhval.3 
|- M = ( ZRHom ` R )
rhmzrhval.4 
|- N = ( ZRHom ` S )
Assertion rhmzrhval 
|- ( ph -> ( F ` ( M ` X ) ) = ( N ` X ) )

Proof

Step Hyp Ref Expression
1 rhmzrhval.1 
 |-  ( ph -> F e. ( R RingHom S ) )
2 rhmzrhval.2 
 |-  ( ph -> X e. ZZ )
3 rhmzrhval.3 
 |-  M = ( ZRHom ` R )
4 rhmzrhval.4 
 |-  N = ( ZRHom ` S )
5 rhmrcl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
6 1 5 syl 
 |-  ( ph -> R e. Ring )
7 eqid 
 |-  ( .g ` R ) = ( .g ` R )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 3 7 8 zrhval2 
 |-  ( R e. Ring -> M = ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) )
10 6 9 syl 
 |-  ( ph -> M = ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) )
11 10 fveq1d 
 |-  ( ph -> ( M ` X ) = ( ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) ` X ) )
12 11 fveq2d 
 |-  ( ph -> ( F ` ( M ` X ) ) = ( F ` ( ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) ` X ) ) )
13 eqidd 
 |-  ( ph -> ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) = ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) )
14 oveq1 
 |-  ( x = X -> ( x ( .g ` R ) ( 1r ` R ) ) = ( X ( .g ` R ) ( 1r ` R ) ) )
15 14 adantl 
 |-  ( ( ph /\ x = X ) -> ( x ( .g ` R ) ( 1r ` R ) ) = ( X ( .g ` R ) ( 1r ` R ) ) )
16 ovexd 
 |-  ( ph -> ( X ( .g ` R ) ( 1r ` R ) ) e. _V )
17 13 15 2 16 fvmptd 
 |-  ( ph -> ( ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) ` X ) = ( X ( .g ` R ) ( 1r ` R ) ) )
18 17 fveq2d 
 |-  ( ph -> ( F ` ( ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) ` X ) ) = ( F ` ( X ( .g ` R ) ( 1r ` R ) ) ) )
19 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
20 1 19 syl 
 |-  ( ph -> F e. ( R GrpHom S ) )
21 eqid 
 |-  ( Base ` R ) = ( Base ` R )
22 21 8 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
23 6 22 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
24 eqid 
 |-  ( .g ` S ) = ( .g ` S )
25 21 7 24 ghmmulg 
 |-  ( ( F e. ( R GrpHom S ) /\ X e. ZZ /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( F ` ( X ( .g ` R ) ( 1r ` R ) ) ) = ( X ( .g ` S ) ( F ` ( 1r ` R ) ) ) )
26 20 2 23 25 syl3anc 
 |-  ( ph -> ( F ` ( X ( .g ` R ) ( 1r ` R ) ) ) = ( X ( .g ` S ) ( F ` ( 1r ` R ) ) ) )
27 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
28 8 27 rhm1 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
29 1 28 syl 
 |-  ( ph -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
30 29 oveq2d 
 |-  ( ph -> ( X ( .g ` S ) ( F ` ( 1r ` R ) ) ) = ( X ( .g ` S ) ( 1r ` S ) ) )
31 26 30 eqtrd 
 |-  ( ph -> ( F ` ( X ( .g ` R ) ( 1r ` R ) ) ) = ( X ( .g ` S ) ( 1r ` S ) ) )
32 18 31 eqtrd 
 |-  ( ph -> ( F ` ( ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) ` X ) ) = ( X ( .g ` S ) ( 1r ` S ) ) )
33 eqidd 
 |-  ( ph -> ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) = ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) )
34 oveq1 
 |-  ( x = X -> ( x ( .g ` S ) ( 1r ` S ) ) = ( X ( .g ` S ) ( 1r ` S ) ) )
35 34 adantl 
 |-  ( ( ph /\ x = X ) -> ( x ( .g ` S ) ( 1r ` S ) ) = ( X ( .g ` S ) ( 1r ` S ) ) )
36 ovexd 
 |-  ( ph -> ( X ( .g ` S ) ( 1r ` S ) ) e. _V )
37 33 35 2 36 fvmptd 
 |-  ( ph -> ( ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) ` X ) = ( X ( .g ` S ) ( 1r ` S ) ) )
38 37 eqcomd 
 |-  ( ph -> ( X ( .g ` S ) ( 1r ` S ) ) = ( ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) ` X ) )
39 32 38 eqtrd 
 |-  ( ph -> ( F ` ( ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) ` X ) ) = ( ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) ` X ) )
40 12 39 eqtrd 
 |-  ( ph -> ( F ` ( M ` X ) ) = ( ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) ` X ) )
41 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
42 1 41 syl 
 |-  ( ph -> S e. Ring )
43 4 24 27 zrhval2 
 |-  ( S e. Ring -> N = ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) )
44 43 fveq1d 
 |-  ( S e. Ring -> ( N ` X ) = ( ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) ` X ) )
45 42 44 syl 
 |-  ( ph -> ( N ` X ) = ( ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) ` X ) )
46 45 eqcomd 
 |-  ( ph -> ( ( x e. ZZ |-> ( x ( .g ` S ) ( 1r ` S ) ) ) ` X ) = ( N ` X ) )
47 40 46 eqtrd 
 |-  ( ph -> ( F ` ( M ` X ) ) = ( N ` X ) )