Metamath Proof Explorer

Theorem cntzmhm2

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 cntzmhm2 
|- ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> ( F " S ) C_ ( Y ` ( F " T ) ) )

Proof

Step Hyp Ref Expression
1 cntzmhm.z 
 |-  Z = ( Cntz ` G )
2 cntzmhm.y 
 |-  Y = ( Cntz ` H )
3 1 2 cntzmhm 
 |-  ( ( F e. ( G MndHom H ) /\ x e. ( Z ` T ) ) -> ( F ` x ) e. ( Y ` ( F " T ) ) )
4 3 ralrimiva 
 |-  ( F e. ( G MndHom H ) -> A. x e. ( Z ` T ) ( F ` x ) e. ( Y ` ( F " T ) ) )
5 ssralv 
 |-  ( S C_ ( Z ` T ) -> ( A. x e. ( Z ` T ) ( F ` x ) e. ( Y ` ( F " T ) ) -> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) ) )
6 4 5 mpan9 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 eqid 
 |-  ( Base ` H ) = ( Base ` H )
9 7 8 mhmf 
 |-  ( F e. ( G MndHom H ) -> F : ( Base ` G ) --> ( Base ` H ) )
10 9 adantr 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> F : ( Base ` G ) --> ( Base ` H ) )
11 10 ffund 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> Fun F )
12 simpr 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> S C_ ( Z ` T ) )
13 7 1 cntzssv 
 |-  ( Z ` T ) C_ ( Base ` G )
14 12 13 sstrdi 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> S C_ ( Base ` G ) )
15 10 fdmd 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> dom F = ( Base ` G ) )
16 14 15 sseqtrrd 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> S C_ dom F )
17 funimass4 
 |-  ( ( Fun F /\ S C_ dom F ) -> ( ( F " S ) C_ ( Y ` ( F " T ) ) <-> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) ) )
18 11 16 17 syl2anc 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> ( ( F " S ) C_ ( Y ` ( F " T ) ) <-> A. x e. S ( F ` x ) e. ( Y ` ( F " T ) ) ) )
19 6 18 mpbird 
 |-  ( ( F e. ( G MndHom H ) /\ S C_ ( Z ` T ) ) -> ( F " S ) C_ ( Y ` ( F " T ) ) )