Metamath Proof Explorer

Theorem cntzsubm

Description: Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses cntzrec.b 
|- B = ( Base ` M )
cntzrec.z 
|- Z = ( Cntz ` M )
Assertion cntzsubm 
|- ( ( M e. Mnd /\ S C_ B ) -> ( Z ` S ) e. ( SubMnd ` M ) )

Proof

Step Hyp Ref Expression
1 cntzrec.b 
 |-  B = ( Base ` M )
2 cntzrec.z 
 |-  Z = ( Cntz ` M )
3 1 2 cntzssv 
 |-  ( Z ` S ) C_ B
4 3 a1i 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( Z ` S ) C_ B )
5 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
6 1 5 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. B )
7 6 adantr 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( 0g ` M ) e. B )
8 simpll 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ x e. S ) -> M e. Mnd )
9 simpr 
 |-  ( ( M e. Mnd /\ S C_ B ) -> S C_ B )
10 9 sselda 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ x e. S ) -> x e. B )
11 eqid 
 |-  ( +g ` M ) = ( +g ` M )
12 1 11 5 mndlid 
 |-  ( ( M e. Mnd /\ x e. B ) -> ( ( 0g ` M ) ( +g ` M ) x ) = x )
13 8 10 12 syl2anc 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ x e. S ) -> ( ( 0g ` M ) ( +g ` M ) x ) = x )
14 1 11 5 mndrid 
 |-  ( ( M e. Mnd /\ x e. B ) -> ( x ( +g ` M ) ( 0g ` M ) ) = x )
15 8 10 14 syl2anc 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ x e. S ) -> ( x ( +g ` M ) ( 0g ` M ) ) = x )
16 13 15 eqtr4d 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ x e. S ) -> ( ( 0g ` M ) ( +g ` M ) x ) = ( x ( +g ` M ) ( 0g ` M ) ) )
17 16 ralrimiva 
 |-  ( ( M e. Mnd /\ S C_ B ) -> A. x e. S ( ( 0g ` M ) ( +g ` M ) x ) = ( x ( +g ` M ) ( 0g ` M ) ) )
18 1 11 2 elcntz 
 |-  ( S C_ B -> ( ( 0g ` M ) e. ( Z ` S ) <-> ( ( 0g ` M ) e. B /\ A. x e. S ( ( 0g ` M ) ( +g ` M ) x ) = ( x ( +g ` M ) ( 0g ` M ) ) ) ) )
19 18 adantl 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( ( 0g ` M ) e. ( Z ` S ) <-> ( ( 0g ` M ) e. B /\ A. x e. S ( ( 0g ` M ) ( +g ` M ) x ) = ( x ( +g ` M ) ( 0g ` M ) ) ) ) )
20 7 17 19 mpbir2and 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( 0g ` M ) e. ( Z ` S ) )
21 simpll 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> M e. Mnd )
22 simprl 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> y e. ( Z ` S ) )
23 3 22 sselid 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> y e. B )
24 simprr 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> z e. ( Z ` S ) )
25 3 24 sselid 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> z e. B )
26 1 11 mndcl 
 |-  ( ( M e. Mnd /\ y e. B /\ z e. B ) -> ( y ( +g ` M ) z ) e. B )
27 21 23 25 26 syl3anc 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> ( y ( +g ` M ) z ) e. B )
28 21 adantr 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> M e. Mnd )
29 23 adantr 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> y e. B )
30 25 adantr 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> z e. B )
31 10 adantlr 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> x e. B )
32 1 11 mndass 
 |-  ( ( M e. Mnd /\ ( y e. B /\ z e. B /\ x e. B ) ) -> ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( y ( +g ` M ) ( z ( +g ` M ) x ) ) )
33 28 29 30 31 32 syl13anc 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( y ( +g ` M ) ( z ( +g ` M ) x ) ) )
34 11 2 cntzi 
 |-  ( ( z e. ( Z ` S ) /\ x e. S ) -> ( z ( +g ` M ) x ) = ( x ( +g ` M ) z ) )
35 24 34 sylan 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( z ( +g ` M ) x ) = ( x ( +g ` M ) z ) )
36 35 oveq2d 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( y ( +g ` M ) ( z ( +g ` M ) x ) ) = ( y ( +g ` M ) ( x ( +g ` M ) z ) ) )
37 1 11 mndass 
 |-  ( ( M e. Mnd /\ ( y e. B /\ x e. B /\ z e. B ) ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) z ) = ( y ( +g ` M ) ( x ( +g ` M ) z ) ) )
38 28 29 31 30 37 syl13anc 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) z ) = ( y ( +g ` M ) ( x ( +g ` M ) z ) ) )
39 11 2 cntzi 
 |-  ( ( y e. ( Z ` S ) /\ x e. S ) -> ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) )
40 22 39 sylan 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) )
41 40 oveq1d 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) z ) = ( ( x ( +g ` M ) y ) ( +g ` M ) z ) )
42 36 38 41 3eqtr2d 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( y ( +g ` M ) ( z ( +g ` M ) x ) ) = ( ( x ( +g ` M ) y ) ( +g ` M ) z ) )
43 1 11 mndass 
 |-  ( ( M e. Mnd /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
44 28 31 29 30 43 syl13anc 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( ( x ( +g ` M ) y ) ( +g ` M ) z ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
45 33 42 44 3eqtrd 
 |-  ( ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) /\ x e. S ) -> ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
46 45 ralrimiva 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> A. x e. S ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) )
47 1 11 2 elcntz 
 |-  ( S C_ B -> ( ( y ( +g ` M ) z ) e. ( Z ` S ) <-> ( ( y ( +g ` M ) z ) e. B /\ A. x e. S ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) )
48 47 ad2antlr 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> ( ( y ( +g ` M ) z ) e. ( Z ` S ) <-> ( ( y ( +g ` M ) z ) e. B /\ A. x e. S ( ( y ( +g ` M ) z ) ( +g ` M ) x ) = ( x ( +g ` M ) ( y ( +g ` M ) z ) ) ) ) )
49 27 46 48 mpbir2and 
 |-  ( ( ( M e. Mnd /\ S C_ B ) /\ ( y e. ( Z ` S ) /\ z e. ( Z ` S ) ) ) -> ( y ( +g ` M ) z ) e. ( Z ` S ) )
50 49 ralrimivva 
 |-  ( ( M e. Mnd /\ S C_ B ) -> A. y e. ( Z ` S ) A. z e. ( Z ` S ) ( y ( +g ` M ) z ) e. ( Z ` S ) )
51 1 5 11 issubm 
 |-  ( M e. Mnd -> ( ( Z ` S ) e. ( SubMnd ` M ) <-> ( ( Z ` S ) C_ B /\ ( 0g ` M ) e. ( Z ` S ) /\ A. y e. ( Z ` S ) A. z e. ( Z ` S ) ( y ( +g ` M ) z ) e. ( Z ` S ) ) ) )
52 51 adantr 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( ( Z ` S ) e. ( SubMnd ` M ) <-> ( ( Z ` S ) C_ B /\ ( 0g ` M ) e. ( Z ` S ) /\ A. y e. ( Z ` S ) A. z e. ( Z ` S ) ( y ( +g ` M ) z ) e. ( Z ` S ) ) ) )
53 4 20 50 52 mpbir3and 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( Z ` S ) e. ( SubMnd ` M ) )