Theorem chrcl

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

	Ref	Expression
Hypothesis	chrcl.c	$$⊢C=\mathrm{chr}\left(R\right)$$
Assertion	chrcl	$$⊢R\in \mathrm{Ring}\to C\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		chrcl.c	$$⊢C=\mathrm{chr}\left(R\right)$$
2		eqid	$$⊢\mathrm{od}\left(R\right)=\mathrm{od}\left(R\right)$$
3		eqid	$$⊢1_R=1_R$$
4	2 3 1	chrval	$$⊢\mathrm{od}\left(R\right)\left(1_R\right)=C$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	5 3	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
7	5 2	odcl	$$⊢1_R\in {\mathrm{Base}}_R\to \mathrm{od}\left(R\right)\left(1_R\right)\in {\mathbb{N}}_0$$
8	6 7	syl	$$⊢R\in \mathrm{Ring}\to \mathrm{od}\left(R\right)\left(1_R\right)\in {\mathbb{N}}_0$$
9	4 8	eqeltrrid	$$⊢R\in \mathrm{Ring}\to C\in {\mathbb{N}}_0$$