domnchr

Description: The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015)

		Ref	Expression
	Assertion	domnchr	$⊢ R \in Domn \to (chr (R) = 0 \lor chr (R) \in ℙ)$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$⊢ chr (R) \neq 0 \leftrightarrow \neg chr (R) = 0$
2		domnring	$⊢ R \in Domn \to R \in Ring$
3		eqid	$⊢ chr (R) = chr (R)$
4	3	chrcl	$⊢ R \in Ring \to chr (R) \in ℕ_{0}$
5	2 4	syl	$⊢ R \in Domn \to chr (R) \in ℕ_{0}$
6	5	adantr	$⊢ (R \in Domn \land chr (R) \neq 0) \to chr (R) \in ℕ_{0}$
7		simpr	$⊢ (R \in Domn \land chr (R) \neq 0) \to chr (R) \neq 0$
8		eldifsn	$⊢ chr (R) \in (ℕ_{0} ∖ \{0\}) \leftrightarrow (chr (R) \in ℕ_{0} \land chr (R) \neq 0)$
9	6 7 8	sylanbrc	$⊢ (R \in Domn \land chr (R) \neq 0) \to chr (R) \in (ℕ_{0} ∖ \{0\})$
10		dfn2	$⊢ ℕ = ℕ_{0} ∖ \{0\}$
11	9 10	eleqtrrdi	$⊢ (R \in Domn \land chr (R) \neq 0) \to chr (R) \in ℕ$
12		domnnzr	$⊢ R \in Domn \to R \in NzRing$
13		nzrring	$⊢ R \in NzRing \to R \in Ring$
14		chrnzr	$⊢ R \in Ring \to (R \in NzRing \leftrightarrow chr (R) \neq 1)$
15	13 14	syl	$⊢ R \in NzRing \to (R \in NzRing \leftrightarrow chr (R) \neq 1)$
16	15	ibi	$⊢ R \in NzRing \to chr (R) \neq 1$
17	12 16	syl	$⊢ R \in Domn \to chr (R) \neq 1$
18	17	adantr	$⊢ (R \in Domn \land chr (R) \neq 0) \to chr (R) \neq 1$
19		eluz2b3	$⊢ chr (R) \in ℤ_{\geq 2} \leftrightarrow (chr (R) \in ℕ \land chr (R) \neq 1)$
20	11 18 19	sylanbrc	$⊢ (R \in Domn \land chr (R) \neq 0) \to chr (R) \in ℤ_{\geq 2}$
21	2	ad2antrr	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to R \in Ring$
22		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
23	22	zrhrhm	$⊢ R \in Ring \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
24	21 23	syl	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to ℤRHom (R) \in (ℤ_{ring} RingHom R)$
25		simprl	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to x \in ℤ$
26		simprr	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to y \in ℤ$
27		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
28		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
29		eqid	$⊢ \cdot_{R} = \cdot_{R}$
30	27 28 29	rhmmul	$⊢ (ℤRHom (R) \in (ℤ_{ring} RingHom R) \land x \in ℤ \land y \in ℤ) \to ℤRHom (R) (x y) = ℤRHom (R) (x) \cdot_{R} ℤRHom (R) (y)$
31	24 25 26 30	syl3anc	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to ℤRHom (R) (x y) = ℤRHom (R) (x) \cdot_{R} ℤRHom (R) (y)$
32	31	eqeq1d	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (ℤRHom (R) (x y) = 0_{R} \leftrightarrow ℤRHom (R) (x) \cdot_{R} ℤRHom (R) (y) = 0_{R})$
33		simpll	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to R \in Domn$
34		eqid	$⊢ {Base}_{R} = {Base}_{R}$
35	27 34	rhmf	$⊢ ℤRHom (R) \in (ℤ_{ring} RingHom R) \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
36	24 35	syl	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to ℤRHom (R) : ℤ ⟶ {Base}_{R}$
37	36 25	ffvelcdmd	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to ℤRHom (R) (x) \in {Base}_{R}$
38	36 26	ffvelcdmd	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to ℤRHom (R) (y) \in {Base}_{R}$
39		eqid	$⊢ 0_{R} = 0_{R}$
40	34 29 39	domneq0	$⊢ (R \in Domn \land ℤRHom (R) (x) \in {Base}_{R} \land ℤRHom (R) (y) \in {Base}_{R}) \to (ℤRHom (R) (x) \cdot_{R} ℤRHom (R) (y) = 0_{R} \leftrightarrow (ℤRHom (R) (x) = 0_{R} \lor ℤRHom (R) (y) = 0_{R}))$
41	33 37 38 40	syl3anc	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (ℤRHom (R) (x) \cdot_{R} ℤRHom (R) (y) = 0_{R} \leftrightarrow (ℤRHom (R) (x) = 0_{R} \lor ℤRHom (R) (y) = 0_{R}))$
42	32 41	bitrd	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (ℤRHom (R) (x y) = 0_{R} \leftrightarrow (ℤRHom (R) (x) = 0_{R} \lor ℤRHom (R) (y) = 0_{R}))$
43	42	biimpd	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (ℤRHom (R) (x y) = 0_{R} \to (ℤRHom (R) (x) = 0_{R} \lor ℤRHom (R) (y) = 0_{R}))$
44		zmulcl	$⊢ (x \in ℤ \land y \in ℤ) \to x y \in ℤ$
45	44	adantl	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to x y \in ℤ$
46	3 22 39	chrdvds	$⊢ (R \in Ring \land x y \in ℤ) \to (chr (R) ∥ x y \leftrightarrow ℤRHom (R) (x y) = 0_{R})$
47	21 45 46	syl2anc	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (chr (R) ∥ x y \leftrightarrow ℤRHom (R) (x y) = 0_{R})$
48	3 22 39	chrdvds	$⊢ (R \in Ring \land x \in ℤ) \to (chr (R) ∥ x \leftrightarrow ℤRHom (R) (x) = 0_{R})$
49	21 25 48	syl2anc	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (chr (R) ∥ x \leftrightarrow ℤRHom (R) (x) = 0_{R})$
50	3 22 39	chrdvds	$⊢ (R \in Ring \land y \in ℤ) \to (chr (R) ∥ y \leftrightarrow ℤRHom (R) (y) = 0_{R})$
51	21 26 50	syl2anc	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (chr (R) ∥ y \leftrightarrow ℤRHom (R) (y) = 0_{R})$
52	49 51	orbi12d	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to ((chr (R) ∥ x \lor chr (R) ∥ y) \leftrightarrow (ℤRHom (R) (x) = 0_{R} \lor ℤRHom (R) (y) = 0_{R}))$
53	43 47 52	3imtr4d	$⊢ ((R \in Domn \land chr (R) \neq 0) \land (x \in ℤ \land y \in ℤ)) \to (chr (R) ∥ x y \to (chr (R) ∥ x \lor chr (R) ∥ y))$
54	53	ralrimivva	$⊢ (R \in Domn \land chr (R) \neq 0) \to \forall x \in ℤ \forall y \in ℤ (chr (R) ∥ x y \to (chr (R) ∥ x \lor chr (R) ∥ y))$
55		isprm6	$⊢ chr (R) \in ℙ \leftrightarrow (chr (R) \in ℤ_{\geq 2} \land \forall x \in ℤ \forall y \in ℤ (chr (R) ∥ x y \to (chr (R) ∥ x \lor chr (R) ∥ y)))$
56	20 54 55	sylanbrc	$⊢ (R \in Domn \land chr (R) \neq 0) \to chr (R) \in ℙ$
57	56	ex	$⊢ R \in Domn \to (chr (R) \neq 0 \to chr (R) \in ℙ)$
58	1 57	biimtrrid	$⊢ R \in Domn \to (\neg chr (R) = 0 \to chr (R) \in ℙ)$
59	58	orrd	$⊢ R \in Domn \to (chr (R) = 0 \lor chr (R) \in ℙ)$

Metamath Proof Explorer

Theorem domnchr

Proof