Theorem mgmhmlin

Description: A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	mgmhmlin.b	$$⊢B={\mathrm{Base}}_S$$
	mgmhmlin.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	mgmhmlin.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
Assertion	mgmhmlin	$$⊢\left(F\in \left(S\mathrm{MgmHom}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		mgmhmlin.b	$$⊢B={\mathrm{Base}}_S$$
2		mgmhmlin.p	$$⊢\underset{\dot{}}{+}={+}_S$$
3		mgmhmlin.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
4		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
5	1 4 2 3	ismgmhm	$$⊢F\in \left(S\mathrm{MgmHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\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)\right)\right)$$
6		fvoveq1	$$⊢x=X\to F\left(x\underset{\dot{}}{+}y\right)=F\left(X\underset{\dot{}}{+}y\right)$$
7		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
8	7	oveq1d	$$⊢x=X\to F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(y\right)$$
9	6 8	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)$$
10		oveq2	$$⊢y=Y\to X\underset{\dot{}}{+}y=X\underset{\dot{}}{+}Y$$
11	10	fveq2d	$$⊢y=Y\to F\left(X\underset{\dot{}}{+}y\right)=F\left(X\underset{\dot{}}{+}Y\right)$$
12		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
13	12	oveq2d	$$⊢y=Y\to F\left(X\right)\underset{\dot{}}{⨣}F\left(y\right)=F\left(X\right)\underset{\dot{}}{⨣}F\left(Y\right)$$
14	11 13	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)$$
15	9 14	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)$$
16	15	com12	$$⊢\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 \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)$$
17	16	ad2antll	$$⊢\left(\left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\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)\right)\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)$$
18	5 17	sylbi	$$⊢F\in \left(S\mathrm{MgmHom}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)$$
19	18	3impib	$$⊢\left(F\in \left(S\mathrm{MgmHom}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)$$