Theorem zrh1

Description: Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	zrh1.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	zrh1.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	zrh1	$$⊢R\in \mathrm{Ring}\to L\left(1\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		zrh1.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
2		zrh1.o	$$⊢\underset{\dot{}}{1}=1_R$$
3	1	zrhrhm	$$⊢R\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
4		zring1	$$⊢1=1_{{\mathbb{Z}}_{\mathrm{ring}}}$$
5	4 2	rhm1	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\to L\left(1\right)=\underset{\dot{}}{1}$$
6	3 5	syl	$$⊢R\in \mathrm{Ring}\to L\left(1\right)=\underset{\dot{}}{1}$$