Theorem mhmlin

Description: A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Hypotheses	mhmlin.b	$$⊢B={\mathrm{Base}}_S$$
	mhmlin.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	mhmlin.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
Assertion	mhmlin	$$⊢\left(F\in \left(S\mathrm{MndHom}T\right)\wedge X\in B\wedge Y\in B\right)\to F\left(X\underset{\dot{}}{+}Y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mhmlin.b	$$⊢B={\mathrm{Base}}_S$$
2		mhmlin.p	$$⊢\underset{\dot{}}{+}={+}_S$$
3		mhmlin.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
4		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
5		eqid	$$⊢0_S=0_S$$
6		eqid	$$⊢0_T=0_T$$
7	1 4 2 3 5 6	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:B⟶{\mathrm{Base}}_T\wedge \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\wedge F\left(0_S\right)=0_T\right)\right)$$
8	7	simprbi	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to \left(F:B⟶{\mathrm{Base}}_T\wedge \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\wedge F\left(0_S\right)=0_T\right)$$
9	8	simp2d	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to \forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
10		fvoveq1	$$⊢x=X\to F\left(x\underset{\dot{}}{+}y\right)=F\left(X\underset{\dot{}}{+}y\right)$$
11		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
12	11	oveq1d	$$⊢x=X\to F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(y\right)$$
13	10 12	eqeq12d	$$⊢x=X\to \left(F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\leftrightarrow F\left(X\underset{\dot{}}{+}y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(y\right)\right)$$
14		oveq2	$$⊢y=Y\to X\underset{\dot{}}{+}y=X\underset{\dot{}}{+}Y$$
15	14	fveq2d	$$⊢y=Y\to F\left(X\underset{\dot{}}{+}y\right)=F\left(X\underset{\dot{}}{+}Y\right)$$
16		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
17	16	oveq2d	$$⊢y=Y\to F\left(X\right)\underset{\dot{}}{⨣}F\left(y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(Y\right)$$
18	15 17	eqeq12d	$$⊢y=Y\to \left(F\left(X\underset{\dot{}}{+}y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(y\right)\leftrightarrow F\left(X\underset{\dot{}}{+}Y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(Y\right)\right)$$
19	13 18	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in BF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\to F\left(X\underset{\dot{}}{+}Y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(Y\right)\right)$$
20	9 19	syl5com	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to \left(\left(X\in B\wedge Y\in B\right)\to F\left(X\underset{\dot{}}{+}Y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(Y\right)\right)$$
21	20	3impib	$$⊢\left(F\in \left(S\mathrm{MndHom}T\right)\wedge X\in B\wedge Y\in B\right)\to F\left(X\underset{\dot{}}{+}Y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(Y\right)$$