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