Theorem isghm

Description: Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014) (Proof shortened by SN, 5-Jun-2025)

	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	adantr	$$⊢\left(s=S\wedge t=T\right)\to {\mathrm{Base}}_s=X$$
16		fveq2	$$⊢t=T\to {\mathrm{Base}}_t={\mathrm{Base}}_T$$
17	16 2	eqtr4di	$$⊢t=T\to {\mathrm{Base}}_t=Y$$
18	17	adantl	$$⊢\left(s=S\wedge t=T\right)\to {\mathrm{Base}}_t=Y$$
19	15 18	feq23d	$$⊢\left(s=S\wedge t=T\right)\to \left(f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\leftrightarrow f:X⟶Y\right)$$
20		fveq2	$$⊢s=S\to {+}_s={+}_S$$
21	20 3	eqtr4di	$$⊢s=S\to {+}_s=\underset{\dot{}}{+}$$
22	21	oveqd	$$⊢s=S\to u{+}_{s}v=u\underset{\dot{}}{+}v$$
23	22	fveq2d	$$⊢s=S\to f\left(u{+}_{s}v\right)=f\left(u\underset{\dot{}}{+}v\right)$$
24		fveq2	$$⊢t=T\to {+}_t={+}_T$$
25	24 4	eqtr4di	$$⊢t=T\to {+}_t=\underset{\dot{}}{⨣}$$
26	25	oveqd	$$⊢t=T\to f\left(u\right){+}_{t}f\left(v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)$$
27	23 26	eqeqan12d	$$⊢\left(s=S\wedge t=T\right)\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)\underset{\dot{}}{⨣}f\left(v\right)\right)$$
28	15 27	raleqbidv	$$⊢\left(s=S\wedge t=T\right)\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)\underset{\dot{}}{⨣}f\left(v\right)\right)$$
29	15 28	raleqbidv	$$⊢\left(s=S\wedge t=T\right)\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)\underset{\dot{}}{⨣}f\left(v\right)\right)$$
30	19 29	anbi12d	$$⊢\left(s=S\wedge t=T\right)\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⟶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)$$
31	12 30	bitrid	$$⊢\left(s=S\wedge t=T\right)\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⟶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)$$
32	31	abbidv	$$⊢\left(s=S\wedge t=T\right)\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⟶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\}$$
33	2	fvexi	$$⊢Y\in \mathrm{V}$$
34		fsetex	$$⊢Y\in \mathrm{V}\to \left\{f|f:X⟶Y\right\}\in \mathrm{V}$$
35	33 34	ax-mp	$$⊢\left\{f|f:X⟶Y\right\}\in \mathrm{V}$$
36		abanssl	$$⊢\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\}$$
37	35 36	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}$$
38	32 5 37	ovmpoa	$$⊢\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\}$$
39	38	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)$$
40	1	fvexi	$$⊢X\in \mathrm{V}$$
41		fex2	$$⊢\left(F:X⟶Y\wedge X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to F\in \mathrm{V}$$
42	40 33 41	mp3an23	$$⊢F:X⟶Y\to F\in \mathrm{V}$$
43	42	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}$$
44		feq1	$$⊢f=F\to \left(f:X⟶Y\leftrightarrow F:X⟶Y\right)$$
45		fveq1	$$⊢f=F\to f\left(u\underset{\dot{}}{+}v\right)=F\left(u\underset{\dot{}}{+}v\right)$$
46		fveq1	$$⊢f=F\to f\left(u\right)=F\left(u\right)$$
47		fveq1	$$⊢f=F\to f\left(v\right)=F\left(v\right)$$
48	46 47	oveq12d	$$⊢f=F\to f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)$$
49	45 48	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)$$
50	49	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)$$
51	44 50	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)$$
52	43 51	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)$$
53	39 52	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)$$
54	6 53	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)$$