Metamath Proof Explorer

Theorem isghmOLD

Description: Obsolete version of isghm as of 5-Jun-2025. (Contributed by Stefan O'Rear, 31-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses isghm.w ⊢ 𝑋 = ( Base ‘ 𝑆 )
isghm.x ⊢ 𝑌 = ( Base ‘ 𝑇 )
isghm.a ⊢ + = ( +g ‘ 𝑆 )
isghm.b ⊢ ⨣ = ( +g ‘ 𝑇 )
Assertion isghmOLD ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isghm.w ⊢ 𝑋 = ( Base ‘ 𝑆 )
2 isghm.x ⊢ 𝑌 = ( Base ‘ 𝑇 )
3 isghm.a ⊢ + = ( +g ‘ 𝑆 )
4 isghm.b ⊢ ⨣ = ( +g ‘ 𝑇 )
5 df-ghm ⊢ GrpHom = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } )
6 5 elmpocl ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) )
7 fvex ⊢ ( Base ‘ 𝑠 ) ∈ V
8 feq2 ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ) )
9 raleq ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
10 9 raleqbi1dv ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
11 8 10 anbi12d ⊢ ( 𝑤 = ( Base ‘ 𝑠 ) → ( ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ) )
12 7 11 sbcie ⊢ ( [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
13 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
14 13 1 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = 𝑋 )
15 14 feq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ) )
16 fveq2 ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = ( +g ‘ 𝑆 ) )
17 16 3 eqtr4di ⊢ ( 𝑠 = 𝑆 → ( +g ‘ 𝑠 ) = + )
18 17 oveqd ⊢ ( 𝑠 = 𝑆 → ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) = ( 𝑢 + 𝑣 ) )
19 18 fveqeq2d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
20 14 19 raleqbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
21 14 20 raleqbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) )
22 15 21 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑓 : ( Base ‘ 𝑠 ) ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝑠 ) ∀ 𝑣 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ) )
23 12 22 bitrid ⊢ ( 𝑠 = 𝑆 → ( [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ) )
24 23 abbidv ⊢ ( 𝑠 = 𝑆 → { 𝑓 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑓 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑤 ∀ 𝑣 ∈ 𝑤 ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑠 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } )
25 fveq2 ⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = ( Base ‘ 𝑇 ) )
26 25 2 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( Base ‘ 𝑡 ) = 𝑌 )
27 26 feq3d ⊢ ( 𝑡 = 𝑇 → ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ↔ 𝑓 : 𝑋 ⟶ 𝑌 ) )
28 fveq2 ⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ( +g ‘ 𝑇 ) )
29 28 4 eqtr4di ⊢ ( 𝑡 = 𝑇 → ( +g ‘ 𝑡 ) = ⨣ )
30 29 oveqd ⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) )
31 30 eqeq2d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
32 31 2ralbidv ⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) )
33 27 32 anbi12d ⊢ ( 𝑡 = 𝑇 → ( ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) ) )
34 33 abbidv ⊢ ( 𝑡 = 𝑇 → { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑣 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } )
35 1 fvexi ⊢ 𝑋 ∈ V
36 2 fvexi ⊢ 𝑌 ∈ V
37 mapex ⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → { 𝑓 ∣ 𝑓 : 𝑋 ⟶ 𝑌 } ∈ V )
38 35 36 37 mp2an ⊢ { 𝑓 ∣ 𝑓 : 𝑋 ⟶ 𝑌 } ∈ V
39 simpl ⊢ ( ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) → 𝑓 : 𝑋 ⟶ 𝑌 )
40 39 ss2abi ⊢ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ⊆ { 𝑓 ∣ 𝑓 : 𝑋 ⟶ 𝑌 }
41 38 40 ssexi ⊢ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ∈ V
42 24 34 5 41 ovmpo ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } )
43 42 eleq2d ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ) )
44 fex ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ∈ V ) → 𝐹 ∈ V )
45 35 44 mpan2 ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 ∈ V )
46 45 adantr ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) → 𝐹 ∈ V )
47 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑋 ⟶ 𝑌 ↔ 𝐹 : 𝑋 ⟶ 𝑌 ) )
48 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) )
49 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑢 ) )
50 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
51 49 50 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) )
52 48 51 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
53 52 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
54 47 53 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
55 46 54 elab3 ⊢ ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝑓 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ⨣ ( 𝑓 ‘ 𝑣 ) ) ) } ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) )
56 43 55 bitrdi ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )
57 6 56 biadanii ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑋 ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) ⨣ ( 𝐹 ‘ 𝑣 ) ) ) ) )