This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znchr

Description: Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypothesis znchr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion znchr ( 𝑁 ∈ ℕ0 → ( chr ‘ 𝑌 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 znchr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 1 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
3 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
4 2 3 syl ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ Ring )
5 nn0z ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
6 eqid ⊢ ( chr ‘ 𝑌 ) = ( chr ‘ 𝑌 )
7 eqid ⊢ ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
8 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
9 6 7 8 chrdvds ⊢ ( ( 𝑌 ∈ Ring ∧ 𝑥 ∈ ℤ ) → ( ( chr ‘ 𝑌 ) ∥ 𝑥 ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ) )
10 4 5 9 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℕ0 ) → ( ( chr ‘ 𝑌 ) ∥ 𝑥 ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ) )
11 1 7 8 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑥 ) )
12 5 11 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℕ0 ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ 𝑥 ) )
13 10 12 bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℕ0 ) → ( ( chr ‘ 𝑌 ) ∥ 𝑥 ↔ 𝑁 ∥ 𝑥 ) )
14 13 ralrimiva ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑥 ∈ ℕ0 ( ( chr ‘ 𝑌 ) ∥ 𝑥 ↔ 𝑁 ∥ 𝑥 ) )
15 6 chrcl ⊢ ( 𝑌 ∈ Ring → ( chr ‘ 𝑌 ) ∈ ℕ0 )
16 4 15 syl ⊢ ( 𝑁 ∈ ℕ0 → ( chr ‘ 𝑌 ) ∈ ℕ0 )
17 dvdsext ⊢ ( ( ( chr ‘ 𝑌 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( chr ‘ 𝑌 ) = 𝑁 ↔ ∀ 𝑥 ∈ ℕ0 ( ( chr ‘ 𝑌 ) ∥ 𝑥 ↔ 𝑁 ∥ 𝑥 ) ) )
18 16 17 mpancom ⊢ ( 𝑁 ∈ ℕ0 → ( ( chr ‘ 𝑌 ) = 𝑁 ↔ ∀ 𝑥 ∈ ℕ0 ( ( chr ‘ 𝑌 ) ∥ 𝑥 ↔ 𝑁 ∥ 𝑥 ) ) )
19 14 18 mpbird ⊢ ( 𝑁 ∈ ℕ0 → ( chr ‘ 𝑌 ) = 𝑁 )