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

Metamath Proof Explorer

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 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) = 𝐵 )