This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
cntzmhm.y ⊢ 𝑌 = ( Cntz ‘ 𝐻 )
Assertion cntzmhm2 ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → ( 𝐹 “ 𝑆 ) ⊆ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 cntzmhm.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2 cntzmhm.y ⊢ 𝑌 = ( Cntz ‘ 𝐻 )
3 1 2 cntzmhm ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑇 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) )
4 3 ralrimiva ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑇 ) ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) )
5 ssralv ⊢ ( 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) → ( ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑇 ) ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) ) )
6 4 5 mpan9 ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
9 7 8 mhmf ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
10 9 adantr ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
11 10 ffund ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → Fun 𝐹 )
12 simpr ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) )
13 7 1 cntzssv ⊢ ( 𝑍 ‘ 𝑇 ) ⊆ ( Base ‘ 𝐺 )
14 12 13 sstrdi ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
15 10 fdmd ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → dom 𝐹 = ( Base ‘ 𝐺 ) )
16 14 15 sseqtrrd ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → 𝑆 ⊆ dom 𝐹 )
17 funimass4 ⊢ ( ( Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑆 ) ⊆ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) ) )
18 11 16 17 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → ( ( 𝐹 “ 𝑆 ) ⊆ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) ) )
19 6 18 mpbird ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → ( 𝐹 “ 𝑆 ) ⊆ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) )