Metamath Proof Explorer

Theorem isghm

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

Ref Expression
Hypotheses isghm.w âŠĒ 𝑋 = ( Base ‘ 𝑆 )
isghm.x âŠĒ 𝑌 = ( Base ‘ 𝑇 )
isghm.a âŠĒ + = ( +g ‘ 𝑆 )
isghm.b âŠĒ âĻĢ = ( +g ‘ 𝑇 )
Assertion isghm ( ðđ ∈ ( 𝑆 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 ) ∧ ( ðđ : 𝑋 âŸķ 𝑌 ∧ ∀ ð‘Ē ∈ 𝑋 ∀ ð‘Ģ ∈ 𝑋 ( ðđ ‘ ( ð‘Ē + ð‘Ģ ) ) = ( ( ðđ ‘ ð‘Ē ) âĻĢ ( ðđ ‘ ð‘Ģ ) ) ) ) )