Metamath Proof Explorer

Theorem cntzmhm

Description: Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cntzmhm.z 
|- Z = ( Cntz ` G )
cntzmhm.y 
|- Y = ( Cntz ` H )
Assertion cntzmhm 
|- ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( F ` A ) e. ( Y ` ( F " S ) ) )

Proof

Step Hyp Ref Expression
1 cntzmhm.z 
 |-  Z = ( Cntz ` G )
2 cntzmhm.y 
 |-  Y = ( Cntz ` H )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 3 4 mhmf 
 |-  ( F e. ( G MndHom H ) -> F : ( Base ` G ) --> ( Base ` H ) )
6 3 1 cntzssv 
 |-  ( Z ` S ) C_ ( Base ` G )
7 6 sseli 
 |-  ( A e. ( Z ` S ) -> A e. ( Base ` G ) )
8 ffvelrn 
 |-  ( ( F : ( Base ` G ) --> ( Base ` H ) /\ A e. ( Base ` G ) ) -> ( F ` A ) e. ( Base ` H ) )
9 5 7 8 syl2an 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( F ` A ) e. ( Base ` H ) )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 10 1 cntzi 
 |-  ( ( A e. ( Z ` S ) /\ x e. S ) -> ( A ( +g ` G ) x ) = ( x ( +g ` G ) A ) )
12 11 adantll 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> ( A ( +g ` G ) x ) = ( x ( +g ` G ) A ) )
13 12 fveq2d 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> ( F ` ( A ( +g ` G ) x ) ) = ( F ` ( x ( +g ` G ) A ) ) )
14 simpll 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> F e. ( G MndHom H ) )
15 7 ad2antlr 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> A e. ( Base ` G ) )
16 3 1 cntzrcl 
 |-  ( A e. ( Z ` S ) -> ( G e. _V /\ S C_ ( Base ` G ) ) )
17 16 adantl 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( G e. _V /\ S C_ ( Base ` G ) ) )
18 17 simprd 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> S C_ ( Base ` G ) )
19 18 sselda 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> x e. ( Base ` G ) )
20 eqid 
 |-  ( +g ` H ) = ( +g ` H )
21 3 10 20 mhmlin 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Base ` G ) /\ x e. ( Base ` G ) ) -> ( F ` ( A ( +g ` G ) x ) ) = ( ( F ` A ) ( +g ` H ) ( F ` x ) ) )
22 14 15 19 21 syl3anc 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> ( F ` ( A ( +g ` G ) x ) ) = ( ( F ` A ) ( +g ` H ) ( F ` x ) ) )
23 3 10 20 mhmlin 
 |-  ( ( F e. ( G MndHom H ) /\ x e. ( Base ` G ) /\ A e. ( Base ` G ) ) -> ( F ` ( x ( +g ` G ) A ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) )
24 14 19 15 23 syl3anc 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> ( F ` ( x ( +g ` G ) A ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) )
25 13 22 24 3eqtr3d 
 |-  ( ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) /\ x e. S ) -> ( ( F ` A ) ( +g ` H ) ( F ` x ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) )
26 25 ralrimiva 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> A. x e. S ( ( F ` A ) ( +g ` H ) ( F ` x ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) )
27 5 adantr 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> F : ( Base ` G ) --> ( Base ` H ) )
28 27 ffnd 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> F Fn ( Base ` G ) )
29 oveq2 
 |-  ( y = ( F ` x ) -> ( ( F ` A ) ( +g ` H ) y ) = ( ( F ` A ) ( +g ` H ) ( F ` x ) ) )
30 oveq1 
 |-  ( y = ( F ` x ) -> ( y ( +g ` H ) ( F ` A ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) )
31 29 30 eqeq12d 
 |-  ( y = ( F ` x ) -> ( ( ( F ` A ) ( +g ` H ) y ) = ( y ( +g ` H ) ( F ` A ) ) <-> ( ( F ` A ) ( +g ` H ) ( F ` x ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) ) )
32 31 ralima 
 |-  ( ( F Fn ( Base ` G ) /\ S C_ ( Base ` G ) ) -> ( A. y e. ( F " S ) ( ( F ` A ) ( +g ` H ) y ) = ( y ( +g ` H ) ( F ` A ) ) <-> A. x e. S ( ( F ` A ) ( +g ` H ) ( F ` x ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) ) )
33 28 18 32 syl2anc 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( A. y e. ( F " S ) ( ( F ` A ) ( +g ` H ) y ) = ( y ( +g ` H ) ( F ` A ) ) <-> A. x e. S ( ( F ` A ) ( +g ` H ) ( F ` x ) ) = ( ( F ` x ) ( +g ` H ) ( F ` A ) ) ) )
34 26 33 mpbird 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> A. y e. ( F " S ) ( ( F ` A ) ( +g ` H ) y ) = ( y ( +g ` H ) ( F ` A ) ) )
35 imassrn 
 |-  ( F " S ) C_ ran F
36 27 frnd 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ran F C_ ( Base ` H ) )
37 35 36 sstrid 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( F " S ) C_ ( Base ` H ) )
38 4 20 2 elcntz 
 |-  ( ( F " S ) C_ ( Base ` H ) -> ( ( F ` A ) e. ( Y ` ( F " S ) ) <-> ( ( F ` A ) e. ( Base ` H ) /\ A. y e. ( F " S ) ( ( F ` A ) ( +g ` H ) y ) = ( y ( +g ` H ) ( F ` A ) ) ) ) )
39 37 38 syl 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( ( F ` A ) e. ( Y ` ( F " S ) ) <-> ( ( F ` A ) e. ( Base ` H ) /\ A. y e. ( F " S ) ( ( F ` A ) ( +g ` H ) y ) = ( y ( +g ` H ) ( F ` A ) ) ) ) )
40 9 34 39 mpbir2and 
 |-  ( ( F e. ( G MndHom H ) /\ A e. ( Z ` S ) ) -> ( F ` A ) e. ( Y ` ( F " S ) ) )