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 \|`s ( Cntr ` M ) )
	Assertion	cntrcmnd	\|- ( M e. Mnd -> Z e. CMnd )

Proof

Step	Hyp	Ref	Expression
1		cntrcmnd.z	\|- Z = ( M \|`s ( Cntr ` M ) )
2		eqid	\|- ( Base ` M ) = ( Base ` M )
3	2	cntrss	\|- ( Cntr ` M ) C_ ( Base ` M )
4	1 2	ressbas2	\|- ( ( Cntr ` M ) C_ ( Base ` M ) -> ( Cntr ` M ) = ( Base ` Z ) )
5	3 4	mp1i	\|- ( M e. Mnd -> ( Cntr ` M ) = ( Base ` Z ) )
6		fvex	\|- ( Cntr ` M ) e. _V
7		eqid	\|- ( +g ` M ) = ( +g ` M )
8	1 7	ressplusg	\|- ( ( Cntr ` M ) e. _V -> ( +g ` M ) = ( +g ` Z ) )
9	6 8	mp1i	\|- ( M e. Mnd -> ( +g ` M ) = ( +g ` Z ) )
10		eqid	\|- ( Cntz ` M ) = ( Cntz ` M )
11	2 10	cntrval	\|- ( ( Cntz ` M ) ` ( Base ` M ) ) = ( Cntr ` M )
12		ssid	\|- ( Base ` M ) C_ ( Base ` M )
13	2 10	cntzsubm	\|- ( ( M e. Mnd /\ ( Base ` M ) C_ ( Base ` M ) ) -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubMnd ` M ) )
14	12 13	mpan2	\|- ( M e. Mnd -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubMnd ` M ) )
15	11 14	eqeltrrid	\|- ( M e. Mnd -> ( Cntr ` M ) e. ( SubMnd ` M ) )
16	1	submmnd	\|- ( ( Cntr ` M ) e. ( SubMnd ` M ) -> Z e. Mnd )
17	15 16	syl	\|- ( M e. Mnd -> Z e. Mnd )
18		simp2	\|- ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> x e. ( Cntr ` M ) )
19		simp3	\|- ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> y e. ( Cntr ` M ) )
20	3 19	sselid	\|- ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> y e. ( Base ` M ) )
21		eqid	\|- ( Cntr ` M ) = ( Cntr ` M )
22	2 7 21	cntri	\|- ( ( x e. ( Cntr ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
23	18 20 22	syl2anc	\|- ( ( M e. Mnd /\ x e. ( Cntr ` M ) /\ y e. ( Cntr ` M ) ) -> ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
24	5 9 17 23	iscmnd	\|- ( M e. Mnd -> Z e. CMnd )

Metamath Proof Explorer

Theorem cntrcmnd

Proof