Theorem cntrcmnd

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

	Ref	Expression
Hypothesis	cntrcmnd.z	⊢ 𝑍 = ( 𝑀 ↾s ( Cntr ‘ 𝑀 ) )
Assertion	cntrcmnd	⊢ ( 𝑀 ∈ Mnd → 𝑍 ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		cntrcmnd.z	⊢ 𝑍 = ( 𝑀 ↾s ( Cntr ‘ 𝑀 ) )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3	2	cntrss	⊢ ( Cntr ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 )
4	1 2	ressbas2	⊢ ( ( Cntr ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) → ( Cntr ‘ 𝑀 ) = ( Base ‘ 𝑍 ) )
5	3 4	mp1i	⊢ ( 𝑀 ∈ Mnd → ( Cntr ‘ 𝑀 ) = ( Base ‘ 𝑍 ) )
6		fvex	⊢ ( Cntr ‘ 𝑀 ) ∈ V
7		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
8	1 7	ressplusg	⊢ ( ( Cntr ‘ 𝑀 ) ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑍 ) )
9	6 8	mp1i	⊢ ( 𝑀 ∈ Mnd → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑍 ) )
10		eqid	⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 )
11	2 10	cntrval	⊢ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = ( Cntr ‘ 𝑀 )
12		ssid	⊢ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 )
13	2 10	cntzsubm	⊢ ( ( 𝑀 ∈ Mnd ∧ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) ) → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubMnd ‘ 𝑀 ) )
14	12 13	mpan2	⊢ ( 𝑀 ∈ Mnd → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubMnd ‘ 𝑀 ) )
15	11 14	eqeltrrid	⊢ ( 𝑀 ∈ Mnd → ( Cntr ‘ 𝑀 ) ∈ ( SubMnd ‘ 𝑀 ) )
16	1	submmnd	⊢ ( ( Cntr ‘ 𝑀 ) ∈ ( SubMnd ‘ 𝑀 ) → 𝑍 ∈ Mnd )
17	15 16	syl	⊢ ( 𝑀 ∈ Mnd → 𝑍 ∈ Mnd )
18		simp2	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ ( Cntr ‘ 𝑀 ) ∧ 𝑦 ∈ ( Cntr ‘ 𝑀 ) ) → 𝑥 ∈ ( Cntr ‘ 𝑀 ) )
19		simp3	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ ( Cntr ‘ 𝑀 ) ∧ 𝑦 ∈ ( Cntr ‘ 𝑀 ) ) → 𝑦 ∈ ( Cntr ‘ 𝑀 ) )
20	3 19	sselid	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ ( Cntr ‘ 𝑀 ) ∧ 𝑦 ∈ ( Cntr ‘ 𝑀 ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
21		eqid	⊢ ( Cntr ‘ 𝑀 ) = ( Cntr ‘ 𝑀 )
22	2 7 21	cntri	⊢ ( ( 𝑥 ∈ ( Cntr ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
23	18 20 22	syl2anc	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ ( Cntr ‘ 𝑀 ) ∧ 𝑦 ∈ ( Cntr ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
24	5 9 17 23	iscmnd	⊢ ( 𝑀 ∈ Mnd → 𝑍 ∈ CMnd )