This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES The complex numbers as an algebraic extensible structure Algebraic constructions based on the complex numbers 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 ‘ 𝑔 ) ) )