Theorem rhmzrhval

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

	Ref	Expression
Hypotheses	rhmzrhval.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
	rhmzrhval.2	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
	rhmzrhval.3	⊢ 𝑀 = ( ℤRHom ‘ 𝑅 )
	rhmzrhval.4	⊢ 𝑁 = ( ℤRHom ‘ 𝑆 )
Assertion	rhmzrhval	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmzrhval.1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
2		rhmzrhval.2	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
3		rhmzrhval.3	⊢ 𝑀 = ( ℤRHom ‘ 𝑅 )
4		rhmzrhval.4	⊢ 𝑁 = ( ℤRHom ‘ 𝑆 )
5		rhmrcl1	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
6	1 5	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
8		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
9	3 7 8	zrhval2	⊢ ( 𝑅 ∈ Ring → 𝑀 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
10	6 9	syl	⊢ ( 𝜑 → 𝑀 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
11	10	fveq1d	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) = ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) )
12	11	fveq2d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) ) )
13		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
14		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
16		ovexd	⊢ ( 𝜑 → ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ∈ V )
17	13 15 2 16	fvmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) = ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
18	17	fveq2d	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
19		rhmghm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
20	1 19	syl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
21		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
22	21 8	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
23	6 22	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
24		eqid	⊢ ( .g ‘ 𝑆 ) = ( .g ‘ 𝑆 )
25	21 7 24	ghmmulg	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑋 ∈ ℤ ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) )
26	20 2 23 25	syl3anc	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) )
27		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
28	8 27	rhm1	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
29	1 28	syl	⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
30	29	oveq2d	⊢ ( 𝜑 → ( 𝑋 ( .g ‘ 𝑆 ) ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
31	26 30	eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
32	18 31	eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
33		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) )
34		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
35	34	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
36		ovexd	⊢ ( 𝜑 → ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ∈ V )
37	33 35 2 36	fvmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) ‘ 𝑋 ) = ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
38	37	eqcomd	⊢ ( 𝜑 → ( 𝑋 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) ‘ 𝑋 ) )
39	32 38	eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) ) = ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) ‘ 𝑋 ) )
40	12 39	eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) = ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) ‘ 𝑋 ) )
41		rhmrcl2	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
42	1 41	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
43	4 24 27	zrhval2	⊢ ( 𝑆 ∈ Ring → 𝑁 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) )
44	43	fveq1d	⊢ ( 𝑆 ∈ Ring → ( 𝑁 ‘ 𝑋 ) = ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) ‘ 𝑋 ) )
45	42 44	syl	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) = ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) ‘ 𝑋 ) )
46	45	eqcomd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) ) ‘ 𝑋 ) = ( 𝑁 ‘ 𝑋 ) )
47	40 46	eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝑁 ‘ 𝑋 ) )