Theorem chrcl

Description: Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypothesis	chrcl.c	⊢ 𝐶 = ( chr ‘ 𝑅 )
Assertion	chrcl	⊢ ( 𝑅 ∈ Ring → 𝐶 ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		chrcl.c	⊢ 𝐶 = ( chr ‘ 𝑅 )
2		eqid	⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
3		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4	2 3 1	chrval	⊢ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 𝐶
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	5 3	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
7	5 2	odcl	⊢ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) → ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ℕ0 )
8	6 7	syl	⊢ ( 𝑅 ∈ Ring → ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ℕ0 )
9	4 8	eqeltrrid	⊢ ( 𝑅 ∈ Ring → 𝐶 ∈ ℕ0 )