This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )