Metamath Proof Explorer


Theorem cntzel

Description: Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses cntzfval.b B=BaseM
cntzfval.p +˙=+M
cntzfval.z Z=CntzM
Assertion cntzel SBXBXZSySX+˙y=y+˙X

Proof

Step Hyp Ref Expression
1 cntzfval.b B=BaseM
2 cntzfval.p +˙=+M
3 cntzfval.z Z=CntzM
4 1 2 3 elcntz SBXZSXBySX+˙y=y+˙X
5 4 baibd SBXBXZSySX+˙y=y+˙X