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 ) ) )