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 S GrpHom T G S GrpHom T dom F G SubGrp S

Proof

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