Theorem mhm0

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

	Ref	Expression
Hypotheses	mhm0.z	$$⊢\underset{\dot{}}{0}=0_S$$
	mhm0.y	$$⊢Y=0_T$$
Assertion	mhm0	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to F\left(\underset{\dot{}}{0}\right)=Y$$

Proof

Step	Hyp	Ref	Expression
1		mhm0.z	$$⊢\underset{\dot{}}{0}=0_S$$
2		mhm0.y	$$⊢Y=0_T$$
3		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
4		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
5		eqid	$$⊢{+}_S={+}_S$$
6		eqid	$$⊢{+}_T={+}_T$$
7	3 4 5 6 1 2	ismhm	$$⊢F\in \left(S\mathrm{MndHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)\wedge \left(F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T\wedge \forall x\in {\mathrm{Base}}_S\forall y\in {\mathrm{Base}}_{S}F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$
8	7	simprbi	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to \left(F:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T\wedge \forall x\in {\mathrm{Base}}_S\forall y\in {\mathrm{Base}}_{S}F\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)$$
9	8	simp3d	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to F\left(\underset{\dot{}}{0}\right)=Y$$