Metamath Proof Explorer


Theorem cntzcmnf

Description: Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cntzcmnf.b B=BaseG
cntzcmnf.z Z=CntzG
cntzcmnf.g φGCMnd
cntzcmnf.f φF:AB
Assertion cntzcmnf φranFZranF

Proof

Step Hyp Ref Expression
1 cntzcmnf.b B=BaseG
2 cntzcmnf.z Z=CntzG
3 cntzcmnf.g φGCMnd
4 cntzcmnf.f φF:AB
5 4 frnd φranFB
6 1 2 cntzcmn GCMndranFBZranF=B
7 3 5 6 syl2anc φZranF=B
8 5 7 sseqtrrd φranFZranF