rhmzrhval

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

	Ref	Expression
Hypotheses	rhmzrhval.1	$⊢ φ \to F \in (R RingHom S)$
	rhmzrhval.2	$⊢ φ \to X \in ℤ$
	rhmzrhval.3	$⊢ M = ℤRHom (R)$
	rhmzrhval.4	$⊢ N = ℤRHom (S)$
Assertion	rhmzrhval	$⊢ φ \to F (M (X)) = N (X)$

Proof

Step	Hyp	Ref	Expression
1		rhmzrhval.1	$⊢ φ \to F \in (R RingHom S)$
2		rhmzrhval.2	$⊢ φ \to X \in ℤ$
3		rhmzrhval.3	$⊢ M = ℤRHom (R)$
4		rhmzrhval.4	$⊢ N = ℤRHom (S)$
5		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
6	1 5	syl	$⊢ φ \to R \in Ring$
7		eqid	$⊢ \cdot_{R} = \cdot_{R}$
8		eqid	$⊢ 1_{R} = 1_{R}$
9	3 7 8	zrhval2	$⊢ R \in Ring \to M = (x \in ℤ ⟼ x \cdot_{R} 1_{R})$
10	6 9	syl	$⊢ φ \to M = (x \in ℤ ⟼ x \cdot_{R} 1_{R})$
11	10	fveq1d	$⊢ φ \to M (X) = (x \in ℤ ⟼ x \cdot_{R} 1_{R}) (X)$
12	11	fveq2d	$⊢ φ \to F (M (X)) = F ((x \in ℤ ⟼ x \cdot_{R} 1_{R}) (X))$
13		eqidd	$⊢ φ \to (x \in ℤ ⟼ x \cdot_{R} 1_{R}) = (x \in ℤ ⟼ x \cdot_{R} 1_{R})$
14		oveq1	$⊢ x = X \to x \cdot_{R} 1_{R} = X \cdot_{R} 1_{R}$
15	14	adantl	$⊢ (φ \land x = X) \to x \cdot_{R} 1_{R} = X \cdot_{R} 1_{R}$
16		ovexd	$⊢ φ \to X \cdot_{R} 1_{R} \in V$
17	13 15 2 16	fvmptd	$⊢ φ \to (x \in ℤ ⟼ x \cdot_{R} 1_{R}) (X) = X \cdot_{R} 1_{R}$
18	17	fveq2d	$⊢ φ \to F ((x \in ℤ ⟼ x \cdot_{R} 1_{R}) (X)) = F (X \cdot_{R} 1_{R})$
19		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
20	1 19	syl	$⊢ φ \to F \in (R GrpHom S)$
21		eqid	$⊢ {Base}_{R} = {Base}_{R}$
22	21 8	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
23	6 22	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
24		eqid	$⊢ \cdot_{S} = \cdot_{S}$
25	21 7 24	ghmmulg	$⊢ (F \in (R GrpHom S) \land X \in ℤ \land 1_{R} \in {Base}_{R}) \to F (X \cdot_{R} 1_{R}) = X \cdot_{S} F (1_{R})$
26	20 2 23 25	syl3anc	$⊢ φ \to F (X \cdot_{R} 1_{R}) = X \cdot_{S} F (1_{R})$
27		eqid	$⊢ 1_{S} = 1_{S}$
28	8 27	rhm1	$⊢ F \in (R RingHom S) \to F (1_{R}) = 1_{S}$
29	1 28	syl	$⊢ φ \to F (1_{R}) = 1_{S}$
30	29	oveq2d	$⊢ φ \to X \cdot_{S} F (1_{R}) = X \cdot_{S} 1_{S}$
31	26 30	eqtrd	$⊢ φ \to F (X \cdot_{R} 1_{R}) = X \cdot_{S} 1_{S}$
32	18 31	eqtrd	$⊢ φ \to F ((x \in ℤ ⟼ x \cdot_{R} 1_{R}) (X)) = X \cdot_{S} 1_{S}$
33		eqidd	$⊢ φ \to (x \in ℤ ⟼ x \cdot_{S} 1_{S}) = (x \in ℤ ⟼ x \cdot_{S} 1_{S})$
34		oveq1	$⊢ x = X \to x \cdot_{S} 1_{S} = X \cdot_{S} 1_{S}$
35	34	adantl	$⊢ (φ \land x = X) \to x \cdot_{S} 1_{S} = X \cdot_{S} 1_{S}$
36		ovexd	$⊢ φ \to X \cdot_{S} 1_{S} \in V$
37	33 35 2 36	fvmptd	$⊢ φ \to (x \in ℤ ⟼ x \cdot_{S} 1_{S}) (X) = X \cdot_{S} 1_{S}$
38	37	eqcomd	$⊢ φ \to X \cdot_{S} 1_{S} = (x \in ℤ ⟼ x \cdot_{S} 1_{S}) (X)$
39	32 38	eqtrd	$⊢ φ \to F ((x \in ℤ ⟼ x \cdot_{R} 1_{R}) (X)) = (x \in ℤ ⟼ x \cdot_{S} 1_{S}) (X)$
40	12 39	eqtrd	$⊢ φ \to F (M (X)) = (x \in ℤ ⟼ x \cdot_{S} 1_{S}) (X)$
41		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
42	1 41	syl	$⊢ φ \to S \in Ring$
43	4 24 27	zrhval2	$⊢ S \in Ring \to N = (x \in ℤ ⟼ x \cdot_{S} 1_{S})$
44	43	fveq1d	$⊢ S \in Ring \to N (X) = (x \in ℤ ⟼ x \cdot_{S} 1_{S}) (X)$
45	42 44	syl	$⊢ φ \to N (X) = (x \in ℤ ⟼ x \cdot_{S} 1_{S}) (X)$
46	45	eqcomd	$⊢ φ \to (x \in ℤ ⟼ x \cdot_{S} 1_{S}) (X) = N (X)$
47	40 46	eqtrd	$⊢ φ \to F (M (X)) = N (X)$

Metamath Proof Explorer

Theorem rhmzrhval

Proof