Theorem 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	⊢ ( 𝑅 ∈ Domn → ( ( chr ‘ 𝑅 ) = 0 ∨ ( chr ‘ 𝑅 ) ∈ ℙ ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( ( chr ‘ 𝑅 ) ≠ 0 ↔ ¬ ( chr ‘ 𝑅 ) = 0 )
2		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
3		eqid	⊢ ( chr ‘ 𝑅 ) = ( chr ‘ 𝑅 )
4	3	chrcl	⊢ ( 𝑅 ∈ Ring → ( chr ‘ 𝑅 ) ∈ ℕ0 )
5	2 4	syl	⊢ ( 𝑅 ∈ Domn → ( chr ‘ 𝑅 ) ∈ ℕ0 )
6	5	adantr	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ( chr ‘ 𝑅 ) ∈ ℕ0 )
7		simpr	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ( chr ‘ 𝑅 ) ≠ 0 )
8		eldifsn	⊢ ( ( chr ‘ 𝑅 ) ∈ ( ℕ0 ∖ { 0 } ) ↔ ( ( chr ‘ 𝑅 ) ∈ ℕ0 ∧ ( chr ‘ 𝑅 ) ≠ 0 ) )
9	6 7 8	sylanbrc	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ( chr ‘ 𝑅 ) ∈ ( ℕ0 ∖ { 0 } ) )
10		dfn2	⊢ ℕ = ( ℕ0 ∖ { 0 } )
11	9 10	eleqtrrdi	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ( chr ‘ 𝑅 ) ∈ ℕ )
12		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
13		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
14		chrnzr	⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ( chr ‘ 𝑅 ) ≠ 1 ) )
15	13 14	syl	⊢ ( 𝑅 ∈ NzRing → ( 𝑅 ∈ NzRing ↔ ( chr ‘ 𝑅 ) ≠ 1 ) )
16	15	ibi	⊢ ( 𝑅 ∈ NzRing → ( chr ‘ 𝑅 ) ≠ 1 )
17	12 16	syl	⊢ ( 𝑅 ∈ Domn → ( chr ‘ 𝑅 ) ≠ 1 )
18	17	adantr	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ( chr ‘ 𝑅 ) ≠ 1 )
19		eluz2b3	⊢ ( ( chr ‘ 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( chr ‘ 𝑅 ) ∈ ℕ ∧ ( chr ‘ 𝑅 ) ≠ 1 ) )
20	11 18 19	sylanbrc	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ( chr ‘ 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) )
21	2	ad2antrr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑅 ∈ Ring )
22		eqid	⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
23	22	zrhrhm	⊢ ( 𝑅 ∈ Ring → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
24	21 23	syl	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) )
25		simprl	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
26		simprr	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
27		zringbas	⊢ ℤ = ( Base ‘ ℤring )
28		zringmulr	⊢ · = ( .r ‘ ℤring )
29		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
30	27 28 29	rhmmul	⊢ ( ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) ) )
31	24 25 26 30	syl3anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) ) )
32	31	eqeq1d	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) ) = ( 0g ‘ 𝑅 ) ) )
33		simpll	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑅 ∈ Domn )
34		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
35	27 34	rhmf	⊢ ( ( ℤRHom ‘ 𝑅 ) ∈ ( ℤring RingHom 𝑅 ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
36	24 35	syl	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ℤRHom ‘ 𝑅 ) : ℤ ⟶ ( Base ‘ 𝑅 ) )
37	36 25	ffvelcdmd	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
38	36 26	ffvelcdmd	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
39		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
40	34 29 39	domneq0	⊢ ( ( 𝑅 ∈ Domn ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) ) )
41	33 37 38 40	syl3anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) ) )
42	32 41	bitrd	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) ) )
43	42	biimpd	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( 0g ‘ 𝑅 ) → ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) ) )
44		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
45	44	adantl	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
46	3 22 39	chrdvds	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 · 𝑦 ) ∈ ℤ ) → ( ( chr ‘ 𝑅 ) ∥ ( 𝑥 · 𝑦 ) ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( 0g ‘ 𝑅 ) ) )
47	21 45 46	syl2anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( chr ‘ 𝑅 ) ∥ ( 𝑥 · 𝑦 ) ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ ( 𝑥 · 𝑦 ) ) = ( 0g ‘ 𝑅 ) ) )
48	3 22 39	chrdvds	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ℤ ) → ( ( chr ‘ 𝑅 ) ∥ 𝑥 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
49	21 25 48	syl2anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( chr ‘ 𝑅 ) ∥ 𝑥 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ) )
50	3 22 39	chrdvds	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ℤ ) → ( ( chr ‘ 𝑅 ) ∥ 𝑦 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) )
51	21 26 50	syl2anc	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( chr ‘ 𝑅 ) ∥ 𝑦 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) )
52	49 51	orbi12d	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( chr ‘ 𝑅 ) ∥ 𝑥 ∨ ( chr ‘ 𝑅 ) ∥ 𝑦 ) ↔ ( ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) ∨ ( ( ℤRHom ‘ 𝑅 ) ‘ 𝑦 ) = ( 0g ‘ 𝑅 ) ) ) )
53	43 47 52	3imtr4d	⊢ ( ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( chr ‘ 𝑅 ) ∥ ( 𝑥 · 𝑦 ) → ( ( chr ‘ 𝑅 ) ∥ 𝑥 ∨ ( chr ‘ 𝑅 ) ∥ 𝑦 ) ) )
54	53	ralrimivva	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( ( chr ‘ 𝑅 ) ∥ ( 𝑥 · 𝑦 ) → ( ( chr ‘ 𝑅 ) ∥ 𝑥 ∨ ( chr ‘ 𝑅 ) ∥ 𝑦 ) ) )
55		isprm6	⊢ ( ( chr ‘ 𝑅 ) ∈ ℙ ↔ ( ( chr ‘ 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( ( chr ‘ 𝑅 ) ∥ ( 𝑥 · 𝑦 ) → ( ( chr ‘ 𝑅 ) ∥ 𝑥 ∨ ( chr ‘ 𝑅 ) ∥ 𝑦 ) ) ) )
56	20 54 55	sylanbrc	⊢ ( ( 𝑅 ∈ Domn ∧ ( chr ‘ 𝑅 ) ≠ 0 ) → ( chr ‘ 𝑅 ) ∈ ℙ )
57	56	ex	⊢ ( 𝑅 ∈ Domn → ( ( chr ‘ 𝑅 ) ≠ 0 → ( chr ‘ 𝑅 ) ∈ ℙ ) )
58	1 57	biimtrrid	⊢ ( 𝑅 ∈ Domn → ( ¬ ( chr ‘ 𝑅 ) = 0 → ( chr ‘ 𝑅 ) ∈ ℙ ) )
59	58	orrd	⊢ ( 𝑅 ∈ Domn → ( ( chr ‘ 𝑅 ) = 0 ∨ ( chr ‘ 𝑅 ) ∈ ℙ ) )