Metamath Proof Explorer


Theorem conjnmz

Description: A subgroup is unchanged under conjugation by an element of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses conjghm.x X = Base G
conjghm.p + ˙ = + G
conjghm.m - ˙ = - G
conjsubg.f F = x S A + ˙ x - ˙ A
conjnmz.1 N = y X | z X y + ˙ z S z + ˙ y S
Assertion conjnmz S SubGrp G A N S = ran F

Proof

Step Hyp Ref Expression
1 conjghm.x X = Base G
2 conjghm.p + ˙ = + G
3 conjghm.m - ˙ = - G
4 conjsubg.f F = x S A + ˙ x - ˙ A
5 conjnmz.1 N = y X | z X y + ˙ z S z + ˙ y S
6 subgrcl S SubGrp G G Grp
7 6 ad2antrr S SubGrp G A N w S G Grp
8 eqid inv g G = inv g G
9 5 ssrab3 N X
10 simplr S SubGrp G A N w S A N
11 9 10 sselid S SubGrp G A N w S A X
12 1 8 7 11 grpinvcld S SubGrp G A N w S inv g G A X
13 1 subgss S SubGrp G S X
14 13 adantr S SubGrp G A N S X
15 14 sselda S SubGrp G A N w S w X
16 1 2 7 12 15 11 grpassd S SubGrp G A N w S inv g G A + ˙ w + ˙ A = inv g G A + ˙ w + ˙ A
17 eqid 0 G = 0 G
18 1 2 17 8 7 11 grprinvd S SubGrp G A N w S A + ˙ inv g G A = 0 G
19 18 oveq1d S SubGrp G A N w S A + ˙ inv g G A + ˙ w = 0 G + ˙ w
20 1 2 7 11 12 15 grpassd S SubGrp G A N w S A + ˙ inv g G A + ˙ w = A + ˙ inv g G A + ˙ w
21 1 2 17 7 15 grplidd S SubGrp G A N w S 0 G + ˙ w = w
22 19 20 21 3eqtr3d S SubGrp G A N w S A + ˙ inv g G A + ˙ w = w
23 simpr S SubGrp G A N w S w S
24 22 23 eqeltrd S SubGrp G A N w S A + ˙ inv g G A + ˙ w S
25 1 2 7 12 15 grpcld S SubGrp G A N w S inv g G A + ˙ w X
26 5 nmzbi A N inv g G A + ˙ w X A + ˙ inv g G A + ˙ w S inv g G A + ˙ w + ˙ A S
27 10 25 26 syl2anc S SubGrp G A N w S A + ˙ inv g G A + ˙ w S inv g G A + ˙ w + ˙ A S
28 24 27 mpbid S SubGrp G A N w S inv g G A + ˙ w + ˙ A S
29 16 28 eqeltrrd S SubGrp G A N w S inv g G A + ˙ w + ˙ A S
30 oveq2 x = inv g G A + ˙ w + ˙ A A + ˙ x = A + ˙ inv g G A + ˙ w + ˙ A
31 30 oveq1d x = inv g G A + ˙ w + ˙ A A + ˙ x - ˙ A = A + ˙ inv g G A + ˙ w + ˙ A - ˙ A
32 ovex A + ˙ inv g G A + ˙ w + ˙ A - ˙ A V
33 31 4 32 fvmpt inv g G A + ˙ w + ˙ A S F inv g G A + ˙ w + ˙ A = A + ˙ inv g G A + ˙ w + ˙ A - ˙ A
34 29 33 syl S SubGrp G A N w S F inv g G A + ˙ w + ˙ A = A + ˙ inv g G A + ˙ w + ˙ A - ˙ A
35 18 oveq1d S SubGrp G A N w S A + ˙ inv g G A + ˙ w + ˙ A = 0 G + ˙ w + ˙ A
36 1 2 7 15 11 grpcld S SubGrp G A N w S w + ˙ A X
37 1 2 7 11 12 36 grpassd S SubGrp G A N w S A + ˙ inv g G A + ˙ w + ˙ A = A + ˙ inv g G A + ˙ w + ˙ A
38 1 2 17 7 36 grplidd S SubGrp G A N w S 0 G + ˙ w + ˙ A = w + ˙ A
39 35 37 38 3eqtr3d S SubGrp G A N w S A + ˙ inv g G A + ˙ w + ˙ A = w + ˙ A
40 39 oveq1d S SubGrp G A N w S A + ˙ inv g G A + ˙ w + ˙ A - ˙ A = w + ˙ A - ˙ A
41 1 2 3 grppncan G Grp w X A X w + ˙ A - ˙ A = w
42 7 15 11 41 syl3anc S SubGrp G A N w S w + ˙ A - ˙ A = w
43 34 40 42 3eqtrd S SubGrp G A N w S F inv g G A + ˙ w + ˙ A = w
44 ovex A + ˙ x - ˙ A V
45 44 4 fnmpti F Fn S
46 fnfvelrn F Fn S inv g G A + ˙ w + ˙ A S F inv g G A + ˙ w + ˙ A ran F
47 45 29 46 sylancr S SubGrp G A N w S F inv g G A + ˙ w + ˙ A ran F
48 43 47 eqeltrrd S SubGrp G A N w S w ran F
49 48 ex S SubGrp G A N w S w ran F
50 49 ssrdv S SubGrp G A N S ran F
51 6 ad2antrr S SubGrp G A N x S G Grp
52 simplr S SubGrp G A N x S A N
53 9 52 sselid S SubGrp G A N x S A X
54 14 sselda S SubGrp G A N x S x X
55 1 2 3 grpaddsubass G Grp A X x X A X A + ˙ x - ˙ A = A + ˙ x - ˙ A
56 51 53 54 53 55 syl13anc S SubGrp G A N x S A + ˙ x - ˙ A = A + ˙ x - ˙ A
57 1 2 3 grpnpcan G Grp x X A X x - ˙ A + ˙ A = x
58 51 54 53 57 syl3anc S SubGrp G A N x S x - ˙ A + ˙ A = x
59 simpr S SubGrp G A N x S x S
60 58 59 eqeltrd S SubGrp G A N x S x - ˙ A + ˙ A S
61 1 3 grpsubcl G Grp x X A X x - ˙ A X
62 51 54 53 61 syl3anc S SubGrp G A N x S x - ˙ A X
63 5 nmzbi A N x - ˙ A X A + ˙ x - ˙ A S x - ˙ A + ˙ A S
64 52 62 63 syl2anc S SubGrp G A N x S A + ˙ x - ˙ A S x - ˙ A + ˙ A S
65 60 64 mpbird S SubGrp G A N x S A + ˙ x - ˙ A S
66 56 65 eqeltrd S SubGrp G A N x S A + ˙ x - ˙ A S
67 66 4 fmptd S SubGrp G A N F : S S
68 67 frnd S SubGrp G A N ran F S
69 50 68 eqssd S SubGrp G A N S = ran F