Theorem ismgmhm

Description: Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	ismgmhm.b	$$⊢B={\mathrm{Base}}_S$$
	ismgmhm.c	$$⊢C={\mathrm{Base}}_T$$
	ismgmhm.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	ismgmhm.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
Assertion	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⟶C\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)$$

Proof

Step	Hyp	Ref	Expression
1		ismgmhm.b	$$⊢B={\mathrm{Base}}_S$$
2		ismgmhm.c	$$⊢C={\mathrm{Base}}_T$$
3		ismgmhm.p	$$⊢\underset{\dot{}}{+}={+}_S$$
4		ismgmhm.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
5		mgmhmrcl	$$⊢F\in \left(S\mathrm{MgmHom}T\right)\to \left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\right)$$
6		fveq2	$$⊢t=T\to {\mathrm{Base}}_t={\mathrm{Base}}_T$$
7	6 2	eqtr4di	$$⊢t=T\to {\mathrm{Base}}_t=C$$
8		fveq2	$$⊢s=S\to {\mathrm{Base}}_s={\mathrm{Base}}_S$$
9	8 1	eqtr4di	$$⊢s=S\to {\mathrm{Base}}_s=B$$
10	7 9	oveqan12rd	$$⊢\left(s=S\wedge t=T\right)\to {{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}=C^B$$
11	9	adantr	$$⊢\left(s=S\wedge t=T\right)\to {\mathrm{Base}}_s=B$$
12		fveq2	$$⊢s=S\to {+}_s={+}_S$$
13	12 3	eqtr4di	$$⊢s=S\to {+}_s=\underset{\dot{}}{+}$$
14	13	oveqd	$$⊢s=S\to x{+}_{s}y=x\underset{\dot{}}{+}y$$
15	14	fveq2d	$$⊢s=S\to f\left(x{+}_{s}y\right)=f\left(x\underset{\dot{}}{+}y\right)$$
16		fveq2	$$⊢t=T\to {+}_t={+}_T$$
17	16 4	eqtr4di	$$⊢t=T\to {+}_t=\underset{\dot{}}{⨣}$$
18	17	oveqd	$$⊢t=T\to f\left(x\right){+}_{t}f\left(y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)$$
19	15 18	eqeqan12d	$$⊢\left(s=S\wedge t=T\right)\to \left(f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\leftrightarrow f\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\right)$$
20	11 19	raleqbidv	$$⊢\left(s=S\wedge t=T\right)\to \left(\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\leftrightarrow \forall y\in Bf\left(x\underset{\dot{}}{+}y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)\right)$$
21	11 20	raleqbidv	$$⊢\left(s=S\wedge t=T\right)\to \left(\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)\leftrightarrow \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)$$
22	10 21	rabeqbidv	$$⊢\left(s=S\wedge t=T\right)\to \left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\right\}=\left\{f\in \left(C^B\right)|\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\}$$
23		df-mgmhm	$$⊢\mathrm{MgmHom}=\left(s\in \mathrm{Mgm},t\in \mathrm{Mgm}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\right\}\right)$$
24		ovex	$$⊢C^B\in \mathrm{V}$$
25	24	rabex	$$⊢\left\{f\in \left(C^B\right)|\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\}\in \mathrm{V}$$
26	22 23 25	ovmpoa	$$⊢\left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\right)\to S\mathrm{MgmHom}T=\left\{f\in \left(C^B\right)|\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\}$$
27	26	eleq2d	$$⊢\left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\right)\to \left(F\in \left(S\mathrm{MgmHom}T\right)\leftrightarrow F\in \left\{f\in \left(C^B\right)|\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)$$
28		fveq1	$$⊢f=F\to f\left(x\underset{\dot{}}{+}y\right)=F\left(x\underset{\dot{}}{+}y\right)$$
29		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
30		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
31	29 30	oveq12d	$$⊢f=F\to f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
32	28 31	eqeq12d	$$⊢f=F\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)$$
33	32	2ralbidv	$$⊢f=F\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)\leftrightarrow \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)$$
34	33	elrab	$$⊢F\in \left\{f\in \left(C^B\right)|\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\}\leftrightarrow \left(F\in \left(C^B\right)\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)$$
35	2	fvexi	$$⊢C\in \mathrm{V}$$
36	1	fvexi	$$⊢B\in \mathrm{V}$$
37	35 36	elmap	$$⊢F\in \left(C^B\right)\leftrightarrow F:B⟶C$$
38	37	anbi1i	$$⊢\left(F\in \left(C^B\right)\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)\leftrightarrow \left(F:B⟶C\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)$$
39	34 38	bitri	$$⊢F\in \left\{f\in \left(C^B\right)|\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\}\leftrightarrow \left(F:B⟶C\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)$$
40	27 39	bitrdi	$$⊢\left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\right)\to \left(F\in \left(S\mathrm{MgmHom}T\right)\leftrightarrow \left(F:B⟶C\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)$$
41	5 40	biadanii	$$⊢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⟶C\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)$$