Theorem ismhm

Description: Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Hypotheses	ismhm.b	$$⊢B={\mathrm{Base}}_S$$
	ismhm.c	$$⊢C={\mathrm{Base}}_T$$
	ismhm.p	$$⊢\underset{\dot{}}{+}={+}_S$$
	ismhm.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
	ismhm.z	$$⊢\underset{\dot{}}{0}=0_S$$
	ismhm.y	$$⊢Y=0_T$$
Assertion	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⟶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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismhm.b	$$⊢B={\mathrm{Base}}_S$$
2		ismhm.c	$$⊢C={\mathrm{Base}}_T$$
3		ismhm.p	$$⊢\underset{\dot{}}{+}={+}_S$$
4		ismhm.q	$$⊢\underset{\dot{}}{⨣}={+}_T$$
5		ismhm.z	$$⊢\underset{\dot{}}{0}=0_S$$
6		ismhm.y	$$⊢Y=0_T$$
7		df-mhm	$$⊢\mathrm{MndHom}=\left(s\in \mathrm{Mnd},t\in \mathrm{Mnd}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\wedge f\left(0_s\right)=0_t\right)\right\}\right)$$
8	7	elmpocl	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to \left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)$$
9		fveq2	$$⊢t=T\to {\mathrm{Base}}_t={\mathrm{Base}}_T$$
10	9 2	eqtr4di	$$⊢t=T\to {\mathrm{Base}}_t=C$$
11		fveq2	$$⊢s=S\to {\mathrm{Base}}_s={\mathrm{Base}}_S$$
12	11 1	eqtr4di	$$⊢s=S\to {\mathrm{Base}}_s=B$$
13	10 12	oveqan12rd	$$⊢\left(s=S\wedge t=T\right)\to {{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}=C^B$$
14	12	adantr	$$⊢\left(s=S\wedge t=T\right)\to {\mathrm{Base}}_s=B$$
15		fveq2	$$⊢s=S\to {+}_s={+}_S$$
16	15 3	eqtr4di	$$⊢s=S\to {+}_s=\underset{\dot{}}{+}$$
17	16	oveqd	$$⊢s=S\to x{+}_{s}y=x\underset{\dot{}}{+}y$$
18	17	fveq2d	$$⊢s=S\to f\left(x{+}_{s}y\right)=f\left(x\underset{\dot{}}{+}y\right)$$
19		fveq2	$$⊢t=T\to {+}_t={+}_T$$
20	19 4	eqtr4di	$$⊢t=T\to {+}_t=\underset{\dot{}}{⨣}$$
21	20	oveqd	$$⊢t=T\to f\left(x\right){+}_{t}f\left(y\right)=f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)$$
22	18 21	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)$$
23	14 22	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)$$
24	14 23	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)$$
25		fveq2	$$⊢s=S\to 0_s=0_S$$
26	25 5	eqtr4di	$$⊢s=S\to 0_s=\underset{\dot{}}{0}$$
27	26	fveq2d	$$⊢s=S\to f\left(0_s\right)=f\left(\underset{\dot{}}{0}\right)$$
28		fveq2	$$⊢t=T\to 0_t=0_T$$
29	28 6	eqtr4di	$$⊢t=T\to 0_t=Y$$
30	27 29	eqeqan12d	$$⊢\left(s=S\wedge t=T\right)\to \left(f\left(0_s\right)=0_t\leftrightarrow f\left(\underset{\dot{}}{0}\right)=Y\right)$$
31	24 30	anbi12d	$$⊢\left(s=S\wedge t=T\right)\to \left(\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)\wedge f\left(0_s\right)=0_t\right)\leftrightarrow \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)\wedge f\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$
32	13 31	rabeqbidv	$$⊢\left(s=S\wedge t=T\right)\to \left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\wedge f\left(0_s\right)=0_t\right)\right\}=\left\{f\in \left(C^B\right)|\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)\wedge f\left(\underset{\dot{}}{0}\right)=Y\right)\right\}$$
33		ovex	$$⊢C^B\in \mathrm{V}$$
34	33	rabex	$$⊢\left\{f\in \left(C^B\right)|\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)\wedge f\left(\underset{\dot{}}{0}\right)=Y\right)\right\}\in \mathrm{V}$$
35	32 7 34	ovmpoa	$$⊢\left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)\to S\mathrm{MndHom}T=\left\{f\in \left(C^B\right)|\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)\wedge f\left(\underset{\dot{}}{0}\right)=Y\right)\right\}$$
36	35	eleq2d	$$⊢\left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)\to \left(F\in \left(S\mathrm{MndHom}T\right)\leftrightarrow F\in \left\{f\in \left(C^B\right)|\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)\wedge f\left(\underset{\dot{}}{0}\right)=Y\right)\right\}\right)$$
37	2	fvexi	$$⊢C\in \mathrm{V}$$
38	1	fvexi	$$⊢B\in \mathrm{V}$$
39	37 38	elmap	$$⊢F\in \left(C^B\right)\leftrightarrow F:B⟶C$$
40	39	anbi1i	$$⊢\left(F\in \left(C^B\right)\wedge \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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)\leftrightarrow \left(F:B⟶C\wedge \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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$
41		fveq1	$$⊢f=F\to f\left(x\underset{\dot{}}{+}y\right)=F\left(x\underset{\dot{}}{+}y\right)$$
42		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
43		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
44	42 43	oveq12d	$$⊢f=F\to f\left(x\right)\underset{\dot{}}{⨣}f\left(y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
45	41 44	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)$$
46	45	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)$$
47		fveq1	$$⊢f=F\to f\left(\underset{\dot{}}{0}\right)=F\left(\underset{\dot{}}{0}\right)$$
48	47	eqeq1d	$$⊢f=F\to \left(f\left(\underset{\dot{}}{0}\right)=Y\leftrightarrow F\left(\underset{\dot{}}{0}\right)=Y\right)$$
49	46 48	anbi12d	$$⊢f=F\to \left(\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)\wedge f\left(\underset{\dot{}}{0}\right)=Y\right)\leftrightarrow \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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$
50	49	elrab	$$⊢F\in \left\{f\in \left(C^B\right)|\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)\wedge f\left(\underset{\dot{}}{0}\right)=Y\right)\right\}\leftrightarrow \left(F\in \left(C^B\right)\wedge \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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$
51		3anass	$$⊢\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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\leftrightarrow \left(F:B⟶C\wedge \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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$
52	40 50 51	3bitr4i	$$⊢F\in \left\{f\in \left(C^B\right)|\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)\wedge f\left(\underset{\dot{}}{0}\right)=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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)$$
53	36 52	syl6bb	$$⊢\left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)\to \left(F\in \left(S\mathrm{MndHom}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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$
54	8 53	biadanii	$$⊢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⟶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)\wedge F\left(\underset{\dot{}}{0}\right)=Y\right)\right)$$