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 X | y X x + ˙ y S y + ˙ x S
nmzsubg.2 X = Base G
nmzsubg.3 + ˙ = + G
Assertion nmzsubg G Grp N SubGrp G

Proof

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