Theorem sn-isghm

Description: Longer proof of isghm , unsuccessfully attempting to simplify isghm using elovmpo according to an editorial note (now removed). (Contributed by SN, 7-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sn-isghm.w	$$⊢X={\mathrm{Base}}_S$$
	sn-isghm.x	$$⊢Y={\mathrm{Base}}_T$$
	sn-isghm.a	$$⊢\underset{\dot{}}{+}={+}_S$$
	sn-isghm.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
Assertion	sn-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		sn-isghm.w	$$⊢X={\mathrm{Base}}_S$$
2		sn-isghm.x	$$⊢Y={\mathrm{Base}}_T$$
3		sn-isghm.a	$$⊢\underset{\dot{}}{+}={+}_S$$
4		sn-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		fvex	$$⊢{\mathrm{Base}}_s\in \mathrm{V}$$
7		feq2	$$⊢w={\mathrm{Base}}_s\to \left(f:w⟶{\mathrm{Base}}_t\leftrightarrow f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\right)$$
8		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)$$
9	8	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)$$
10	7 9	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)$$
11	6 10	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)$$
12	11	abbii	$$⊢\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:{\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\}$$
13		fvex	$$⊢{\mathrm{Base}}_t\in \mathrm{V}$$
14		fsetex	$$⊢{\mathrm{Base}}_t\in \mathrm{V}\to \left\{f|f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\right\}\in \mathrm{V}$$
15	13 14	ax-mp	$$⊢\left\{f|f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\right\}\in \mathrm{V}$$
16		abanssl	$$⊢\left\{f|\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\}\subseteq \left\{f|f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\right\}$$
17	15 16	ssexi	$$⊢\left\{f|\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\}\in \mathrm{V}$$
18	12 17	eqeltri	$$⊢\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\}\in \mathrm{V}$$
19		fveq2	$$⊢s=S\to {\mathrm{Base}}_s={\mathrm{Base}}_S$$
20	19 1	eqtr4di	$$⊢s=S\to {\mathrm{Base}}_s=X$$
21	20	adantr	$$⊢\left(s=S\wedge t=T\right)\to {\mathrm{Base}}_s=X$$
22		fveq2	$$⊢t=T\to {\mathrm{Base}}_t={\mathrm{Base}}_T$$
23	22 2	eqtr4di	$$⊢t=T\to {\mathrm{Base}}_t=Y$$
24	23	adantl	$$⊢\left(s=S\wedge t=T\right)\to {\mathrm{Base}}_t=Y$$
25	21 24	feq23d	$$⊢\left(s=S\wedge t=T\right)\to \left(f:{\mathrm{Base}}_s⟶{\mathrm{Base}}_t\leftrightarrow f:X⟶Y\right)$$
26		fveq2	$$⊢s=S\to {+}_s={+}_S$$
27	26 3	eqtr4di	$$⊢s=S\to {+}_s=\underset{\dot{}}{+}$$
28	27	oveqd	$$⊢s=S\to u{+}_{s}v=u\underset{\dot{}}{+}v$$
29	28	fveq2d	$$⊢s=S\to f\left(u{+}_{s}v\right)=f\left(u\underset{\dot{}}{+}v\right)$$
30		fveq2	$$⊢t=T\to {+}_t={+}_T$$
31	30 4	eqtr4di	$$⊢t=T\to {+}_t=\underset{\dot{}}{⨣}$$
32	31	oveqd	$$⊢t=T\to f\left(u\right){+}_{t}f\left(v\right)=f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)$$
33	29 32	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)$$
34	21 33	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)$$
35	21 34	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)$$
36	25 35	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)$$
37	36	abbidv	$$⊢\left(s=S\wedge t=T\right)\to \left\{f|\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\}=\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\}$$
38	12 37	eqtrid	$$⊢\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\}$$
39	5 18 38	elovmpo	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\wedge 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	2	fvexi	$$⊢Y\in \mathrm{V}$$
42		fex2	$$⊢\left(F:X⟶Y\wedge X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to F\in \mathrm{V}$$
43	40 41 42	mp3an23	$$⊢F:X⟶Y\to F\in \mathrm{V}$$
44	43	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}$$
45		feq1	$$⊢f=F\to \left(f:X⟶Y\leftrightarrow F:X⟶Y\right)$$
46		fveq1	$$⊢f=F\to f\left(u\underset{\dot{}}{+}v\right)=F\left(u\underset{\dot{}}{+}v\right)$$
47		fveq1	$$⊢f=F\to f\left(u\right)=F\left(u\right)$$
48		fveq1	$$⊢f=F\to f\left(v\right)=F\left(v\right)$$
49	47 48	oveq12d	$$⊢f=F\to f\left(u\right)\underset{\dot{}}{⨣}f\left(v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)$$
50	46 49	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)$$
51	50	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)$$
52	45 51	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)$$
53	44 52	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)$$
54	53	3anbi3i	$$⊢\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\wedge 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)\leftrightarrow \left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\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)$$
55		df-3an	$$⊢\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\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)\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)$$
56	39 54 55	3bitri	$$⊢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)$$