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	⊢ 𝑋 = ( Base ‘ 𝑆 )
	sn-isghm.x	⊢ 𝑌 = ( Base ‘ 𝑇 )
	sn-isghm.a	⊢ + = ( +g ‘ 𝑆 )
	sn-isghm.b	⊢ ⨣ = ( +g ‘ 𝑇 )
Assertion	sn-isghm	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sn-isghm.w	⊢ 𝑋 = ( Base ‘ 𝑆 )
2		sn-isghm.x	⊢ 𝑌 = ( Base ‘ 𝑇 )
3		sn-isghm.a	⊢ + = ( +g ‘ 𝑆 )
4		sn-isghm.b	⊢ ⨣ = ( +g ‘ 𝑇 )
5		df-ghm	⊢ GrpHom = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } )
6		fvex	⊢ ( Base ‘ 𝑠 ) ∈ V
7		feq2	⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ) )
8		raleq	⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
9	8	raleqbi1dv	⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
10	7 9	anbi12d	⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ) )
11	6 10	sbcie	⊢ ( [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
12	11	abbii	⊢ { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) }
13		fvex	⊢ ( Base ‘ 𝑡 ) ∈ V
14		fsetex	⊢ ( ( Base ‘ 𝑡 ) ∈ V → { 𝑓 ∣ 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) } ∈ V )
15	13 14	ax-mp	⊢ { 𝑓 ∣ 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) } ∈ V
16		abanssl	⊢ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } ⊆ { 𝑓 ∣ 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) }
17	15 16	ssexi	⊢ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } ∈ V
18	12 17	eqeltri	⊢ { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } ∈ V
19		fveq2	⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
20	19 1	eqtr4di	⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝑋 )
21	20	adantr	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑠 ) = 𝑋 )
22		fveq2	⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = ( Base ‘ 𝑇 ) )
23	22 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = 𝑌 )
24	23	adantl	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( Base ‘ 𝑡 ) = 𝑌 )
25	21 24	feq23d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
26		fveq2	⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = ( +g ‘ 𝑆 ) )
27	26 3	eqtr4di	⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = + )
28	27	oveqd	⊢ ( 𝑠 = 𝑆 → ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) = ( 𝑢 + 𝑣 ) )
29	28	fveq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) )
30		fveq2	⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ( +g ‘ 𝑇 ) )
31	30 4	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ⨣ )
32	31	oveqd	⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) )
33	29 32	eqeqan12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
34	21 33	raleqbidv	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
35	21 34	raleqbidv	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
36	25 35	anbi12d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) ) )
37	36	abbidv	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } )
38	12 37	eqtrid	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } )
39	5 18 38	elovmpo	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ) )
40	1	fvexi	⊢ 𝑋 ∈ V
41	2	fvexi	⊢ 𝑌 ∈ V
42		fex2	⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) → 𝐹 ∈ V )
43	40 41 42	mp3an23	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 ∈ V )
44	43	adantr	⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) → 𝐹 ∈ V )
45		feq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑋 ⟶ 𝑌 ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
46		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) )
47		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
48		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
49	47 48	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) )
50	46 49	eqeq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
51	50	2ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
52	45 51	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
53	44 52	elab3	⊢ ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
54	53	3anbi3i	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ) ↔ ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
55		df-3an	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
56	39 54 55	3bitri	⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )