Metamath Proof Explorer

Theorem mhmeql

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

Ref Expression
Assertion mhmeql 
|- ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> dom ( F i^i G ) e. ( SubMnd ` S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` S ) = ( Base ` S )
2 eqid 
 |-  ( Base ` T ) = ( Base ` T )
3 1 2 mhmf 
 |-  ( F e. ( S MndHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
4 3 adantr 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
5 4 ffnd 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> F Fn ( Base ` S ) )
6 1 2 mhmf 
 |-  ( G e. ( S MndHom T ) -> G : ( Base ` S ) --> ( Base ` T ) )
7 6 adantl 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> G : ( Base ` S ) --> ( Base ` T ) )
8 7 ffnd 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> G Fn ( Base ` S ) )
9 fndmin 
 |-  ( ( F Fn ( Base ` S ) /\ G Fn ( Base ` S ) ) -> dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
10 5 8 9 syl2anc 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> dom ( F i^i G ) = { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
11 ssrab2 
 |-  { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } C_ ( Base ` S )
12 11 a1i 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } C_ ( Base ` S ) )
13 fveq2 
 |-  ( z = ( 0g ` S ) -> ( F ` z ) = ( F ` ( 0g ` S ) ) )
14 fveq2 
 |-  ( z = ( 0g ` S ) -> ( G ` z ) = ( G ` ( 0g ` S ) ) )
15 13 14 eqeq12d 
 |-  ( z = ( 0g ` S ) -> ( ( F ` z ) = ( G ` z ) <-> ( F ` ( 0g ` S ) ) = ( G ` ( 0g ` S ) ) ) )
16 mhmrcl1 
 |-  ( F e. ( S MndHom T ) -> S e. Mnd )
17 16 adantr 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> S e. Mnd )
18 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
19 1 18 mndidcl 
 |-  ( S e. Mnd -> ( 0g ` S ) e. ( Base ` S ) )
20 17 19 syl 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> ( 0g ` S ) e. ( Base ` S ) )
21 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
22 18 21 mhm0 
 |-  ( F e. ( S MndHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
23 22 adantr 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
24 18 21 mhm0 
 |-  ( G e. ( S MndHom T ) -> ( G ` ( 0g ` S ) ) = ( 0g ` T ) )
25 24 adantl 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> ( G ` ( 0g ` S ) ) = ( 0g ` T ) )
26 23 25 eqtr4d 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> ( F ` ( 0g ` S ) ) = ( G ` ( 0g ` S ) ) )
27 15 20 26 elrabd 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> ( 0g ` S ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
28 fveq2 
 |-  ( z = ( x ( +g ` S ) y ) -> ( F ` z ) = ( F ` ( x ( +g ` S ) y ) ) )
29 fveq2 
 |-  ( z = ( x ( +g ` S ) y ) -> ( G ` z ) = ( G ` ( x ( +g ` S ) y ) ) )
30 28 29 eqeq12d 
 |-  ( z = ( x ( +g ` S ) y ) -> ( ( F ` z ) = ( G ` z ) <-> ( F ` ( x ( +g ` S ) y ) ) = ( G ` ( x ( +g ` S ) y ) ) ) )
31 17 ad2antrr 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> S e. Mnd )
32 simplrl 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> x e. ( Base ` S ) )
33 simprl 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> y e. ( Base ` S ) )
34 eqid 
 |-  ( +g ` S ) = ( +g ` S )
35 1 34 mndcl 
 |-  ( ( S e. Mnd /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
36 31 32 33 35 syl3anc 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
37 simplll 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> F e. ( S MndHom T ) )
38 eqid 
 |-  ( +g ` T ) = ( +g ` T )
39 1 34 38 mhmlin 
 |-  ( ( F e. ( S MndHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
40 37 32 33 39 syl3anc 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
41 simpllr 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> G e. ( S MndHom T ) )
42 1 34 38 mhmlin 
 |-  ( ( G e. ( S MndHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( G ` ( x ( +g ` S ) y ) ) = ( ( G ` x ) ( +g ` T ) ( G ` y ) ) )
43 41 32 33 42 syl3anc 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( G ` ( x ( +g ` S ) y ) ) = ( ( G ` x ) ( +g ` T ) ( G ` y ) ) )
44 simplrr 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` x ) = ( G ` x ) )
45 simprr 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` y ) = ( G ` y ) )
46 44 45 oveq12d 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( ( F ` x ) ( +g ` T ) ( F ` y ) ) = ( ( G ` x ) ( +g ` T ) ( G ` y ) ) )
47 43 46 eqtr4d 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( G ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
48 40 47 eqtr4d 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( G ` ( x ( +g ` S ) y ) ) )
49 30 36 48 elrabd 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
50 49 expr 
 |-  ( ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` y ) = ( G ` y ) -> ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
51 50 ralrimiva 
 |-  ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> A. y e. ( Base ` S ) ( ( F ` y ) = ( G ` y ) -> ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
52 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
53 fveq2 
 |-  ( z = y -> ( G ` z ) = ( G ` y ) )
54 52 53 eqeq12d 
 |-  ( z = y -> ( ( F ` z ) = ( G ` z ) <-> ( F ` y ) = ( G ` y ) ) )
55 54 ralrab 
 |-  ( A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } <-> A. y e. ( Base ` S ) ( ( F ` y ) = ( G ` y ) -> ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
56 51 55 sylibr 
 |-  ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) -> A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
57 56 expr 
 |-  ( ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) /\ x e. ( Base ` S ) ) -> ( ( F ` x ) = ( G ` x ) -> A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
58 57 ralrimiva 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> A. x e. ( Base ` S ) ( ( F ` x ) = ( G ` x ) -> A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
59 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
60 fveq2 
 |-  ( z = x -> ( G ` z ) = ( G ` x ) )
61 59 60 eqeq12d 
 |-  ( z = x -> ( ( F ` z ) = ( G ` z ) <-> ( F ` x ) = ( G ` x ) ) )
62 61 ralrab 
 |-  ( A. x e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } <-> A. x e. ( Base ` S ) ( ( F ` x ) = ( G ` x ) -> A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) )
63 58 62 sylibr 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> A. x e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } )
64 1 18 34 issubm 
 |-  ( S e. Mnd -> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } e. ( SubMnd ` S ) <-> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } C_ ( Base ` S ) /\ ( 0g ` S ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } /\ A. x e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) ) )
65 17 64 syl 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } e. ( SubMnd ` S ) <-> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } C_ ( Base ` S ) /\ ( 0g ` S ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } /\ A. x e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } A. y e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } ) ) )
66 12 27 63 65 mpbir3and 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } e. ( SubMnd ` S ) )
67 10 66 eqeltrd 
 |-  ( ( F e. ( S MndHom T ) /\ G e. ( S MndHom T ) ) -> dom ( F i^i G ) e. ( SubMnd ` S ) )