Metamath Proof Explorer

Theorem cntzsubg

Description: Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 cntzrec.b 
 |-  B = ( Base ` M )
2 cntzrec.z 
 |-  Z = ( Cntz ` M )
3 grpmnd 
 |-  ( M e. Grp -> M e. Mnd )
4 1 2 cntzsubm 
 |-  ( ( M e. Mnd /\ S C_ B ) -> ( Z ` S ) e. ( SubMnd ` M ) )
5 3 4 sylan 
 |-  ( ( M e. Grp /\ S C_ B ) -> ( Z ` S ) e. ( SubMnd ` M ) )
6 simpll 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> M e. Grp )
7 1 2 cntzssv 
 |-  ( Z ` S ) C_ B
8 simprl 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> x e. ( Z ` S ) )
9 7 8 sseldi 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> x e. B )
10 eqid 
 |-  ( invg ` M ) = ( invg ` M )
11 1 10 grpinvcl 
 |-  ( ( M e. Grp /\ x e. B ) -> ( ( invg ` M ) ` x ) e. B )
12 6 9 11 syl2anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( invg ` M ) ` x ) e. B )
13 ssel2 
 |-  ( ( S C_ B /\ y e. S ) -> y e. B )
14 13 ad2ant2l 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> y e. B )
15 eqid 
 |-  ( +g ` M ) = ( +g ` M )
16 1 15 grpcl 
 |-  ( ( M e. Grp /\ x e. B /\ ( ( invg ` M ) ` x ) e. B ) -> ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) e. B )
17 6 9 12 16 syl3anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) e. B )
18 1 15 grpass 
 |-  ( ( M e. Grp /\ ( ( ( invg ` M ) ` x ) e. B /\ y e. B /\ ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) e. B ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( y ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) ) )
19 6 12 14 17 18 syl13anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( y ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) ) )
20 1 15 grpass 
 |-  ( ( M e. Grp /\ ( y e. B /\ x e. B /\ ( ( invg ` M ) ` x ) e. B ) ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) ( ( invg ` M ) ` x ) ) = ( y ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
21 6 14 9 12 20 syl13anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( y ( +g ` M ) x ) ( +g ` M ) ( ( invg ` M ) ` x ) ) = ( y ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
22 21 oveq2d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) ( ( y ( +g ` M ) x ) ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( y ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) ) )
23 19 22 eqtr4d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( ( y ( +g ` M ) x ) ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
24 15 2 cntzi 
 |-  ( ( x e. ( Z ` S ) /\ y e. S ) -> ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
25 24 adantl 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( x ( +g ` M ) y ) = ( y ( +g ` M ) x ) )
26 25 oveq1d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( x ( +g ` M ) y ) ( +g ` M ) ( ( invg ` M ) ` x ) ) = ( ( y ( +g ` M ) x ) ( +g ` M ) ( ( invg ` M ) ` x ) ) )
27 26 oveq2d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( ( y ( +g ` M ) x ) ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
28 23 27 eqtr4d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
29 1 15 grpcl 
 |-  ( ( M e. Grp /\ y e. B /\ ( ( invg ` M ) ` x ) e. B ) -> ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) e. B )
30 6 14 12 29 syl3anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) e. B )
31 1 15 grpass 
 |-  ( ( M e. Grp /\ ( ( ( invg ` M ) ` x ) e. B /\ x e. B /\ ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) e. B ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( x ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) ) )
32 6 12 9 30 31 syl13anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( x ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) ) )
33 1 15 grpass 
 |-  ( ( M e. Grp /\ ( x e. B /\ y e. B /\ ( ( invg ` M ) ` x ) e. B ) ) -> ( ( x ( +g ` M ) y ) ( +g ` M ) ( ( invg ` M ) ` x ) ) = ( x ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
34 6 9 14 12 33 syl13anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( x ( +g ` M ) y ) ( +g ` M ) ( ( invg ` M ) ` x ) ) = ( x ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
35 34 oveq2d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( x ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) ) )
36 32 35 eqtr4d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) ( ( x ( +g ` M ) y ) ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
37 28 36 eqtr4d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
38 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
39 1 15 38 10 grprinv 
 |-  ( ( M e. Grp /\ x e. B ) -> ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) = ( 0g ` M ) )
40 6 9 39 syl2anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) = ( 0g ` M ) )
41 40 oveq2d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( 0g ` M ) ) )
42 1 15 grpcl 
 |-  ( ( M e. Grp /\ ( ( invg ` M ) ` x ) e. B /\ y e. B ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) e. B )
43 6 12 14 42 syl3anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) e. B )
44 1 15 38 grprid 
 |-  ( ( M e. Grp /\ ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) e. B ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( 0g ` M ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) )
45 6 43 44 syl2anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( 0g ` M ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) )
46 41 45 eqtrd 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) ( +g ` M ) ( x ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) )
47 1 15 38 10 grplinv 
 |-  ( ( M e. Grp /\ x e. B ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) = ( 0g ` M ) )
48 6 9 47 syl2anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) = ( 0g ` M ) )
49 48 oveq1d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( ( 0g ` M ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
50 1 15 38 grplid 
 |-  ( ( M e. Grp /\ ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) e. B ) -> ( ( 0g ` M ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) )
51 6 30 50 syl2anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( 0g ` M ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) )
52 49 51 eqtrd 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( ( invg ` M ) ` x ) ( +g ` M ) x ) ( +g ` M ) ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) )
53 37 46 52 3eqtr3d 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ ( x e. ( Z ` S ) /\ y e. S ) ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) )
54 53 anassrs 
 |-  ( ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) /\ y e. S ) -> ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) )
55 54 ralrimiva 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> A. y e. S ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) )
56 simplr 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> S C_ B )
57 simpll 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> M e. Grp )
58 simpr 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> x e. ( Z ` S ) )
59 7 58 sseldi 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> x e. B )
60 57 59 11 syl2anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( invg ` M ) ` x ) e. B )
61 1 15 2 cntzel 
 |-  ( ( S C_ B /\ ( ( invg ` M ) ` x ) e. B ) -> ( ( ( invg ` M ) ` x ) e. ( Z ` S ) <-> A. y e. S ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
62 56 60 61 syl2anc 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( ( invg ` M ) ` x ) e. ( Z ` S ) <-> A. y e. S ( ( ( invg ` M ) ` x ) ( +g ` M ) y ) = ( y ( +g ` M ) ( ( invg ` M ) ` x ) ) ) )
63 55 62 mpbird 
 |-  ( ( ( M e. Grp /\ S C_ B ) /\ x e. ( Z ` S ) ) -> ( ( invg ` M ) ` x ) e. ( Z ` S ) )
64 63 ralrimiva 
 |-  ( ( M e. Grp /\ S C_ B ) -> A. x e. ( Z ` S ) ( ( invg ` M ) ` x ) e. ( Z ` S ) )
65 10 issubg3 
 |-  ( M e. Grp -> ( ( Z ` S ) e. ( SubGrp ` M ) <-> ( ( Z ` S ) e. ( SubMnd ` M ) /\ A. x e. ( Z ` S ) ( ( invg ` M ) ` x ) e. ( Z ` S ) ) ) )
66 65 adantr 
 |-  ( ( M e. Grp /\ S C_ B ) -> ( ( Z ` S ) e. ( SubGrp ` M ) <-> ( ( Z ` S ) e. ( SubMnd ` M ) /\ A. x e. ( Z ` S ) ( ( invg ` M ) ` x ) e. ( Z ` S ) ) ) )
67 5 64 66 mpbir2and 
 |-  ( ( M e. Grp /\ S C_ B ) -> ( Z ` S ) e. ( SubGrp ` M ) )