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 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 ) ) ) ) )
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 ) ) ) ) )