Theorem chrcl

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

	Ref	Expression
Hypothesis	chrcl.c	|- C = ( chr ` R )
Assertion	chrcl	|- ( R e. Ring -> C e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		chrcl.c	|- C = ( chr ` R )
2		eqid	|- ( od ` R ) = ( od ` R )
3		eqid	|- ( 1r ` R ) = ( 1r ` R )
4	2 3 1	chrval	|- ( ( od ` R ) ` ( 1r ` R ) ) = C
5		eqid	|- ( Base ` R ) = ( Base ` R )
6	5 3	ringidcl	|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
7	5 2	odcl	|- ( ( 1r ` R ) e. ( Base ` R ) -> ( ( od ` R ) ` ( 1r ` R ) ) e. NN0 )
8	6 7	syl	|- ( R e. Ring -> ( ( od ` R ) ` ( 1r ` R ) ) e. NN0 )
9	4 8	eqeltrrid	|- ( R e. Ring -> C e. NN0 )