Metamath Proof Explorer


Theorem elcntzsn

Description: Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses cntzfval.b B = Base M
cntzfval.p + ˙ = + M
cntzfval.z Z = Cntz M
Assertion elcntzsn Y B X Z Y X B X + ˙ Y = Y + ˙ X

Proof

Step Hyp Ref Expression
1 cntzfval.b B = Base M
2 cntzfval.p + ˙ = + M
3 cntzfval.z Z = Cntz M
4 1 2 3 cntzsnval Y B Z Y = x B | x + ˙ Y = Y + ˙ x
5 4 eleq2d Y B X Z Y X x B | x + ˙ Y = Y + ˙ x
6 oveq1 x = X x + ˙ Y = X + ˙ Y
7 oveq2 x = X Y + ˙ x = Y + ˙ X
8 6 7 eqeq12d x = X x + ˙ Y = Y + ˙ x X + ˙ Y = Y + ˙ X
9 8 elrab X x B | x + ˙ Y = Y + ˙ x X B X + ˙ Y = Y + ˙ X
10 5 9 bitrdi Y B X Z Y X B X + ˙ Y = Y + ˙ X