Theorem cntzcmn

Description: The centralizer of any subset in a commutative monoid is the whole monoid. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	cntzcmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cntzcmn.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
Assertion	cntzcmn	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cntzcmn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cntzcmn.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
3	1 2	cntzssv	⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵
4	3	a1i	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 )
5		simpl1	⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐺 ∈ CMnd )
6		simpl3	⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
7		simp2	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑆 ⊆ 𝐵 )
8	7	sselda	⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐵 )
9		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10	1 9	cmncom	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
11	5 6 8 10	syl3anc	⊢ ( ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
12	11	ralrimiva	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
13	1 9 2	cntzel	⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
14	13	3adant1	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
15	12 14	mpbird	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) )
16	15	3expia	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) )
17	16	ssrdv	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ) → 𝐵 ⊆ ( 𝑍 ‘ 𝑆 ) )
18	4 17	eqssd	⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) = 𝐵 )