Metamath Proof Explorer

Theorem mgmhmeql

Description: The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020)

Ref Expression
Assertion mgmhmeql 
|- ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> dom ( F i^i G ) e. ( SubMgm ` S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` S ) = ( Base ` S )
2 eqid 
 |-  ( Base ` T ) = ( Base ` T )
3 1 2 mgmhmf 
 |-  ( F e. ( S MgmHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
4 3 adantr 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
5 4 ffnd 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> F Fn ( Base ` S ) )
6 1 2 mgmhmf 
 |-  ( G e. ( S MgmHom T ) -> G : ( Base ` S ) --> ( Base ` T ) )
7 6 adantl 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> G : ( Base ` S ) --> ( Base ` T ) )
8 7 ffnd 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 MgmHom T ) /\ G e. ( S MgmHom 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 MgmHom T ) /\ G e. ( S MgmHom T ) ) -> { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } C_ ( Base ` S ) )
13 mgmhmrcl 
 |-  ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )
14 13 simpld 
 |-  ( F e. ( S MgmHom T ) -> S e. Mgm )
15 14 adantr 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> S e. Mgm )
16 15 ad2antrr 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> S e. Mgm )
17 simplrl 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> x e. ( Base ` S ) )
18 simprl 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> y e. ( Base ` S ) )
19 eqid 
 |-  ( +g ` S ) = ( +g ` S )
20 1 19 mgmcl 
 |-  ( ( S e. Mgm /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
21 16 17 18 20 syl3anc 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
22 simplrr 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` x ) = ( G ` x ) )
23 simprr 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> ( F ` y ) = ( G ` y ) )
24 22 23 oveq12d 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) ) )
25 simplll 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> F e. ( S MgmHom T ) )
26 eqid 
 |-  ( +g ` T ) = ( +g ` T )
27 1 19 26 mgmhmlin 
 |-  ( ( F e. ( S MgmHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
28 25 17 18 27 syl3anc 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) ) )
29 simpllr 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ ( F ` x ) = ( G ` x ) ) ) /\ ( y e. ( Base ` S ) /\ ( F ` y ) = ( G ` y ) ) ) -> G e. ( S MgmHom T ) )
30 1 19 26 mgmhmlin 
 |-  ( ( G e. ( S MgmHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( G ` ( x ( +g ` S ) y ) ) = ( ( G ` x ) ( +g ` T ) ( G ` y ) ) )
31 29 17 18 30 syl3anc 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) ) )
32 24 28 31 3eqtr4d 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) ) )
33 fveq2 
 |-  ( z = ( x ( +g ` S ) y ) -> ( F ` z ) = ( F ` ( x ( +g ` S ) y ) ) )
34 fveq2 
 |-  ( z = ( x ( +g ` S ) y ) -> ( G ` z ) = ( G ` ( x ( +g ` S ) y ) ) )
35 33 34 eqeq12d 
 |-  ( z = ( x ( +g ` S ) y ) -> ( ( F ` z ) = ( G ` z ) <-> ( F ` ( x ( +g ` S ) y ) ) = ( G ` ( x ( +g ` S ) y ) ) ) )
36 35 elrab 
 |-  ( ( x ( +g ` S ) y ) e. { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } <-> ( ( x ( +g ` S ) y ) e. ( Base ` S ) /\ ( F ` ( x ( +g ` S ) y ) ) = ( G ` ( x ( +g ` S ) y ) ) ) )
37 21 32 36 sylanbrc 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) } )
38 37 expr 
 |-  ( ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) } ) )
39 38 ralrimiva 
 |-  ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) } ) )
40 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
41 fveq2 
 |-  ( z = y -> ( G ` z ) = ( G ` y ) )
42 40 41 eqeq12d 
 |-  ( z = y -> ( ( F ` z ) = ( G ` z ) <-> ( F ` y ) = ( G ` y ) ) )
43 42 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 ) } ) )
44 39 43 sylibr 
 |-  ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) } )
45 44 expr 
 |-  ( ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) } ) )
46 45 ralrimiva 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) } ) )
47 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
48 fveq2 
 |-  ( z = x -> ( G ` z ) = ( G ` x ) )
49 47 48 eqeq12d 
 |-  ( z = x -> ( ( F ` z ) = ( G ` z ) <-> ( F ` x ) = ( G ` x ) ) )
50 49 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 ) } ) )
51 46 50 sylibr 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom 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 ) } )
52 1 19 issubmgm 
 |-  ( S e. Mgm -> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } e. ( SubMgm ` S ) <-> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } C_ ( Base ` S ) /\ 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 ) } ) ) )
53 15 52 syl 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } e. ( SubMgm ` S ) <-> ( { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } C_ ( Base ` S ) /\ 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 ) } ) ) )
54 12 51 53 mpbir2and 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> { z e. ( Base ` S ) | ( F ` z ) = ( G ` z ) } e. ( SubMgm ` S ) )
55 10 54 eqeltrd 
 |-  ( ( F e. ( S MgmHom T ) /\ G e. ( S MgmHom T ) ) -> dom ( F i^i G ) e. ( SubMgm ` S ) )