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 \in (G MndHom H) \land S \subseteq Z (T)) \to F [S] \subseteq 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 \in (G MndHom H) \land x \in Z (T)) \to F (x) \in Y (F [T])$
4	3	ralrimiva	$⊢ F \in (G MndHom H) \to \forall x \in Z (T) F (x) \in Y (F [T])$
5		ssralv	$⊢ S \subseteq Z (T) \to (\forall x \in Z (T) F (x) \in Y (F [T]) \to \forall x \in S F (x) \in Y (F [T]))$
6	4 5	mpan9	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to \forall x \in S F (x) \in Y (F [T])$
7		eqid	$⊢ {Base}_{G} = {Base}_{G}$
8		eqid	$⊢ {Base}_{H} = {Base}_{H}$
9	7 8	mhmf	$⊢ F \in (G MndHom H) \to F : {Base}_{G} ⟶ {Base}_{H}$
10	9	adantr	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to F : {Base}_{G} ⟶ {Base}_{H}$
11	10	ffund	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to Fun F$
12		simpr	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to S \subseteq Z (T)$
13	7 1	cntzssv	$⊢ Z (T) \subseteq {Base}_{G}$
14	12 13	sstrdi	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to S \subseteq {Base}_{G}$
15	10	fdmd	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to dom F = {Base}_{G}$
16	14 15	sseqtrrd	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to S \subseteq dom F$
17		funimass4	$⊢ (Fun F \land S \subseteq dom F) \to (F [S] \subseteq Y (F [T]) \leftrightarrow \forall x \in S F (x) \in Y (F [T]))$
18	11 16 17	syl2anc	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to (F [S] \subseteq Y (F [T]) \leftrightarrow \forall x \in S F (x) \in Y (F [T]))$
19	6 18	mpbird	$⊢ (F \in (G MndHom H) \land S \subseteq Z (T)) \to F [S] \subseteq Y (F [T])$