Metamath Proof Explorer

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 ‘ 𝑅 ) ∈ ℙ ) )