Theorem zrh0

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

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

Proof

Step	Hyp	Ref	Expression
1		zrh0.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
2		zrh0.z	$$⊢\underset{\dot{}}{0}=0_R$$
3	1	zrhrhm	$$⊢R\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
4		rhmghm	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)$$
5		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
6	5 2	ghmid	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)\to L\left(0\right)=\underset{\dot{}}{0}$$
7	3 4 6	3syl	$$⊢R\in \mathrm{Ring}\to L\left(0\right)=\underset{\dot{}}{0}$$