This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid 
 |-  ( ( ( 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 sselid 
 |-  ( ( ( 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 21 25 26 grpcld 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( w .+ u ) e. X )
31 1 nmzbi 
 |-  ( ( z e. N /\ ( w .+ u ) e. X ) -> ( ( z .+ ( w .+ u ) ) e. S <-> ( ( w .+ u ) .+ z ) e. S ) )
32 22 30 31 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( z .+ ( w .+ u ) ) e. S <-> ( ( w .+ u ) .+ z ) e. S ) )
33 2 3 grpass 
 |-  ( ( G e. Grp /\ ( w e. X /\ u e. X /\ z e. X ) ) -> ( ( w .+ u ) .+ z ) = ( w .+ ( u .+ z ) ) )
34 21 25 26 23 33 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( w .+ u ) .+ z ) = ( w .+ ( u .+ z ) ) )
35 34 eleq1d 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( ( w .+ u ) .+ z ) e. S <-> ( w .+ ( u .+ z ) ) e. S ) )
36 2 3 21 26 23 grpcld 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( u .+ z ) e. X )
37 1 nmzbi 
 |-  ( ( w e. N /\ ( u .+ z ) e. X ) -> ( ( w .+ ( u .+ z ) ) e. S <-> ( ( u .+ z ) .+ w ) e. S ) )
38 24 36 37 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( w .+ ( u .+ z ) ) e. S <-> ( ( u .+ z ) .+ w ) e. S ) )
39 32 35 38 3bitrd 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( z .+ ( w .+ u ) ) e. S <-> ( ( u .+ z ) .+ w ) e. S ) )
40 2 3 grpass 
 |-  ( ( G e. Grp /\ ( u e. X /\ z e. X /\ w e. X ) ) -> ( ( u .+ z ) .+ w ) = ( u .+ ( z .+ w ) ) )
41 21 26 23 25 40 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( u .+ z ) .+ w ) = ( u .+ ( z .+ w ) ) )
42 41 eleq1d 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( ( u .+ z ) .+ w ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) )
43 29 39 42 3bitrd 
 |-  ( ( ( G e. Grp /\ z e. N /\ w e. N ) /\ u e. X ) -> ( ( ( z .+ w ) .+ u ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) )
44 43 ralrimiva 
 |-  ( ( G e. Grp /\ z e. N /\ w e. N ) -> A. u e. X ( ( ( z .+ w ) .+ u ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) )
45 1 elnmz 
 |-  ( ( z .+ w ) e. N <-> ( ( z .+ w ) e. X /\ A. u e. X ( ( ( z .+ w ) .+ u ) e. S <-> ( u .+ ( z .+ w ) ) e. S ) ) )
46 20 44 45 sylanbrc 
 |-  ( ( G e. Grp /\ z e. N /\ w e. N ) -> ( z .+ w ) e. N )
47 46 3expa 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ w e. N ) -> ( z .+ w ) e. N )
48 47 ralrimiva 
 |-  ( ( G e. Grp /\ z e. N ) -> A. w e. N ( z .+ w ) e. N )
49 eqid 
 |-  ( invg ` G ) = ( invg ` G )
50 2 49 grpinvcl 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( invg ` G ) ` z ) e. X )
51 17 50 sylan2 
 |-  ( ( G e. Grp /\ z e. N ) -> ( ( invg ` G ) ` z ) e. X )
52 simplr 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> z e. N )
53 simpll 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> G e. Grp )
54 51 adantr 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( invg ` G ) ` z ) e. X )
55 simpr 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> u e. X )
56 2 3 53 55 54 grpcld 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( u .+ ( ( invg ` G ) ` z ) ) e. X )
57 2 3 53 54 56 grpcld 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) e. X )
58 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 ) )
59 52 57 58 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 ) )
60 4 52 sselid 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> z e. X )
61 2 3 6 49 grprinv 
 |-  ( ( G e. Grp /\ z e. X ) -> ( z .+ ( ( invg ` G ) ` z ) ) = ( 0g ` G ) )
62 53 60 61 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( z .+ ( ( invg ` G ) ` z ) ) = ( 0g ` G ) )
63 62 oveq1d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( z .+ ( ( invg ` G ) ` z ) ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( ( 0g ` G ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) )
64 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 ) ) ) ) )
65 53 60 54 56 64 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 ) ) ) ) )
66 2 3 6 grplid 
 |-  ( ( G e. Grp /\ ( u .+ ( ( invg ` G ) ` z ) ) e. X ) -> ( ( 0g ` G ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( u .+ ( ( invg ` G ) ` z ) ) )
67 53 56 66 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( 0g ` G ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) = ( u .+ ( ( invg ` G ) ` z ) ) )
68 63 65 67 3eqtr3d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( z .+ ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) ) = ( u .+ ( ( invg ` G ) ` z ) ) )
69 68 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 ) )
70 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 ) ) )
71 53 54 56 60 70 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 ) ) )
72 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 ) ) )
73 53 55 54 60 72 syl13anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) = ( u .+ ( ( ( invg ` G ) ` z ) .+ z ) ) )
74 2 3 6 49 grplinv 
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
75 53 60 74 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( invg ` G ) ` z ) .+ z ) = ( 0g ` G ) )
76 75 oveq2d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( u .+ ( ( ( invg ` G ) ` z ) .+ z ) ) = ( u .+ ( 0g ` G ) ) )
77 2 3 6 grprid 
 |-  ( ( G e. Grp /\ u e. X ) -> ( u .+ ( 0g ` G ) ) = u )
78 53 55 77 syl2anc 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( u .+ ( 0g ` G ) ) = u )
79 73 76 78 3eqtrd 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) = u )
80 79 oveq2d 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( invg ` G ) ` z ) .+ ( ( u .+ ( ( invg ` G ) ` z ) ) .+ z ) ) = ( ( ( invg ` G ) ` z ) .+ u ) )
81 71 80 eqtrd 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( ( invg ` G ) ` z ) .+ ( u .+ ( ( invg ` G ) ` z ) ) ) .+ z ) = ( ( ( invg ` G ) ` z ) .+ u ) )
82 81 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 ) )
83 59 69 82 3bitr3rd 
 |-  ( ( ( G e. Grp /\ z e. N ) /\ u e. X ) -> ( ( ( ( invg ` G ) ` z ) .+ u ) e. S <-> ( u .+ ( ( invg ` G ) ` z ) ) e. S ) )
84 83 ralrimiva 
 |-  ( ( G e. Grp /\ z e. N ) -> A. u e. X ( ( ( ( invg ` G ) ` z ) .+ u ) e. S <-> ( u .+ ( ( invg ` G ) ` z ) ) e. S ) )
85 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 ) ) )
86 51 84 85 sylanbrc 
 |-  ( ( G e. Grp /\ z e. N ) -> ( ( invg ` G ) ` z ) e. N )
87 48 86 jca 
 |-  ( ( G e. Grp /\ z e. N ) -> ( A. w e. N ( z .+ w ) e. N /\ ( ( invg ` G ) ` z ) e. N ) )
88 87 ralrimiva 
 |-  ( G e. Grp -> A. z e. N ( A. w e. N ( z .+ w ) e. N /\ ( ( invg ` G ) ` z ) e. N ) )
89 2 3 49 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 ) ) ) )
90 5 15 88 89 mpbir3and 
 |-  ( G e. Grp -> N e. ( SubGrp ` G ) )