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 = ( Base ` R )
	zrhker.1	|- L = ( ZRHom ` R )
	zrhker.2	|- .0. = ( 0g ` R )
Assertion	zrhker	|- ( R e. Ring -> ( ( chr ` R ) = 0 <-> ( `' L " { .0. } ) = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	|- B = ( Base ` R )
2		zrhker.1	|- L = ( ZRHom ` R )
3		zrhker.2	|- .0. = ( 0g ` R )
4	1 2 3	zrhchr	|- ( R e. Ring -> ( ( chr ` R ) = 0 <-> L : ZZ -1-1-> B ) )
5	1 2 3	zrhf1ker	|- ( R e. Ring -> ( L : ZZ -1-1-> B <-> ( `' L " { .0. } ) = { 0 } ) )
6	4 5	bitrd	|- ( R e. Ring -> ( ( chr ` R ) = 0 <-> ( `' L " { .0. } ) = { 0 } ) )