Metamath Proof Explorer

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 = ( Base ` S )
isghm.x 
|- Y = ( Base ` T )
isghm.a 
|- .+ = ( +g ` S )
isghm.b 
|- .+^ = ( +g ` T )
Assertion isghm 
|- ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isghm.w 
 |-  X = ( Base ` S )
2 isghm.x 
 |-  Y = ( Base ` T )
3 isghm.a 
 |-  .+ = ( +g ` S )
4 isghm.b 
 |-  .+^ = ( +g ` T )
5 df-ghm 
 |-  GrpHom = ( s e. Grp , t e. Grp |-> { f | [. ( Base ` s ) / w ]. ( f : w --> ( Base ` t ) /\ A. u e. w A. v e. w ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) } )
6 5 elmpocl 
 |-  ( F e. ( S GrpHom T ) -> ( S e. Grp /\ T e. Grp ) )
7 fvex 
 |-  ( Base ` s ) e. _V
8 feq2 
 |-  ( w = ( Base ` s ) -> ( f : w --> ( Base ` t ) <-> f : ( Base ` s ) --> ( Base ` t ) ) )
9 raleq 
 |-  ( w = ( Base ` s ) -> ( A. v e. w ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> A. v e. ( Base ` s ) ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) )
10 9 raleqbi1dv 
 |-  ( w = ( Base ` s ) -> ( A. u e. w A. v e. w ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> A. u e. ( Base ` s ) A. v e. ( Base ` s ) ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) )
11 8 10 anbi12d 
 |-  ( w = ( Base ` s ) -> ( ( f : w --> ( Base ` t ) /\ A. u e. w A. v e. w ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) <-> ( f : ( Base ` s ) --> ( Base ` t ) /\ A. u e. ( Base ` s ) A. v e. ( Base ` s ) ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) ) )
12 7 11 sbcie 
 |-  ( [. ( Base ` s ) / w ]. ( f : w --> ( Base ` t ) /\ A. u e. w A. v e. w ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) <-> ( f : ( Base ` s ) --> ( Base ` t ) /\ A. u e. ( Base ` s ) A. v e. ( Base ` s ) ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) )
13 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
14 13 1 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = X )
15 14 adantr 
 |-  ( ( s = S /\ t = T ) -> ( Base ` s ) = X )
16 fveq2 
 |-  ( t = T -> ( Base ` t ) = ( Base ` T ) )
17 16 2 eqtr4di 
 |-  ( t = T -> ( Base ` t ) = Y )
18 17 adantl 
 |-  ( ( s = S /\ t = T ) -> ( Base ` t ) = Y )
19 15 18 feq23d 
 |-  ( ( s = S /\ t = T ) -> ( f : ( Base ` s ) --> ( Base ` t ) <-> f : X --> Y ) )
20 fveq2 
 |-  ( s = S -> ( +g ` s ) = ( +g ` S ) )
21 20 3 eqtr4di 
 |-  ( s = S -> ( +g ` s ) = .+ )
22 21 oveqd 
 |-  ( s = S -> ( u ( +g ` s ) v ) = ( u .+ v ) )
23 22 fveq2d 
 |-  ( s = S -> ( f ` ( u ( +g ` s ) v ) ) = ( f ` ( u .+ v ) ) )
24 fveq2 
 |-  ( t = T -> ( +g ` t ) = ( +g ` T ) )
25 24 4 eqtr4di 
 |-  ( t = T -> ( +g ` t ) = .+^ )
26 25 oveqd 
 |-  ( t = T -> ( ( f ` u ) ( +g ` t ) ( f ` v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) )
27 23 26 eqeqan12d 
 |-  ( ( s = S /\ t = T ) -> ( ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) )
28 15 27 raleqbidv 
 |-  ( ( s = S /\ t = T ) -> ( A. v e. ( Base ` s ) ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) )
29 15 28 raleqbidv 
 |-  ( ( s = S /\ t = T ) -> ( A. u e. ( Base ` s ) A. v e. ( Base ` s ) ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) )
30 19 29 anbi12d 
 |-  ( ( s = S /\ t = T ) -> ( ( f : ( Base ` s ) --> ( Base ` t ) /\ A. u e. ( Base ` s ) A. v e. ( Base ` s ) ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) <-> ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) ) )
31 12 30 bitrid 
 |-  ( ( s = S /\ t = T ) -> ( [. ( Base ` s ) / w ]. ( f : w --> ( Base ` t ) /\ A. u e. w A. v e. w ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) <-> ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) ) )
32 31 abbidv 
 |-  ( ( s = S /\ t = T ) -> { f | [. ( Base ` s ) / w ]. ( f : w --> ( Base ` t ) /\ A. u e. w A. v e. w ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) } = { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } )
33 2 fvexi 
 |-  Y e. _V
34 fsetex 
 |-  ( Y e. _V -> { f | f : X --> Y } e. _V )
35 33 34 ax-mp 
 |-  { f | f : X --> Y } e. _V
36 abanssl 
 |-  { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } C_ { f | f : X --> Y }
37 35 36 ssexi 
 |-  { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } e. _V
38 32 5 37 ovmpoa 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } )
39 38 eleq2d 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( F e. ( S GrpHom T ) <-> F e. { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } ) )
40 1 fvexi 
 |-  X e. _V
41 fex2 
 |-  ( ( F : X --> Y /\ X e. _V /\ Y e. _V ) -> F e. _V )
42 40 33 41 mp3an23 
 |-  ( F : X --> Y -> F e. _V )
43 42 adantr 
 |-  ( ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) -> F e. _V )
44 feq1 
 |-  ( f = F -> ( f : X --> Y <-> F : X --> Y ) )
45 fveq1 
 |-  ( f = F -> ( f ` ( u .+ v ) ) = ( F ` ( u .+ v ) ) )
46 fveq1 
 |-  ( f = F -> ( f ` u ) = ( F ` u ) )
47 fveq1 
 |-  ( f = F -> ( f ` v ) = ( F ` v ) )
48 46 47 oveq12d 
 |-  ( f = F -> ( ( f ` u ) .+^ ( f ` v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) )
49 45 48 eqeq12d 
 |-  ( f = F -> ( ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) <-> ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) )
50 49 2ralbidv 
 |-  ( f = F -> ( A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) <-> A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) )
51 44 50 anbi12d 
 |-  ( f = F -> ( ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) <-> ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )
52 43 51 elab3 
 |-  ( F e. { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } <-> ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) )
53 39 52 bitrdi 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( F e. ( S GrpHom T ) <-> ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )
54 6 53 biadanii 
 |-  ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )