Theorem cmnbascntr

Description: The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025)

	Ref	Expression
Hypotheses	cmnbascntr.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cmnbascntr.z	⊢ 𝑍 = ( Cntr ‘ 𝐺 )
Assertion	cmnbascntr	⊢ ( 𝐺 ∈ CMnd → 𝐵 = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		cmnbascntr.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cmnbascntr.z	⊢ 𝑍 = ( Cntr ‘ 𝐺 )
3		eqid	⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
4	1 3	cntrval	⊢ ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = ( Cntr ‘ 𝐺 )
5		ssid	⊢ 𝐵 ⊆ 𝐵
6		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7	1 6 3	cntzval	⊢ ( 𝐵 ⊆ 𝐵 → ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) } )
8	5 7	ax-mp	⊢ ( ( Cntz ‘ 𝐺 ) ‘ 𝐵 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) }
9	2 4 8	3eqtr2i	⊢ 𝑍 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) }
10	1 6	cmncom	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
11	10	3expa	⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
12	11	ralrimiva	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
13	12	rabeqcda	⊢ ( 𝐺 ∈ CMnd → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) } = 𝐵 )
14	9 13	eqtr2id	⊢ ( 𝐺 ∈ CMnd → 𝐵 = 𝑍 )