Metamath Proof Explorer

Theorem submcmn2

Description: A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses subgabl.h 
|- H = ( G |`s S )
submcmn2.z 
|- Z = ( Cntz ` G )
Assertion submcmn2 
|- ( S e. ( SubMnd ` G ) -> ( H e. CMnd <-> S C_ ( Z ` S ) ) )

Proof

Step Hyp Ref Expression
1 subgabl.h 
 |-  H = ( G |`s S )
2 submcmn2.z 
 |-  Z = ( Cntz ` G )
3 1 submbas 
 |-  ( S e. ( SubMnd ` G ) -> S = ( Base ` H ) )
4 eqid 
 |-  ( +g ` G ) = ( +g ` G )
5 1 4 ressplusg 
 |-  ( S e. ( SubMnd ` G ) -> ( +g ` G ) = ( +g ` H ) )
6 5 oveqd 
 |-  ( S e. ( SubMnd ` G ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
7 5 oveqd 
 |-  ( S e. ( SubMnd ` G ) -> ( y ( +g ` G ) x ) = ( y ( +g ` H ) x ) )
8 6 7 eqeq12d 
 |-  ( S e. ( SubMnd ` G ) -> ( ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
9 3 8 raleqbidv 
 |-  ( S e. ( SubMnd ` G ) -> ( A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> A. y e. ( Base ` H ) ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
10 3 9 raleqbidv 
 |-  ( S e. ( SubMnd ` G ) -> ( A. x e. S A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) <-> A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
11 eqid 
 |-  ( Base ` G ) = ( Base ` G )
12 11 submss 
 |-  ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
13 11 4 2 sscntz 
 |-  ( ( S C_ ( Base ` G ) /\ S C_ ( Base ` G ) ) -> ( S C_ ( Z ` S ) <-> A. x e. S A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
14 12 12 13 syl2anc 
 |-  ( S e. ( SubMnd ` G ) -> ( S C_ ( Z ` S ) <-> A. x e. S A. y e. S ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
15 1 submmnd 
 |-  ( S e. ( SubMnd ` G ) -> H e. Mnd )
16 eqid 
 |-  ( Base ` H ) = ( Base ` H )
17 eqid 
 |-  ( +g ` H ) = ( +g ` H )
18 16 17 iscmn 
 |-  ( H e. CMnd <-> ( H e. Mnd /\ A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
19 18 baib 
 |-  ( H e. Mnd -> ( H e. CMnd <-> A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
20 15 19 syl 
 |-  ( S e. ( SubMnd ` G ) -> ( H e. CMnd <-> A. x e. ( Base ` H ) A. y e. ( Base ` H ) ( x ( +g ` H ) y ) = ( y ( +g ` H ) x ) ) )
21 10 14 20 3bitr4rd 
 |-  ( S e. ( SubMnd ` G ) -> ( H e. CMnd <-> S C_ ( Z ` S ) ) )