Definition df-chr

Description: The characteristic of a ring is the smallest positive integer which is equal to 0 when interpreted in the ring, or 0 if there is no such positive integer. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Assertion	df-chr	⊢ chr = ( 𝑔 ∈ V ↦ ( ( od ‘ 𝑔 ) ‘ ( 1r ‘ 𝑔 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cchr	⊢ chr
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		cod	⊢ od
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( od ‘ 𝑔 )
6		cur	⊢ 1r
7	4 6	cfv	⊢ ( 1r ‘ 𝑔 )
8	7 5	cfv	⊢ ( ( od ‘ 𝑔 ) ‘ ( 1r ‘ 𝑔 ) )
9	1 2 8	cmpt	⊢ ( 𝑔 ∈ V ↦ ( ( od ‘ 𝑔 ) ‘ ( 1r ‘ 𝑔 ) ) )
10	0 9	wceq	⊢ chr = ( 𝑔 ∈ V ↦ ( ( od ‘ 𝑔 ) ‘ ( 1r ‘ 𝑔 ) ) )