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 
|- 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 feq2d 
 |-  ( s = S -> ( f : ( Base ` s ) --> ( Base ` t ) <-> f : X --> ( Base ` t ) ) )
16 fveq2 
 |-  ( s = S -> ( +g ` s ) = ( +g ` S ) )
17 16 3 eqtr4di 
 |-  ( s = S -> ( +g ` s ) = .+ )
18 17 oveqd 
 |-  ( s = S -> ( u ( +g ` s ) v ) = ( u .+ v ) )
19 18 fveqeq2d 
 |-  ( s = S -> ( ( f ` ( u ( +g ` s ) v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> ( f ` ( u .+ v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) )
20 14 19 raleqbidv 
 |-  ( s = S -> ( 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 ) ( +g ` t ) ( f ` v ) ) ) )
21 14 20 raleqbidv 
 |-  ( s = S -> ( 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 ) ( +g ` t ) ( f ` v ) ) ) )
22 15 21 anbi12d 
 |-  ( s = S -> ( ( 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 --> ( Base ` t ) /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) ) )
23 12 22 syl5bb 
 |-  ( s = S -> ( [. ( 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 --> ( Base ` t ) /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) ) )
24 23 abbidv 
 |-  ( s = S -> { 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 --> ( Base ` t ) /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) ) } )
25 fveq2 
 |-  ( t = T -> ( Base ` t ) = ( Base ` T ) )
26 25 2 eqtr4di 
 |-  ( t = T -> ( Base ` t ) = Y )
27 26 feq3d 
 |-  ( t = T -> ( f : X --> ( Base ` t ) <-> f : X --> Y ) )
28 fveq2 
 |-  ( t = T -> ( +g ` t ) = ( +g ` T ) )
29 28 4 eqtr4di 
 |-  ( t = T -> ( +g ` t ) = .+^ )
30 29 oveqd 
 |-  ( t = T -> ( ( f ` u ) ( +g ` t ) ( f ` v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) )
31 30 eqeq2d 
 |-  ( t = T -> ( ( f ` ( u .+ v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) )
32 31 2ralbidv 
 |-  ( t = T -> ( A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) ( +g ` t ) ( f ` v ) ) <-> A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) )
33 27 32 anbi12d 
 |-  ( t = T -> ( ( f : X --> ( Base ` t ) /\ A. u e. X A. v e. X ( f ` ( u .+ 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 ) ) ) ) )
34 33 abbidv 
 |-  ( t = T -> { f | ( f : X --> ( Base ` t ) /\ A. u e. X A. v e. X ( f ` ( u .+ 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 ) ) ) } )
35 1 fvexi 
 |-  X e. _V
36 2 fvexi 
 |-  Y e. _V
37 mapex 
 |-  ( ( X e. _V /\ Y e. _V ) -> { f | f : X --> Y } e. _V )
38 35 36 37 mp2an 
 |-  { f | f : X --> Y } e. _V
39 simpl 
 |-  ( ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) -> f : X --> Y )
40 39 ss2abi 
 |-  { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } C_ { f | f : X --> Y }
41 38 40 ssexi 
 |-  { f | ( f : X --> Y /\ A. u e. X A. v e. X ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) ) } e. _V
42 24 34 5 41 ovmpo 
 |-  ( ( 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 ) ) ) } )
43 42 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 ) ) ) } ) )
44 fex 
 |-  ( ( F : X --> Y /\ X e. _V ) -> F e. _V )
45 35 44 mpan2 
 |-  ( F : X --> Y -> F e. _V )
46 45 adantr 
 |-  ( ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) -> F e. _V )
47 feq1 
 |-  ( f = F -> ( f : X --> Y <-> F : X --> Y ) )
48 fveq1 
 |-  ( f = F -> ( f ` ( u .+ v ) ) = ( F ` ( u .+ v ) ) )
49 fveq1 
 |-  ( f = F -> ( f ` u ) = ( F ` u ) )
50 fveq1 
 |-  ( f = F -> ( f ` v ) = ( F ` v ) )
51 49 50 oveq12d 
 |-  ( f = F -> ( ( f ` u ) .+^ ( f ` v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) )
52 48 51 eqeq12d 
 |-  ( f = F -> ( ( f ` ( u .+ v ) ) = ( ( f ` u ) .+^ ( f ` v ) ) <-> ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) )
53 52 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 ) ) ) )
54 47 53 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 ) ) ) ) )
55 46 54 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 ) ) ) )
56 43 55 syl6bb 
 |-  ( ( 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 ) ) ) ) )
57 6 56 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 ) ) ) ) )