Metamath Proof Explorer

Theorem nmzsubg

Description: The normalizer N_G(S) of a subset S of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses elnmz.1 
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
nmzsubg.2 
|- X = ( Base ` G )
nmzsubg.3 
|- .+ = ( +g ` G )
Assertion nmzsubg 
|- ( G e. Grp -> N e. ( SubGrp ` G ) )

Proof

Step Hyp Ref Expression
1 elnmz.1 
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. S <-> ( y .+ x ) e. S ) }
2 nmzsubg.2 
 |-  X = ( Base ` G )
3 nmzsubg.3 
 |-  .+ = ( +g ` G )
4 1 ssrab3 
 |-  N C_ X
5 4 a1i 
 |-  ( G e. Grp -> N C_ X )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 2 6 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
8 2 3 6 grplid 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = z )
9 2 3 6 grprid 
 |-  ( ( G e. Grp /\ z e. X ) -> ( z .+ ( 0g ` G ) ) = z )
10 8 9 eqtr4d 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = ( z .+ ( 0g ` G ) ) )
11 10 eleq1d 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( ( 0g ` G ) .+ z ) e. S <-> ( z .+ ( 0g ` G ) ) e. S ) )
12 11 ralrimiva 
 |-  ( G e. Grp -> A. z e. X ( ( ( 0g ` G ) .+ z ) e. S <-> ( z .+ ( 0g ` G ) ) e. S ) )
13 1 elnmz 
 |-  ( ( 0g ` G ) e. N <-> ( ( 0g ` G ) e. X /\ A. z e. X ( ( ( 0g ` G ) .+ z ) e. S <-> ( z .+ ( 0g ` G ) ) e. S ) ) )
14 7 12 13 sylanbrc 
 |-  ( G e. Grp -> ( 0g ` G ) e. N )
15 14 ne0d 
 |-  ( G e. Grp -> N =/= (/) )
16 id 
 |-  ( G e. Grp -> G e. Grp )
17 4 sseli 
 |-  ( z e. N -> z e. X )
18 4 sseli 
 |-  ( w e. N -> w e. X )
19 2 3 grpcl 
 |-  ( ( G e. Grp /\ z e. X /\ w e. X ) -> ( z .+ w ) e. X )
20 16 17 18 19 syl3an 
 |-  ( ( G e. Grp /\ z e. N /\ w e. N ) -> ( z .+ w ) e. X )
21 simpl1 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> G e. Grp )
22 simpl2 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> z e. N )
23 4 22 sseldi 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> z e. X )
24 simpl3 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> w e. N )
25 4 24 sseldi 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> w e. X )
26 simpr 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> u e. X )
27 2 3 grpass 
 |-  ( ( G e. Grp /\ ( z e. X /\ w e. X /\ u e. X ) ) -> ( ( z .+ w ) .+ u ) = ( z .+ ( w .+ u ) ) )
28 21 23 25 26 27 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( z .+ w ) .+ u ) = ( z .+ ( w .+ u ) ) )
29 28 eleq1d 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( ( z .+ w ) .+ u ) e. S <-> ( z .+ ( w .+ u ) ) e. S ) )
30 2 3 grpcl 
 |-  ( ( G e. Grp /\ w e. X /\ u e. X ) -> ( w .+ u ) e. X )
31 21 25 26 30 syl3anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( w .+ u ) e. X )
32 1 nmzbi 
 |-  ( ( z e. N /\ ( w .+ u ) e. X ) -> ( ( z .+ ( w .+ u ) ) e. S <-> ( ( w .+ u ) .+ z ) e. S ) )
33 22 31 32 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( z .+ ( w .+ u ) ) e. S <-> ( ( w .+ u ) .+ z ) e. S ) )
34 2 3 grpass 
 |-  ( ( G e. Grp /\ ( w e. X /\ u e. X /\ z e. X ) ) -> ( ( w .+ u ) .+ z ) = ( w .+ ( u .+ z ) ) )
35 21 25 26 23 34 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( w .+ u ) .+ z ) = ( w .+ ( u .+ z ) ) )
36 35 eleq1d 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( ( w .+ u ) .+ z ) e. S <-> ( w .+ ( u .+ z ) ) e. S ) )
37 2 3 grpcl 
 |-  ( ( G e. Grp /\ u e. X /\ z e. X ) -> ( u .+ z ) e. X )
38 21 26 23 37 syl3anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( u .+ z ) e. X )
39 1 nmzbi 
 |-  ( ( w e. N /\ ( u .+ z ) e. X ) -> ( ( w .+ ( u .+ z ) ) e. S <-> ( ( u .+ z ) .+ w ) e. S ) )
40 24 38 39 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( w .+ ( u .+ z ) ) e. S <-> ( ( u .+ z ) .+ w ) e. S ) )
41 33 36 40 3bitrd 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( z .+ ( w .+ u ) ) e. S <-> ( ( u .+ z ) .+ w ) e. S ) )
42 2 3 grpass 
 |-  ( ( G e. Grp /\ ( u e. X /\ z e. X /\ w e. X ) ) -> ( ( u .+ z ) .+ w ) = ( u .+ ( z .+ w ) ) )
43 21 26 23 25 42 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( u .+ z ) .+ w ) = ( u .+ ( z .+ w ) ) )
44 43 eleq1d 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( ( u .+ z ) .+ w ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) )
45 29 41 44 3bitrd 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( ( z .+ w ) .+ u ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) )
46 45 ralrimiva 
 |-  ( ( G e. Grp /\ z e. N /\ w e. N ) -> A. u e. X ( ( ( z .+ w ) .+ u ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) )
47 1 elnmz 
 |-  ( ( z .+ w ) e. N <-> ( ( z .+ w ) e. X /\ A. u e. X ( ( ( z .+ w ) .+ u ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) ) )
48 20 46 47 sylanbrc 
 |-  ( ( G e. Grp /\ z e. N /\ w e. N ) -> ( z .+ w ) e. N )
49 48 3expa 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ w e. N ) -> ( z .+ w ) e. N )
50 49 ralrimiva 
 |-  ( ( G e. Grp /\ z e. N ) -> A. w e. N ( z .+ w ) e. N )
51 eqid 
 |-  ( invg ` G ) = ( invg ` G )
52 2 51 grpinvcl 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( invg ` G ) ` z ) e. X )
53 17 52 sylan2 
 |-  ( ( G e. Grp /\ z e. N ) -> ( ( invg ` G ) ` z ) e. X )
54 simplr 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> z e. N )
55 simpll 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> G e. Grp )
56 53 adantr 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( invg ` G ) ` z ) e. X )
57 simpr 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> u e. X )
58 2 3 grpcl 
 |-  ( ( G e. Grp /\ u e. X /\ ( ( invg ` G ) ` z ) e. X ) -> ( u .+ ( ( invg ` G ) ` z ) ) e. X )
59 55 57 56 58 syl3anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( u .+ ( ( invg ` G ) ` z ) ) e. X )
60 2 3 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` z ) e. X /\ ( u .+ ( ( invg ` G ) ` z ) ) e. X ) -> ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) e. X )
61 55 56 59 60 syl3anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) e. X )
62 1 nmzbi 
 |-  ( ( z e. N /\ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) e. X ) -> ( ( z .+ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) ) e. S <-> ( ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) .+ z ) e. S ) )
63 54 61 62 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( z .+ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) ) e. S <-> ( ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) .+ z ) e. S ) )
64 4 54 sseldi 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> z e. X )
65 2 3 6 51 grprinv 
 |-  ( ( G e. Grp /\ z e. X ) -> ( z .+ ( ( invg ` G ) ` z ) ) = ( 0g ` G ) )
66 55 64 65 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( z .+ ( ( invg ` G ) ` z ) ) = ( 0g ` G ) )
67 66 oveq1d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( z .+ ( ( invg ` G ) ` z ) ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( ( 0g ` G ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) )
68 2 3 grpass 
 |-  ( ( G e. Grp /\ ( z e. X /\ ( ( invg ` G ) ` z ) e. X /\ ( u .+ ( ( invg ` G ) ` z ) ) e. X ) ) -> ( ( z .+ ( ( invg ` G ) ` z ) ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( z .+ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) ) )
69 55 64 56 59 68 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( z .+ ( ( invg ` G ) ` z ) ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( z .+ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) ) )
70 2 3 6 grplid 
 |-  ( ( G e. Grp /\ ( u .+ ( ( invg ` G ) ` z ) ) e. X ) -> ( ( 0g ` G ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( u .+ ( ( invg ` G ) ` z ) ) )
71 55 59 70 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( 0g ` G ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( u .+ ( ( invg ` G ) ` z ) ) )
72 67 69 71 3eqtr3d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( z .+ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) ) = ( u .+ ( ( invg ` G ) ` z ) ) )
73 72 eleq1d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( z .+ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) ) e. S <-> ( u .+ ( ( invg ` G ) ` z ) ) e. S ) )
74 2 3 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` z ) e. X /\ ( u .+ ( ( invg ` G ) ` z ) ) e. X /\ z e. X ) ) -> ( ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) .+ z ) = ( ( ( invg ` G ) ` z ) .+ ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) ) )
75 55 56 59 64 74 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) .+ z ) = ( ( ( invg ` G ) ` z ) .+ ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) ) )
76 2 3 grpass 
 |-  ( ( G e. Grp /\ ( u e. X /\ ( ( invg ` G ) ` z ) e. X /\ z e. X ) ) -> ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) = ( u .+ ( ( ( invg ` G ) ` z ) .+ z ) ) )
77 55 57 56 64 76 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) = ( u .+ ( ( ( invg ` G ) ` z ) .+ z ) ) )
78 2 3 6 51 grplinv 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
79 55 64 78 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
80 79 oveq2d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( u .+ ( ( ( invg ` G ) ` z ) .+ z ) ) = ( u .+ ( 0g ` G ) ) )
81 2 3 6 grprid 
 |-  ( ( G e. Grp /\ u e. X ) -> ( u .+ ( 0g ` G ) ) = u )
82 55 57 81 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( u .+ ( 0g ` G ) ) = u )
83 77 80 82 3eqtrd 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) = u )
84 83 oveq2d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( invg ` G ) ` z ) .+ ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) ) = ( ( ( invg ` G ) ` z ) .+ u ) )
85 75 84 eqtrd 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) .+ z ) = ( ( ( invg ` G ) ` z ) .+ u ) )
86 85 eleq1d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) .+ z ) e. S <-> ( ( ( invg ` G ) ` z ) .+ u ) e. S ) )
87 63 73 86 3bitr3rd 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( ( invg ` G ) ` z ) .+ u ) e. S <-> ( u .+ ( ( invg ` G ) ` z ) ) e. S ) )
88 87 ralrimiva 
 |-  ( ( G e. Grp /\ z e. N ) -> A. u e. X ( ( ( ( invg ` G ) ` z ) .+ u ) e. S <-> ( u .+ ( ( invg ` G ) ` z ) ) e. S ) )
89 1 elnmz 
 |-  ( ( ( invg ` G ) ` z ) e. N <-> ( ( ( invg ` G ) ` z ) e. X /\ A. u e. X ( ( ( ( invg ` G ) ` z ) .+ u ) e. S <-> ( u .+ ( ( invg ` G ) ` z ) ) e. S ) ) )
90 53 88 89 sylanbrc 
 |-  ( ( G e. Grp /\ z e. N ) -> ( ( invg ` G ) ` z ) e. N )
91 50 90 jca 
 |-  ( ( G e. Grp /\ z e. N ) -> ( A. w e. N ( z .+ w ) e. N /\ ( ( invg ` G ) ` z ) e. N ) )
92 91 ralrimiva 
 |-  ( G e. Grp -> A. z e. N ( A. w e. N ( z .+ w ) e. N /\ ( ( invg ` G ) ` z ) e. N ) )
93 2 3 51 issubg2 
 |-  ( G e. Grp -> ( N e. ( SubGrp ` G ) <-> ( N C_ X /\ N =/= (/) /\ A. z e. N ( A. w e. N ( z .+ w ) e. N /\ ( ( invg ` G ) ` z ) e. N ) ) ) )
94 5 15 92 93 mpbir3and 
 |-  ( G e. Grp -> N e. ( SubGrp ` G ) )