zrhmulg

Description: Value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	zrhval.l	$⊢ L = ℤRHom (R)$
	zrhval2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	zrhval2.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	zrhmulg	$⊢ (R \in Ring \land N \in ℤ) \to L (N) = N \underset{˙}{\cdot} \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		zrhval.l	$⊢ L = ℤRHom (R)$
2		zrhval2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		zrhval2.1	$⊢ \underset{˙}{1} = 1_{R}$
4	1 2 3	zrhval2	$⊢ R \in Ring \to L = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
5	4	fveq1d	$⊢ R \in Ring \to L (N) = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1}) (N)$
6		oveq1	$⊢ n = N \to n \underset{˙}{\cdot} \underset{˙}{1} = N \underset{˙}{\cdot} \underset{˙}{1}$
7		eqid	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1}) = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
8		ovex	$⊢ N \underset{˙}{\cdot} \underset{˙}{1} \in V$
9	6 7 8	fvmpt	$⊢ N \in ℤ \to (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1}) (N) = N \underset{˙}{\cdot} \underset{˙}{1}$
10	5 9	sylan9eq	$⊢ (R \in Ring \land N \in ℤ) \to L (N) = N \underset{˙}{\cdot} \underset{˙}{1}$

Metamath Proof Explorer