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 ‘ 𝑌 ) = 𝑁 )