Theorem zrhker

Description: The kernel of the homomorphism from the integers to a ring with characteristic 0. (Contributed by Thierry Arnoux, 8-Nov-2017)

	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	zrhker	$$⊢R\in \mathrm{Ring}\to \left(\mathrm{chr}\left(R\right)=0\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	1 2 3	zrhchr	$$⊢R\in \mathrm{Ring}\to \left(\mathrm{chr}\left(R\right)=0\leftrightarrow L:\mathbb{Z}\underset{1-1}{⟶}B\right)$$
5	1 2 3	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)$$
6	4 5	bitrd	$$⊢R\in \mathrm{Ring}\to \left(\mathrm{chr}\left(R\right)=0\leftrightarrow L^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{0\right\}\right)$$