Theorem zrhmulg

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

	Ref	Expression
Hypotheses	zrhval.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrhval2.m	⊢ · = ( .g ‘ 𝑅 )
	zrhval2.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	zrhmulg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ 𝑁 ) = ( 𝑁 · 1 ) )

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2		zrhval2.m	⊢ · = ( .g ‘ 𝑅 )
3		zrhval2.1	⊢ 1 = ( 1r ‘ 𝑅 )
4	1 2 3	zrhval2	⊢ ( 𝑅 ∈ Ring → 𝐿 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )
5	4	fveq1d	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 𝑁 ) = ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) ‘ 𝑁 ) )
6		oveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 · 1 ) = ( 𝑁 · 1 ) )
7		eqid	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
8		ovex	⊢ ( 𝑁 · 1 ) ∈ V
9	6 7 8	fvmpt	⊢ ( 𝑁 ∈ ℤ → ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) ‘ 𝑁 ) = ( 𝑁 · 1 ) )
10	5 9	sylan9eq	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ 𝑁 ) = ( 𝑁 · 1 ) )