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 ` G )
conjghm.m 
|- .- = ( -g ` G )
conjsubg.f 
|- F = ( x e. S |-> ( ( A .+ x ) .- A ) )
conjnmz.1 
|- N = { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) }
Assertion conjnmz 
|- ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> S = ran F )

Proof

Step Hyp Ref Expression
1 conjghm.x 
 |-  X = ( Base ` G )
2 conjghm.p 
 |-  .+ = ( +g ` G )
3 conjghm.m 
 |-  .- = ( -g ` G )
4 conjsubg.f 
 |-  F = ( x e. S |-> ( ( A .+ x ) .- A ) )
5 conjnmz.1 
 |-  N = { y e. X | A. z e. X ( ( y .+ z ) e. S <-> ( z .+ y ) e. S ) }
6 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
7 6 ad2antrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> G e. Grp )
8 5 ssrab3 
 |-  N C_ X
9 simplr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> A e. N )
10 8 9 sselid 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> A e. X )
11 eqid 
 |-  ( invg ` G ) = ( invg ` G )
12 1 11 grpinvcl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ( invg ` G ) ` A ) e. X )
13 7 10 12 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( invg ` G ) ` A ) e. X )
14 1 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ X )
15 14 adantr 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> S C_ X )
16 15 sselda 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> w e. X )
17 1 2 grpass 
 |-  ( ( G e. Grp /\ ( ( ( invg ` G ) ` A ) e. X /\ w e. X /\ A e. X ) ) -> ( ( ( ( invg ` G ) ` A ) .+ w ) .+ A ) = ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) )
18 7 13 16 10 17 syl13anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( ( ( invg ` G ) ` A ) .+ w ) .+ A ) = ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) )
19 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
20 1 2 19 11 grprinv 
 |-  ( ( G e. Grp /\ A e. X ) -> ( A .+ ( ( invg ` G ) ` A ) ) = ( 0g ` G ) )
21 7 10 20 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( A .+ ( ( invg ` G ) ` A ) ) = ( 0g ` G ) )
22 21 oveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( A .+ ( ( invg ` G ) ` A ) ) .+ w ) = ( ( 0g ` G ) .+ w ) )
23 1 2 grpass 
 |-  ( ( G e. Grp /\ ( A e. X /\ ( ( invg ` G ) ` A ) e. X /\ w e. X ) ) -> ( ( A .+ ( ( invg ` G ) ` A ) ) .+ w ) = ( A .+ ( ( ( invg ` G ) ` A ) .+ w ) ) )
24 7 10 13 16 23 syl13anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( A .+ ( ( invg ` G ) ` A ) ) .+ w ) = ( A .+ ( ( ( invg ` G ) ` A ) .+ w ) ) )
25 1 2 19 grplid 
 |-  ( ( G e. Grp /\ w e. X ) -> ( ( 0g ` G ) .+ w ) = w )
26 7 16 25 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( 0g ` G ) .+ w ) = w )
27 22 24 26 3eqtr3d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( A .+ ( ( ( invg ` G ) ` A ) .+ w ) ) = w )
28 simpr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> w e. S )
29 27 28 eqeltrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( A .+ ( ( ( invg ` G ) ` A ) .+ w ) ) e. S )
30 1 2 grpcl 
 |-  ( ( G e. Grp /\ ( ( invg ` G ) ` A ) e. X /\ w e. X ) -> ( ( ( invg ` G ) ` A ) .+ w ) e. X )
31 7 13 16 30 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( ( invg ` G ) ` A ) .+ w ) e. X )
32 5 nmzbi 
 |-  ( ( A e. N /\ ( ( ( invg ` G ) ` A ) .+ w ) e. X ) -> ( ( A .+ ( ( ( invg ` G ) ` A ) .+ w ) ) e. S <-> ( ( ( ( invg ` G ) ` A ) .+ w ) .+ A ) e. S ) )
33 9 31 32 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( A .+ ( ( ( invg ` G ) ` A ) .+ w ) ) e. S <-> ( ( ( ( invg ` G ) ` A ) .+ w ) .+ A ) e. S ) )
34 29 33 mpbid 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( ( ( invg ` G ) ` A ) .+ w ) .+ A ) e. S )
35 18 34 eqeltrrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) e. S )
36 oveq2 
 |-  ( x = ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) -> ( A .+ x ) = ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) )
37 36 oveq1d 
 |-  ( x = ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) -> ( ( A .+ x ) .- A ) = ( ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) .- A ) )
38 ovex 
 |-  ( ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) .- A ) e. _V
39 37 4 38 fvmpt 
 |-  ( ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) e. S -> ( F ` ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) = ( ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) .- A ) )
40 35 39 syl 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( F ` ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) = ( ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) .- A ) )
41 21 oveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( A .+ ( ( invg ` G ) ` A ) ) .+ ( w .+ A ) ) = ( ( 0g ` G ) .+ ( w .+ A ) ) )
42 1 2 grpcl 
 |-  ( ( G e. Grp /\ w e. X /\ A e. X ) -> ( w .+ A ) e. X )
43 7 16 10 42 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( w .+ A ) e. X )
44 1 2 grpass 
 |-  ( ( G e. Grp /\ ( A e. X /\ ( ( invg ` G ) ` A ) e. X /\ ( w .+ A ) e. X ) ) -> ( ( A .+ ( ( invg ` G ) ` A ) ) .+ ( w .+ A ) ) = ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) )
45 7 10 13 43 44 syl13anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( A .+ ( ( invg ` G ) ` A ) ) .+ ( w .+ A ) ) = ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) )
46 1 2 19 grplid 
 |-  ( ( G e. Grp /\ ( w .+ A ) e. X ) -> ( ( 0g ` G ) .+ ( w .+ A ) ) = ( w .+ A ) )
47 7 43 46 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( 0g ` G ) .+ ( w .+ A ) ) = ( w .+ A ) )
48 41 45 47 3eqtr3d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) = ( w .+ A ) )
49 48 oveq1d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( A .+ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) .- A ) = ( ( w .+ A ) .- A ) )
50 1 2 3 grppncan 
 |-  ( ( G e. Grp /\ w e. X /\ A e. X ) -> ( ( w .+ A ) .- A ) = w )
51 7 16 10 50 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( ( w .+ A ) .- A ) = w )
52 40 49 51 3eqtrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( F ` ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) = w )
53 ovex 
 |-  ( ( A .+ x ) .- A ) e. _V
54 53 4 fnmpti 
 |-  F Fn S
55 fnfvelrn 
 |-  ( ( F Fn S /\ ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) e. S ) -> ( F ` ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) e. ran F )
56 54 35 55 sylancr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> ( F ` ( ( ( invg ` G ) ` A ) .+ ( w .+ A ) ) ) e. ran F )
57 52 56 eqeltrrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ w e. S ) -> w e. ran F )
58 57 ex 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> ( w e. S -> w e. ran F ) )
59 58 ssrdv 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> S C_ ran F )
60 6 ad2antrr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> G e. Grp )
61 simplr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> A e. N )
62 8 61 sselid 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> A e. X )
63 15 sselda 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> x e. X )
64 1 2 3 grpaddsubass 
 |-  ( ( G e. Grp /\ ( A e. X /\ x e. X /\ A e. X ) ) -> ( ( A .+ x ) .- A ) = ( A .+ ( x .- A ) ) )
65 60 62 63 62 64 syl13anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> ( ( A .+ x ) .- A ) = ( A .+ ( x .- A ) ) )
66 1 2 3 grpnpcan 
 |-  ( ( G e. Grp /\ x e. X /\ A e. X ) -> ( ( x .- A ) .+ A ) = x )
67 60 63 62 66 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> ( ( x .- A ) .+ A ) = x )
68 simpr 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> x e. S )
69 67 68 eqeltrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> ( ( x .- A ) .+ A ) e. S )
70 1 3 grpsubcl 
 |-  ( ( G e. Grp /\ x e. X /\ A e. X ) -> ( x .- A ) e. X )
71 60 63 62 70 syl3anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> ( x .- A ) e. X )
72 5 nmzbi 
 |-  ( ( A e. N /\ ( x .- A ) e. X ) -> ( ( A .+ ( x .- A ) ) e. S <-> ( ( x .- A ) .+ A ) e. S ) )
73 61 71 72 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> ( ( A .+ ( x .- A ) ) e. S <-> ( ( x .- A ) .+ A ) e. S ) )
74 69 73 mpbird 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> ( A .+ ( x .- A ) ) e. S )
75 65 74 eqeltrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ A e. N ) /\ x e. S ) -> ( ( A .+ x ) .- A ) e. S )
76 75 4 fmptd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> F : S --> S )
77 76 frnd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> ran F C_ S )
78 59 77 eqssd 
 |-  ( ( S e. ( SubGrp ` G ) /\ A e. N ) -> S = ran F )