Metamath Proof Explorer


Theorem mgmhmrcl

Description: Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020)

Ref Expression
Assertion mgmhmrcl FSMgmHomTSMgmTMgm

Proof

Step Hyp Ref Expression
1 df-mgmhm MgmHom=sMgm,tMgmfBasetBases|xBasesyBasesfx+sy=fx+tfy
2 1 elmpocl FSMgmHomTSMgmTMgm