cntrcmnd

Description: The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023)

		Ref	Expression
	Hypothesis	cntrcmnd.z	$⊢ Z = M ↾_{𝑠} Cntr (M)$
	Assertion	cntrcmnd	$⊢ M \in Mnd \to Z \in CMnd$

Step	Hyp	Ref	Expression
1		cntrcmnd.z	$⊢ Z = M ↾_{𝑠} Cntr (M)$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3	2	cntrss	$⊢ Cntr (M) \subseteq {Base}_{M}$
4	1 2	ressbas2	$⊢ Cntr (M) \subseteq {Base}_{M} \to Cntr (M) = {Base}_{Z}$
5	3 4	mp1i	$⊢ M \in Mnd \to Cntr (M) = {Base}_{Z}$
6		fvex	$⊢ Cntr (M) \in V$
7		eqid	$⊢ +_{M} = +_{M}$
8	1 7	ressplusg	$⊢ Cntr (M) \in V \to +_{M} = +_{Z}$
9	6 8	mp1i	$⊢ M \in Mnd \to +_{M} = +_{Z}$
10		eqid	$⊢ Cntz (M) = Cntz (M)$
11	2 10	cntrval	$⊢ Cntz (M) ({Base}_{M}) = Cntr (M)$
12		ssid	$⊢ {Base}_{M} \subseteq {Base}_{M}$
13	2 10	cntzsubm	$⊢ (M \in Mnd \land {Base}_{M} \subseteq {Base}_{M}) \to Cntz (M) ({Base}_{M}) \in SubMnd (M)$
14	12 13	mpan2	$⊢ M \in Mnd \to Cntz (M) ({Base}_{M}) \in SubMnd (M)$
15	11 14	eqeltrrid	$⊢ M \in Mnd \to Cntr (M) \in SubMnd (M)$
16	1	submmnd	$⊢ Cntr (M) \in SubMnd (M) \to Z \in Mnd$
17	15 16	syl	$⊢ M \in Mnd \to Z \in Mnd$
18		simp2	$⊢ (M \in Mnd \land x \in Cntr (M) \land y \in Cntr (M)) \to x \in Cntr (M)$
19		simp3	$⊢ (M \in Mnd \land x \in Cntr (M) \land y \in Cntr (M)) \to y \in Cntr (M)$
20	3 19	sselid	$⊢ (M \in Mnd \land x \in Cntr (M) \land y \in Cntr (M)) \to y \in {Base}_{M}$
21		eqid	$⊢ Cntr (M) = Cntr (M)$
22	2 7 21	cntri	$⊢ (x \in Cntr (M) \land y \in {Base}_{M}) \to x +_{M} y = y +_{M} x$
23	18 20 22	syl2anc	$⊢ (M \in Mnd \land x \in Cntr (M) \land y \in Cntr (M)) \to x +_{M} y = y +_{M} x$
24	5 9 17 23	iscmnd	$⊢ M \in Mnd \to Z \in CMnd$

Metamath Proof Explorer