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

Metamath Proof Explorer

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 \in Ring \to C \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		chrcl.c	$⊢ C = chr (R)$
2		eqid	$⊢ od (R) = od (R)$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	2 3 1	chrval	$⊢ od (R) (1_{R}) = C$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5 3	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
7	5 2	odcl	$⊢ 1_{R} \in {Base}_{R} \to od (R) (1_{R}) \in ℕ_{0}$
8	6 7	syl	$⊢ R \in Ring \to od (R) (1_{R}) \in ℕ_{0}$
9	4 8	eqeltrrid	$⊢ R \in Ring \to C \in ℕ_{0}$