Metamath Proof Explorer

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 = ℤRHom (R)$
		zrhker.2	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	zrhchr	$⊢ R \in Ring \to (chr (R) = 0 \leftrightarrow L : ℤ \underset{1-1}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	$⊢ B = {Base}_{R}$
2		zrhker.1	$⊢ L = ℤRHom (R)$
3		zrhker.2	$⊢ \underset{˙}{0} = 0_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5		eqid	$⊢ 1_{R} = 1_{R}$
6	2 4 5	zrhval2	$⊢ R \in Ring \to L = (x \in ℤ ⟼ x \cdot_{R} 1_{R})$
7		f1eq1	$⊢ L = (x \in ℤ ⟼ x \cdot_{R} 1_{R}) \to (L : ℤ \underset{1-1}{⟶} B \leftrightarrow (x \in ℤ ⟼ x \cdot_{R} 1_{R}) : ℤ \underset{1-1}{⟶} B)$
8	6 7	syl	$⊢ R \in Ring \to (L : ℤ \underset{1-1}{⟶} B \leftrightarrow (x \in ℤ ⟼ x \cdot_{R} 1_{R}) : ℤ \underset{1-1}{⟶} B)$
9		ringgrp	$⊢ R \in Ring \to R \in Grp$
10	1 5	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
11		eqid	$⊢ od (R) = od (R)$
12		eqid	$⊢ (x \in ℤ ⟼ x \cdot_{R} 1_{R}) = (x \in ℤ ⟼ x \cdot_{R} 1_{R})$
13	1 11 4 12	odf1	$⊢ (R \in Grp \land 1_{R} \in B) \to (od (R) (1_{R}) = 0 \leftrightarrow (x \in ℤ ⟼ x \cdot_{R} 1_{R}) : ℤ \underset{1-1}{⟶} B)$
14	9 10 13	syl2anc	$⊢ R \in Ring \to (od (R) (1_{R}) = 0 \leftrightarrow (x \in ℤ ⟼ x \cdot_{R} 1_{R}) : ℤ \underset{1-1}{⟶} B)$
15		eqid	$⊢ chr (R) = chr (R)$
16	11 5 15	chrval	$⊢ od (R) (1_{R}) = chr (R)$
17	16	eqeq1i	$⊢ od (R) (1_{R}) = 0 \leftrightarrow chr (R) = 0$
18	17	a1i	$⊢ R \in Ring \to (od (R) (1_{R}) = 0 \leftrightarrow chr (R) = 0)$
19	8 14 18	3bitr2rd	$⊢ R \in Ring \to (chr (R) = 0 \leftrightarrow L : ℤ \underset{1-1}{⟶} B)$