Database
BASIC ALGEBRAIC STRUCTURES
Groups
Centralizers and centers
elcntr
Next ⟩
cntrss
Metamath Proof Explorer
Ascii
Unicode
Theorem
elcntr
Description:
Elementhood in the center of a magma.
(Contributed by
SN
, 21-Mar-2025)
Ref
Expression
Hypotheses
elcntr.b
⊢
B
=
Base
M
elcntr.p
⊢
+
˙
=
+
M
elcntr.z
⊢
Z
=
Cntr
⁡
M
Assertion
elcntr
⊢
A
∈
Z
↔
A
∈
B
∧
∀
y
∈
B
A
+
˙
y
=
y
+
˙
A
Proof
Step
Hyp
Ref
Expression
1
elcntr.b
⊢
B
=
Base
M
2
elcntr.p
⊢
+
˙
=
+
M
3
elcntr.z
⊢
Z
=
Cntr
⁡
M
4
eqid
⊢
Cntz
⁡
M
=
Cntz
⁡
M
5
1
4
cntrval
⊢
Cntz
⁡
M
⁡
B
=
Cntr
⁡
M
6
3
5
eqtr4i
⊢
Z
=
Cntz
⁡
M
⁡
B
7
6
eleq2i
⊢
A
∈
Z
↔
A
∈
Cntz
⁡
M
⁡
B
8
ssid
⊢
B
⊆
B
9
1
2
4
elcntz
⊢
B
⊆
B
→
A
∈
Cntz
⁡
M
⁡
B
↔
A
∈
B
∧
∀
y
∈
B
A
+
˙
y
=
y
+
˙
A
10
8
9
ax-mp
⊢
A
∈
Cntz
⁡
M
⁡
B
↔
A
∈
B
∧
∀
y
∈
B
A
+
˙
y
=
y
+
˙
A
11
7
10
bitri
⊢
A
∈
Z
↔
A
∈
B
∧
∀
y
∈
B
A
+
˙
y
=
y
+
˙
A