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 𝐻 ) ∧ 𝑆 ⊆ ( 𝑍 ‘ 𝑇 ) ) → ( 𝐹 “ 𝑆 ) ⊆ ( 𝑌 ‘ ( 𝐹 “ 𝑇 ) ) )