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 ∈ G MndHom H ∧ S ⊆ Z ⁡ T → F S ⊆ 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 ∈ G MndHom H ∧ x ∈ Z ⁡ T → F ⁡ x ∈ Y ⁡ F T
4 3 ralrimiva ⊢ F ∈ G MndHom H → ∀ x ∈ Z ⁡ T F ⁡ x ∈ Y ⁡ F T
5 ssralv ⊢ S ⊆ Z ⁡ T → ∀ x ∈ Z ⁡ T F ⁡ x ∈ Y ⁡ F T → ∀ x ∈ S F ⁡ x ∈ Y ⁡ F T
6 4 5 mpan9 ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → ∀ x ∈ S F ⁡ x ∈ Y ⁡ F T
7 eqid ⊢ Base G = Base G
8 eqid ⊢ Base H = Base H
9 7 8 mhmf ⊢ F ∈ G MndHom H → F : Base G ⟶ Base H
10 9 adantr ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → F : Base G ⟶ Base H
11 10 ffund ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → Fun ⁡ F
12 simpr ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → S ⊆ Z ⁡ T
13 7 1 cntzssv ⊢ Z ⁡ T ⊆ Base G
14 12 13 sstrdi ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → S ⊆ Base G
15 10 fdmd ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → dom ⁡ F = Base G
16 14 15 sseqtrrd ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → S ⊆ dom ⁡ F
17 funimass4 ⊢ Fun ⁡ F ∧ S ⊆ dom ⁡ F → F S ⊆ Y ⁡ F T ↔ ∀ x ∈ S F ⁡ x ∈ Y ⁡ F T
18 11 16 17 syl2anc ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → F S ⊆ Y ⁡ F T ↔ ∀ x ∈ S F ⁡ x ∈ Y ⁡ F T
19 6 18 mpbird ⊢ F ∈ G MndHom H ∧ S ⊆ Z ⁡ T → F S ⊆ Y ⁡ F T