This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Define thecenter of a magma, which is the elements that commute with
all others. (Contributed by Stefan O'Rear, 5-Sep-2015)
|
|
Ref |
Expression |
|
Assertion |
df-cntr |
⊢ Cntr = ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) ) |
Detailed syntax breakdown
| Step |
Hyp |
Ref |
Expression |
| 0 |
|
ccntr |
⊢ Cntr |
| 1 |
|
vm |
⊢ 𝑚 |
| 2 |
|
cvv |
⊢ V |
| 3 |
|
ccntz |
⊢ Cntz |
| 4 |
1
|
cv |
⊢ 𝑚 |
| 5 |
4 3
|
cfv |
⊢ ( Cntz ‘ 𝑚 ) |
| 6 |
|
cbs |
⊢ Base |
| 7 |
4 6
|
cfv |
⊢ ( Base ‘ 𝑚 ) |
| 8 |
7 5
|
cfv |
⊢ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) |
| 9 |
1 2 8
|
cmpt |
⊢ ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) ) |
| 10 |
0 9
|
wceq |
⊢ Cntr = ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) ) |