Theorem zrhf1ker

Description: The kernel of the homomorphism from the integers to a ring, if it is injective. (Contributed by Thierry Arnoux, 26-Oct-2017) (Revised by Thierry Arnoux, 23-May-2023)

	Ref	Expression
Hypotheses	zrhker.0	$$⊢B={\mathrm{Base}}_R$$
	zrhker.1	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	zrhker.2	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	zrhf1ker	$$⊢R\in \mathrm{Ring}\to \left(L:\mathbb{Z}\underset{1-1}{⟶}B\leftrightarrow L^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{0\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	$$⊢B={\mathrm{Base}}_R$$
2		zrhker.1	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
3		zrhker.2	$$⊢\underset{\dot{}}{0}=0_R$$
4	2	zrhrhm	$$⊢R\in \mathrm{Ring}\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)$$
5		rhmghm	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{RingHom}R\right)\to L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)$$
6		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
7		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
8	6 1 7 3	kerf1ghm	$$⊢L\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)\to \left(L:\mathbb{Z}\underset{1-1}{⟶}B\leftrightarrow L^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{0\right\}\right)$$
9	4 5 8	3syl	$$⊢R\in \mathrm{Ring}\to \left(L:\mathbb{Z}\underset{1-1}{⟶}B\leftrightarrow L^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{0\right\}\right)$$