Theorem isghm

Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014)

	Ref	Expression
Hypotheses	isghm.w	$$⊢X={\mathrm{Base}}_S$$
	isghm.x	$$⊢Y={\mathrm{Base}}_T$$
	isghm.a	$$⊢\underset{\dot{}}{+}={+}_S$$
	isghm.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
Assertion	isghm	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\wedge \left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isghm.w	$$⊢X={\mathrm{Base}}_S$$
2		isghm.x	$$⊢Y={\mathrm{Base}}_T$$
3		isghm.a	$$⊢\underset{\dot{}}{+}={+}_S$$
4		isghm.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
5		df-ghm	$$⊢\mathrm{GrpHom}=\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(f:w⟶{\mathrm{Base}}_t\wedge \forall u\in w\forall v\in wf\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\right\}\right)$$
6	5	elmpocl	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)$$
7		fvex	$$⊢{\mathrm{Base}}_s\in \mathrm{V}$$
8		feq2	$$⊢w={\mathrm{Base}}_s\to \left(f:w⟶{\mathrm{Base}}_t\leftrightarrow f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\right)$$
9		raleq	$$⊢w={\mathrm{Base}}_s\to \left(\forall v\in wf\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\leftrightarrow \forall v\in {\mathrm{Base}}_{s}f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)$$
10	9	raleqbi1dv	$$⊢w={\mathrm{Base}}_s\to \left(\forall u\in w\forall v\in wf\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\leftrightarrow \forall u\in {\mathrm{Base}}_s\forall v\in {\mathrm{Base}}_{s}f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)$$
11	8 10	anbi12d	$$⊢w={\mathrm{Base}}_s\to \left(\left(f:w⟶{\mathrm{Base}}_t\wedge \forall u\in w\forall v\in wf\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\wedge \forall u\in {\mathrm{Base}}_s\forall v\in {\mathrm{Base}}_{s}f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\right)$$
12	7 11	sbcie	$$⊢\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(f:w⟶{\mathrm{Base}}_t\wedge \forall u\in w\forall v\in wf\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\leftrightarrow \left(f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\wedge \forall u\in {\mathrm{Base}}_s\forall v\in {\mathrm{Base}}_{s}f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)$$
13		fveq2	$$⊢s=S\to {\mathrm{Base}}_s={\mathrm{Base}}_S$$
14	13 1	eqtr4di	$$⊢s=S\to {\mathrm{Base}}_s=X$$
15	14	feq2d	$$⊢s=S\to \left(f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\leftrightarrow f:X⟶{\mathrm{Base}}_t\right)$$
16		fveq2	$$⊢s=S\to {+}_s={+}_S$$
17	16 3	eqtr4di	$$⊢s=S\to {+}_s=\underset{\dot{}}{+}$$
18	17	oveqd	$$⊢s=S\to u{+}_{s}v=u\underset{\dot{}}{+}v$$
19	18	fveqeq2d	$$⊢s=S\to \left(f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\leftrightarrow f\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)$$
20	14 19	raleqbidv	$$⊢s=S\to \left(\forall v\in {\mathrm{Base}}_{s}f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\leftrightarrow \forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)$$
21	14 20	raleqbidv	$$⊢s=S\to \left(\forall u\in {\mathrm{Base}}_s\forall v\in {\mathrm{Base}}_{s}f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\leftrightarrow \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)$$
22	15 21	anbi12d	$$⊢s=S\to \left(\left(f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\wedge \forall u\in {\mathrm{Base}}_s\forall v\in {\mathrm{Base}}_{s}f\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\leftrightarrow \left(f:X⟶{\mathrm{Base}}_t\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\right)$$
23	12 22	syl5bb	$$⊢s=S\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(f:w⟶{\mathrm{Base}}_t\wedge \forall u\in w\forall v\in wf\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\leftrightarrow \left(f:X⟶{\mathrm{Base}}_t\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\right)$$
24	23	abbidv	$$⊢s=S\to \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(f:w⟶{\mathrm{Base}}_t\wedge \forall u\in w\forall v\in wf\left(u{+}_{s}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\right\}=\left\{f|\left(f:X⟶{\mathrm{Base}}_t\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\right\}$$
25		fveq2	$$⊢t=T\to {\mathrm{Base}}_t={\mathrm{Base}}_T$$
26	25 2	eqtr4di	$$⊢t=T\to {\mathrm{Base}}_t=Y$$
27	26	feq3d	$$⊢t=T\to \left(f:X⟶{\mathrm{Base}}_t\leftrightarrow f:X⟶Y\right)$$
28		fveq2	$$⊢t=T\to {+}_t={+}_T$$
29	28 4	eqtr4di	$$⊢t=T\to {+}_t=\underset{\dot{}}{⨣}$$
30	29	oveqd	$$⊢t=T\to f\left(u\right){+}_{t}f\left(v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)$$
31	30	eqeq2d	$$⊢t=T\to \left(f\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\leftrightarrow f\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)$$
32	31	2ralbidv	$$⊢t=T\to \left(\forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\leftrightarrow \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)$$
33	27 32	anbi12d	$$⊢t=T\to \left(\left(f:X⟶{\mathrm{Base}}_t\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\leftrightarrow \left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\right)$$
34	33	abbidv	$$⊢t=T\to \left\{f|\left(f:X⟶{\mathrm{Base}}_t\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right){+}_{t}f\left(v\right)\right)\right\}=\left\{f|\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\right\}$$
35	1	fvexi	$$⊢X\in \mathrm{V}$$
36	2	fvexi	$$⊢Y\in \mathrm{V}$$
37		mapex	$$⊢\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to \left\{f|f:X⟶Y\right\}\in \mathrm{V}$$
38	35 36 37	mp2an	$$⊢\left\{f|f:X⟶Y\right\}\in \mathrm{V}$$
39		simpl	$$⊢\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\to f:X⟶Y$$
40	39	ss2abi	$$⊢\left\{f|\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\right\}\subseteq \left\{f|f:X⟶Y\right\}$$
41	38 40	ssexi	$$⊢\left\{f|\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\right\}\in \mathrm{V}$$
42	24 34 5 41	ovmpo	$$⊢\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\to S\mathrm{GrpHom}T=\left\{f|\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\right\}$$
43	42	eleq2d	$$⊢\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\to \left(F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow F\in \left\{f|\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\right\}\right)$$
44		fex	$$⊢\left(F:X⟶Y\wedge X\in \mathrm{V}\right)\to F\in \mathrm{V}$$
45	35 44	mpan2	$$⊢F:X⟶Y\to F\in \mathrm{V}$$
46	45	adantr	$$⊢\left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\to F\in \mathrm{V}$$
47		feq1	$$⊢f=F\to \left(f:X⟶Y\leftrightarrow F:X⟶Y\right)$$
48		fveq1	$$⊢f=F\to f\left(u\underset{\dot{}}{+}v\right)=F\left(u\underset{\dot{}}{+}v\right)$$
49		fveq1	$$⊢f=F\to f\left(u\right)=F\left(u\right)$$
50		fveq1	$$⊢f=F\to f\left(v\right)=F\left(v\right)$$
51	49 50	oveq12d	$$⊢f=F\to f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)$$
52	48 51	eqeq12d	$$⊢f=F\to \left(f\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\leftrightarrow F\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)$$
53	52	2ralbidv	$$⊢f=F\to \left(\forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\leftrightarrow \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)$$
54	47 53	anbi12d	$$⊢f=F\to \left(\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\leftrightarrow \left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\right)$$
55	46 54	elab3	$$⊢F\in \left\{f|\left(f:X⟶Y\wedge \forall u\in X\forall v\in Xf\left(u\underset{\dot{}}{+}v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)\right)\right\}\leftrightarrow \left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)$$
56	43 55	bitrdi	$$⊢\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\to \left(F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\right)$$
57	6 56	biadanii	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\wedge \left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\right)$$