Metamath Proof Explorer


Theorem cntri

Description: Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses cntri.b B = Base M
cntri.p + ˙ = + M
cntri.z Z = Cntr M
Assertion cntri X Z Y B X + ˙ Y = Y + ˙ X

Proof

Step Hyp Ref Expression
1 cntri.b B = Base M
2 cntri.p + ˙ = + M
3 cntri.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 X Z X Cntz M B
8 2 4 cntzi X Cntz M B Y B X + ˙ Y = Y + ˙ X
9 7 8 sylanb X Z Y B X + ˙ Y = Y + ˙ X