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 
|- B = ( Base ` G )
cntzcmn.z 
|- Z = ( Cntz ` G )
Assertion cntzcmn 
|- ( ( G e. CMnd /\ S C_ B ) -> ( Z ` S ) = B )

Proof

Step Hyp Ref Expression
1 cntzcmn.b 
 |-  B = ( Base ` G )
2 cntzcmn.z 
 |-  Z = ( Cntz ` G )
3 1 2 cntzssv 
 |-  ( Z ` S ) C_ B
4 3 a1i 
 |-  ( ( G e. CMnd /\ S C_ B ) -> ( Z ` S ) C_ B )
5 simpl1 
 |-  ( ( ( G e. CMnd /\ S C_ B /\ x e. B ) /\ y e. S ) -> G e. CMnd )
6 simpl3 
 |-  ( ( ( G e. CMnd /\ S C_ B /\ x e. B ) /\ y e. S ) -> x e. B )
7 simp2 
 |-  ( ( G e. CMnd /\ S C_ B /\ x e. B ) -> S C_ B )
8 7 sselda 
 |-  ( ( ( G e. CMnd /\ S C_ B /\ x e. B ) /\ y e. S ) -> y e. B )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 1 9 cmncom 
 |-  ( ( G e. CMnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
11 5 6 8 10 syl3anc 
 |-  ( ( ( G e. CMnd /\ S C_ B /\ x e. B ) /\ y e. S ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
12 11 ralrimiva 
 |-  ( ( G e. CMnd /\ S C_ B /\ x e. B ) -> A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
13 1 9 2 cntzel 
 |-  ( ( S C_ B /\ x e. B ) -> ( x e. ( Z ` S ) <-> A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
14 13 3adant1 
 |-  ( ( G e. CMnd /\ S C_ B /\ x e. B ) -> ( x e. ( Z ` S ) <-> A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
15 12 14 mpbird 
 |-  ( ( G e. CMnd /\ S C_ B /\ x e. B ) -> x e. ( Z ` S ) )
16 15 3expia 
 |-  ( ( G e. CMnd /\ S C_ B ) -> ( x e. B -> x e. ( Z ` S ) ) )
17 16 ssrdv 
 |-  ( ( G e. CMnd /\ S C_ B ) -> B C_ ( Z ` S ) )
18 4 17 eqssd 
 |-  ( ( G e. CMnd /\ S C_ B ) -> ( Z ` S ) = B )