cntzmhm

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	cntzmhm	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to F (A) \in Y (F [S])$

Proof

Step	Hyp	Ref	Expression
1		cntzmhm.z	$⊢ Z = Cntz (G)$
2		cntzmhm.y	$⊢ Y = Cntz (H)$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4		eqid	$⊢ {Base}_{H} = {Base}_{H}$
5	3 4	mhmf	$⊢ F \in (G MndHom H) \to F : {Base}_{G} ⟶ {Base}_{H}$
6	3 1	cntzssv	$⊢ Z (S) \subseteq {Base}_{G}$
7	6	sseli	$⊢ A \in Z (S) \to A \in {Base}_{G}$
8		ffvelcdm	$⊢ (F : {Base}_{G} ⟶ {Base}_{H} \land A \in {Base}_{G}) \to F (A) \in {Base}_{H}$
9	5 7 8	syl2an	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to F (A) \in {Base}_{H}$
10		eqid	$⊢ +_{G} = +_{G}$
11	10 1	cntzi	$⊢ (A \in Z (S) \land x \in S) \to A +_{G} x = x +_{G} A$
12	11	adantll	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to A +_{G} x = x +_{G} A$
13	12	fveq2d	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to F (A +_{G} x) = F (x +_{G} A)$
14		simpll	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to F \in (G MndHom H)$
15	7	ad2antlr	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to A \in {Base}_{G}$
16	3 1	cntzrcl	$⊢ A \in Z (S) \to (G \in V \land S \subseteq {Base}_{G})$
17	16	adantl	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to (G \in V \land S \subseteq {Base}_{G})$
18	17	simprd	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to S \subseteq {Base}_{G}$
19	18	sselda	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to x \in {Base}_{G}$
20		eqid	$⊢ +_{H} = +_{H}$
21	3 10 20	mhmlin	$⊢ (F \in (G MndHom H) \land A \in {Base}_{G} \land x \in {Base}_{G}) \to F (A +_{G} x) = F (A) +_{H} F (x)$
22	14 15 19 21	syl3anc	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to F (A +_{G} x) = F (A) +_{H} F (x)$
23	3 10 20	mhmlin	$⊢ (F \in (G MndHom H) \land x \in {Base}_{G} \land A \in {Base}_{G}) \to F (x +_{G} A) = F (x) +_{H} F (A)$
24	14 19 15 23	syl3anc	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to F (x +_{G} A) = F (x) +_{H} F (A)$
25	13 22 24	3eqtr3d	$⊢ ((F \in (G MndHom H) \land A \in Z (S)) \land x \in S) \to F (A) +_{H} F (x) = F (x) +_{H} F (A)$
26	25	ralrimiva	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to \forall x \in S F (A) +_{H} F (x) = F (x) +_{H} F (A)$
27	5	adantr	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to F : {Base}_{G} ⟶ {Base}_{H}$
28	27	ffnd	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to F Fn {Base}_{G}$
29		oveq2	$⊢ y = F (x) \to F (A) +_{H} y = F (A) +_{H} F (x)$
30		oveq1	$⊢ y = F (x) \to y +_{H} F (A) = F (x) +_{H} F (A)$
31	29 30	eqeq12d	$⊢ y = F (x) \to (F (A) +_{H} y = y +_{H} F (A) \leftrightarrow F (A) +_{H} F (x) = F (x) +_{H} F (A))$
32	31	ralima	$⊢ (F Fn {Base}_{G} \land S \subseteq {Base}_{G}) \to (\forall y \in F [S] F (A) +_{H} y = y +_{H} F (A) \leftrightarrow \forall x \in S F (A) +_{H} F (x) = F (x) +_{H} F (A))$
33	28 18 32	syl2anc	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to (\forall y \in F [S] F (A) +_{H} y = y +_{H} F (A) \leftrightarrow \forall x \in S F (A) +_{H} F (x) = F (x) +_{H} F (A))$
34	26 33	mpbird	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to \forall y \in F [S] F (A) +_{H} y = y +_{H} F (A)$
35		imassrn	$⊢ F [S] \subseteq ran F$
36	27	frnd	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to ran F \subseteq {Base}_{H}$
37	35 36	sstrid	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to F [S] \subseteq {Base}_{H}$
38	4 20 2	elcntz	$⊢ F [S] \subseteq {Base}_{H} \to (F (A) \in Y (F [S]) \leftrightarrow (F (A) \in {Base}_{H} \land \forall y \in F [S] F (A) +_{H} y = y +_{H} F (A)))$
39	37 38	syl	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to (F (A) \in Y (F [S]) \leftrightarrow (F (A) \in {Base}_{H} \land \forall y \in F [S] F (A) +_{H} y = y +_{H} F (A)))$
40	9 34 39	mpbir2and	$⊢ (F \in (G MndHom H) \land A \in Z (S)) \to F (A) \in Y (F [S])$

Metamath Proof Explorer

Theorem cntzmhm

Proof