Description: Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cntzfval.b | |
|
cntzfval.p | |
||
cntzfval.z | |
||
Assertion | cntzel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cntzfval.b | |
|
2 | cntzfval.p | |
|
3 | cntzfval.z | |
|
4 | 1 2 3 | elcntz | |
5 | 4 | baibd | |