Theorem zrhchr

Description: The kernel of the homomorphism from the integers to a ring is injective if and only if the ring has 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	zrhchr	|- ( R e. Ring -> ( ( chr ` R ) = 0 <-> L : ZZ -1-1-> B ) )

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	|- B = ( Base ` R )
2		zrhker.1	|- L = ( ZRHom ` R )
3		zrhker.2	|- .0. = ( 0g ` R )
4		eqid	|- ( .g ` R ) = ( .g ` R )
5		eqid	|- ( 1r ` R ) = ( 1r ` R )
6	2 4 5	zrhval2	|- ( R e. Ring -> L = ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) )
7		f1eq1	|- ( L = ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) -> ( L : ZZ -1-1-> B <-> ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) : ZZ -1-1-> B ) )
8	6 7	syl	|- ( R e. Ring -> ( L : ZZ -1-1-> B <-> ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) : ZZ -1-1-> B ) )
9		ringgrp	|- ( R e. Ring -> R e. Grp )
10	1 5	ringidcl	|- ( R e. Ring -> ( 1r ` R ) e. B )
11		eqid	|- ( od ` R ) = ( od ` R )
12		eqid	|- ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) = ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) )
13	1 11 4 12	odf1	|- ( ( R e. Grp /\ ( 1r ` R ) e. B ) -> ( ( ( od ` R ) ` ( 1r ` R ) ) = 0 <-> ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) : ZZ -1-1-> B ) )
14	9 10 13	syl2anc	|- ( R e. Ring -> ( ( ( od ` R ) ` ( 1r ` R ) ) = 0 <-> ( x e. ZZ |-> ( x ( .g ` R ) ( 1r ` R ) ) ) : ZZ -1-1-> B ) )
15		eqid	|- ( chr ` R ) = ( chr ` R )
16	11 5 15	chrval	|- ( ( od ` R ) ` ( 1r ` R ) ) = ( chr ` R )
17	16	eqeq1i	|- ( ( ( od ` R ) ` ( 1r ` R ) ) = 0 <-> ( chr ` R ) = 0 )
18	17	a1i	|- ( R e. Ring -> ( ( ( od ` R ) ` ( 1r ` R ) ) = 0 <-> ( chr ` R ) = 0 ) )
19	8 14 18	3bitr2rd	|- ( R e. Ring -> ( ( chr ` R ) = 0 <-> L : ZZ -1-1-> B ) )