Theorem zrhmulg

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

	Ref	Expression
Hypotheses	zrhval.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	zrhval2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	zrhval2.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	zrhmulg	$$⊢\left(R\in \mathrm{Ring}\wedge N\in \mathbb{Z}\right)\to L\left(N\right)=N\underset{\dot{}}{·}\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
2		zrhval2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		zrhval2.1	$$⊢\underset{\dot{}}{1}=1_R$$
4	1 2 3	zrhval2	$$⊢R\in \mathrm{Ring}\to L=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
5	4	fveq1d	$$⊢R\in \mathrm{Ring}\to L\left(N\right)=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\left(N\right)$$
6		oveq1	$$⊢n=N\to n\underset{\dot{}}{·}\underset{\dot{}}{1}=N\underset{\dot{}}{·}\underset{\dot{}}{1}$$
7		eqid	$$⊢\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
8		ovex	$$⊢N\underset{\dot{}}{·}\underset{\dot{}}{1}\in \mathrm{V}$$
9	6 7 8	fvmpt	$$⊢N\in \mathbb{Z}\to \left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\left(N\right)=N\underset{\dot{}}{·}\underset{\dot{}}{1}$$
10	5 9	sylan9eq	$$⊢\left(R\in \mathrm{Ring}\wedge N\in \mathbb{Z}\right)\to L\left(N\right)=N\underset{\dot{}}{·}\underset{\dot{}}{1}$$