Metamath Proof Explorer

Theorem ghmeql

Description: The equalizer of two group homomorphisms is a subgroup. (Contributed by Stefan O'Rear, 7-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion ghmeql 
|- ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> dom ( F i^i G ) e. ( SubGrp ` S ) )

Proof

Step Hyp Ref Expression
1 ghmmhm 
 |-  ( F e. ( S GrpHom T ) -> F e. ( S MndHom T ) )
2 ghmmhm 
 |-  ( G e. ( S GrpHom T ) -> G e. ( S MndHom T ) )
3 mhmeql 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> dom ( F i^i G ) e. ( SubMnd ` S ) )
4 1 2 3 syl2an 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> dom ( F i^i G ) e. ( SubMnd ` S ) )
5 fveq2 
 |-  ( y = ( ( invg ` S ) ` x ) -> ( F ` y ) = ( F ` ( ( invg ` S ) ` x ) ) )
6 fveq2 
 |-  ( y = ( ( invg ` S ) ` x ) -> ( G ` y ) = ( G ` ( ( invg ` S ) ` x ) ) )
7 5 6 eqeq12d 
 |-  ( y = ( ( invg ` S ) ` x ) -> ( ( F ` y ) = ( G ` y ) <-> ( F ` ( ( invg ` S ) ` x ) ) = ( G ` ( ( invg ` S ) ` x ) ) ) )
8 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
9 8 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> S e. Grp )
10 9 adantr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> S e. Grp )
11 simprl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> x e. ( Base ` S ) )
12 eqid 
 |-  ( Base ` S ) = ( Base ` S )
13 eqid 
 |-  ( invg ` S ) = ( invg ` S )
14 12 13 grpinvcl 
 |-  ( ( S e. Grp /\ x e. ( Base ` S ) ) -> ( ( invg ` S ) ` x ) e. ( Base ` S ) )
15 10 11 14 syl2anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> ( ( invg ` S ) ` x ) e. ( Base ` S ) )
16 simprr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> ( F ` x ) = ( G ` x ) )
17 16 fveq2d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> ( ( invg ` T ) ` ( F ` x ) ) = ( ( invg ` T ) ` ( G ` x ) ) )
18 eqid 
 |-  ( invg ` T ) = ( invg ` T )
19 12 13 18 ghminv 
 |-  ( ( F e. ( S GrpHom T ) /\ x e. ( Base ` S ) ) -> ( F ` ( ( invg ` S ) ` x ) ) = ( ( invg ` T ) ` ( F ` x ) ) )
20 19 ad2ant2r 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> ( F ` ( ( invg ` S ) ` x ) ) = ( ( invg ` T ) ` ( F ` x ) ) )
21 12 13 18 ghminv 
 |-  ( ( G e. ( S GrpHom T ) /\ x e. ( Base ` S ) ) -> ( G ` ( ( invg ` S ) ` x ) ) = ( ( invg ` T ) ` ( G ` x ) ) )
22 21 ad2ant2lr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> ( G ` ( ( invg ` S ) ` x ) ) = ( ( invg ` T ) ` ( G ` x ) ) )
23 17 20 22 3eqtr4d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> ( F ` ( ( invg ` S ) ` x ) ) = ( G ` ( ( invg ` S ) ` x ) ) )
24 7 15 23 elrabd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } )
25 24 expr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) /\ x e. ( Base ` S ) ) -> ( ( F ` x ) = ( G ` x ) -> ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ) )
26 25 ralrimiva 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> A. x e. ( Base ` S ) ( ( F ` x ) = ( G ` x ) -> ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ) )
27 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
28 fveq2 
 |-  ( y = x -> ( G ` y ) = ( G ` x ) )
29 27 28 eqeq12d 
 |-  ( y = x -> ( ( F ` y ) = ( G ` y ) <-> ( F ` x ) = ( G ` x ) ) )
30 29 ralrab 
 |-  ( A. x e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } <-> A. x e. ( Base ` S ) ( ( F ` x ) = ( G ` x ) -> ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ) )
31 26 30 sylibr 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> A. x e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } )
32 eqid 
 |-  ( Base ` T ) = ( Base ` T )
33 12 32 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
34 33 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
35 34 ffnd 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> F Fn ( Base ` S ) )
36 12 32 ghmf 
 |-  ( G e. ( S GrpHom T ) -> G : ( Base ` S ) --> ( Base ` T ) )
37 36 adantl 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> G : ( Base ` S ) --> ( Base ` T ) )
38 37 ffnd 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> G Fn ( Base ` S ) )
39 fndmin 
 |-  ( ( F Fn ( Base ` S ) /\ G Fn ( Base ` S ) ) -> dom ( F i^i G ) = { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } )
40 35 38 39 syl2anc 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> dom ( F i^i G ) = { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } )
41 eleq2 
 |-  ( dom ( F i^i G ) = { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } -> ( ( ( invg ` S ) ` x ) e. dom ( F i^i G ) <-> ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ) )
42 41 raleqbi1dv 
 |-  ( dom ( F i^i G ) = { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } -> ( A. x e. dom ( F i^i G ) ( ( invg ` S ) ` x ) e. dom ( F i^i G ) <-> A. x e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ) )
43 40 42 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> ( A. x e. dom ( F i^i G ) ( ( invg ` S ) ` x ) e. dom ( F i^i G ) <-> A. x e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ( ( invg ` S ) ` x ) e. { y e. ( Base ` S ) | ( F ` y ) = ( G ` y ) } ) )
44 31 43 mpbird 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> A. x e. dom ( F i^i G ) ( ( invg ` S ) ` x ) e. dom ( F i^i G ) )
45 13 issubg3 
 |-  ( S e. Grp -> ( dom ( F i^i G ) e. ( SubGrp ` S ) <-> ( dom ( F i^i G ) e. ( SubMnd ` S ) /\ A. x e. dom ( F i^i G ) ( ( invg ` S ) ` x ) e. dom ( F i^i G ) ) ) )
46 9 45 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> ( dom ( F i^i G ) e. ( SubGrp ` S ) <-> ( dom ( F i^i G ) e. ( SubMnd ` S ) /\ A. x e. dom ( F i^i G ) ( ( invg ` S ) ` x ) e. dom ( F i^i G ) ) ) )
47 4 44 46 mpbir2and 
 |-  ( ( F e. ( S GrpHom T ) /\ G e. ( S GrpHom T ) ) -> dom ( F i^i G ) e. ( SubGrp ` S ) )