Metamath Proof Explorer


Theorem mhm0

Description: A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses mhm0.z 0˙=0S
mhm0.y Y=0T
Assertion mhm0 FSMndHomTF0˙=Y

Proof

Step Hyp Ref Expression
1 mhm0.z 0˙=0S
2 mhm0.y Y=0T
3 eqid BaseS=BaseS
4 eqid BaseT=BaseT
5 eqid +S=+S
6 eqid +T=+T
7 3 4 5 6 1 2 ismhm FSMndHomTSMndTMndF:BaseSBaseTxBaseSyBaseSFx+Sy=Fx+TFyF0˙=Y
8 7 simprbi FSMndHomTF:BaseSBaseTxBaseSyBaseSFx+Sy=Fx+TFyF0˙=Y
9 8 simp3d FSMndHomTF0˙=Y