Metamath Proof Explorer

Theorem sylow3lem2

Description: Lemma for sylow3 , first part. The stabilizer of a given Sylow subgroup K in the group action .(+) acting on all of G is the normalizer N_G(K). (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x 
|- X = ( Base ` G )
sylow3.g 
|- ( ph -> G e. Grp )
sylow3.xf 
|- ( ph -> X e. Fin )
sylow3.p 
|- ( ph -> P e. Prime )
sylow3lem1.a 
|- .+ = ( +g ` G )
sylow3lem1.d 
|- .- = ( -g ` G )
sylow3lem1.m 
|- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
sylow3lem2.k 
|- ( ph -> K e. ( P pSyl G ) )
sylow3lem2.h 
|- H = { u e. X | ( u .(+) K ) = K }
sylow3lem2.n 
|- N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }
Assertion sylow3lem2 
|- ( ph -> H = N )

Proof

Step Hyp Ref Expression
1 sylow3.x 
 |-  X = ( Base ` G )
2 sylow3.g 
 |-  ( ph -> G e. Grp )
3 sylow3.xf 
 |-  ( ph -> X e. Fin )
4 sylow3.p 
 |-  ( ph -> P e. Prime )
5 sylow3lem1.a 
 |-  .+ = ( +g ` G )
6 sylow3lem1.d 
 |-  .- = ( -g ` G )
7 sylow3lem1.m 
 |-  .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
8 sylow3lem2.k 
 |-  ( ph -> K e. ( P pSyl G ) )
9 sylow3lem2.h 
 |-  H = { u e. X | ( u .(+) K ) = K }
10 sylow3lem2.n 
 |-  N = { x e. X | A. y e. X ( ( x .+ y ) e. K <-> ( y .+ x ) e. K ) }
11 10 ssrab3 
 |-  N C_ X
12 sseqin2 
 |-  ( N C_ X <-> ( X i^i N ) = N )
13 11 12 mpbi 
 |-  ( X i^i N ) = N
14 simpr 
 |-  ( ( ph /\ u e. X ) -> u e. X )
15 8 adantr 
 |-  ( ( ph /\ u e. X ) -> K e. ( P pSyl G ) )
16 mptexg 
 |-  ( K e. ( P pSyl G ) -> ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V )
17 rnexg 
 |-  ( ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V -> ran ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V )
18 15 16 17 3syl 
 |-  ( ( ph /\ u e. X ) -> ran ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V )
19 simpr 
 |-  ( ( x = u /\ y = K ) -> y = K )
20 simpl 
 |-  ( ( x = u /\ y = K ) -> x = u )
21 20 oveq1d 
 |-  ( ( x = u /\ y = K ) -> ( x .+ z ) = ( u .+ z ) )
22 21 20 oveq12d 
 |-  ( ( x = u /\ y = K ) -> ( ( x .+ z ) .- x ) = ( ( u .+ z ) .- u ) )
23 19 22 mpteq12dv 
 |-  ( ( x = u /\ y = K ) -> ( z e. y |-> ( ( x .+ z ) .- x ) ) = ( z e. K |-> ( ( u .+ z ) .- u ) ) )
24 23 rneqd 
 |-  ( ( x = u /\ y = K ) -> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
25 24 7 ovmpoga 
 |-  ( ( u e. X /\ K e. ( P pSyl G ) /\ ran ( z e. K |-> ( ( u .+ z ) .- u ) ) e. _V ) -> ( u .(+) K ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
26 14 15 18 25 syl3anc 
 |-  ( ( ph /\ u e. X ) -> ( u .(+) K ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
27 26 adantr 
 |-  ( ( ( ph /\ u e. X ) /\ u e. N ) -> ( u .(+) K ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
28 slwsubg 
 |-  ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) )
29 8 28 syl 
 |-  ( ph -> K e. ( SubGrp ` G ) )
30 29 adantr 
 |-  ( ( ph /\ u e. X ) -> K e. ( SubGrp ` G ) )
31 eqid 
 |-  ( z e. K |-> ( ( u .+ z ) .- u ) ) = ( z e. K |-> ( ( u .+ z ) .- u ) )
32 1 5 6 31 10 conjnmz 
 |-  ( ( K e. ( SubGrp ` G ) /\ u e. N ) -> K = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
33 30 32 sylan 
 |-  ( ( ( ph /\ u e. X ) /\ u e. N ) -> K = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
34 27 33 eqtr4d 
 |-  ( ( ( ph /\ u e. X ) /\ u e. N ) -> ( u .(+) K ) = K )
35 simplr 
 |-  ( ( ( ph /\ u e. X ) /\ ( u .(+) K ) = K ) -> u e. X )
36 simprl 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( u .(+) K ) = K )
37 26 adantr 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( u .(+) K ) = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
38 36 37 eqtr3d 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> K = ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
39 38 eleq2d 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( ( u .+ w ) e. K <-> ( u .+ w ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) ) )
40 ovex 
 |-  ( u .+ w ) e. _V
41 eqeq1 
 |-  ( v = ( u .+ w ) -> ( v = ( ( u .+ z ) .- u ) <-> ( u .+ w ) = ( ( u .+ z ) .- u ) ) )
42 41 rexbidv 
 |-  ( v = ( u .+ w ) -> ( E. z e. K v = ( ( u .+ z ) .- u ) <-> E. z e. K ( u .+ w ) = ( ( u .+ z ) .- u ) ) )
43 31 rnmpt 
 |-  ran ( z e. K |-> ( ( u .+ z ) .- u ) ) = { v | E. z e. K v = ( ( u .+ z ) .- u ) }
44 40 42 43 elab2 
 |-  ( ( u .+ w ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) <-> E. z e. K ( u .+ w ) = ( ( u .+ z ) .- u ) )
45 simprr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( u .+ w ) = ( ( u .+ z ) .- u ) )
46 2 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> G e. Grp )
47 simpllr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> u e. X )
48 1 subgss 
 |-  ( K e. ( SubGrp ` G ) -> K C_ X )
49 29 48 syl 
 |-  ( ph -> K C_ X )
50 49 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> K C_ X )
51 simprl 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> z e. K )
52 50 51 sseldd 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> z e. X )
53 1 5 6 grpaddsubass 
 |-  ( ( G e. Grp /\ ( u e. X /\ z e. X /\ u e. X ) ) -> ( ( u .+ z ) .- u ) = ( u .+ ( z .- u ) ) )
54 46 47 52 47 53 syl13anc 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( ( u .+ z ) .- u ) = ( u .+ ( z .- u ) ) )
55 45 54 eqtr2d 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( u .+ ( z .- u ) ) = ( u .+ w ) )
56 1 6 grpsubcl 
 |-  ( ( G e. Grp /\ z e. X /\ u e. X ) -> ( z .- u ) e. X )
57 46 52 47 56 syl3anc 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( z .- u ) e. X )
58 simplrr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> w e. X )
59 1 5 grplcan 
 |-  ( ( G e. Grp /\ ( ( z .- u ) e. X /\ w e. X /\ u e. X ) ) -> ( ( u .+ ( z .- u ) ) = ( u .+ w ) <-> ( z .- u ) = w ) )
60 46 57 58 47 59 syl13anc 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( ( u .+ ( z .- u ) ) = ( u .+ w ) <-> ( z .- u ) = w ) )
61 55 60 mpbid 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( z .- u ) = w )
62 1 5 6 grpsubadd 
 |-  ( ( G e. Grp /\ ( z e. X /\ u e. X /\ w e. X ) ) -> ( ( z .- u ) = w <-> ( w .+ u ) = z ) )
63 46 52 47 58 62 syl13anc 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( ( z .- u ) = w <-> ( w .+ u ) = z ) )
64 61 63 mpbid 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( w .+ u ) = z )
65 64 51 eqeltrd 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( z e. K /\ ( u .+ w ) = ( ( u .+ z ) .- u ) ) ) -> ( w .+ u ) e. K )
66 65 rexlimdvaa 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( E. z e. K ( u .+ w ) = ( ( u .+ z ) .- u ) -> ( w .+ u ) e. K ) )
67 44 66 syl5bi 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( ( u .+ w ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) -> ( w .+ u ) e. K ) )
68 simpr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( w .+ u ) e. K )
69 oveq2 
 |-  ( z = ( w .+ u ) -> ( u .+ z ) = ( u .+ ( w .+ u ) ) )
70 69 oveq1d 
 |-  ( z = ( w .+ u ) -> ( ( u .+ z ) .- u ) = ( ( u .+ ( w .+ u ) ) .- u ) )
71 ovex 
 |-  ( ( u .+ ( w .+ u ) ) .- u ) e. _V
72 70 31 71 fvmpt 
 |-  ( ( w .+ u ) e. K -> ( ( z e. K |-> ( ( u .+ z ) .- u ) ) ` ( w .+ u ) ) = ( ( u .+ ( w .+ u ) ) .- u ) )
73 68 72 syl 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( ( z e. K |-> ( ( u .+ z ) .- u ) ) ` ( w .+ u ) ) = ( ( u .+ ( w .+ u ) ) .- u ) )
74 2 ad3antrrr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> G e. Grp )
75 simpllr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> u e. X )
76 simplrr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> w e. X )
77 1 5 grpass 
 |-  ( ( G e. Grp /\ ( u e. X /\ w e. X /\ u e. X ) ) -> ( ( u .+ w ) .+ u ) = ( u .+ ( w .+ u ) ) )
78 74 75 76 75 77 syl13anc 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( ( u .+ w ) .+ u ) = ( u .+ ( w .+ u ) ) )
79 78 oveq1d 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( ( ( u .+ w ) .+ u ) .- u ) = ( ( u .+ ( w .+ u ) ) .- u ) )
80 1 5 grpcl 
 |-  ( ( G e. Grp /\ u e. X /\ w e. X ) -> ( u .+ w ) e. X )
81 74 75 76 80 syl3anc 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( u .+ w ) e. X )
82 1 5 6 grppncan 
 |-  ( ( G e. Grp /\ ( u .+ w ) e. X /\ u e. X ) -> ( ( ( u .+ w ) .+ u ) .- u ) = ( u .+ w ) )
83 74 81 75 82 syl3anc 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( ( ( u .+ w ) .+ u ) .- u ) = ( u .+ w ) )
84 73 79 83 3eqtr2d 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( ( z e. K |-> ( ( u .+ z ) .- u ) ) ` ( w .+ u ) ) = ( u .+ w ) )
85 ovex 
 |-  ( ( u .+ z ) .- u ) e. _V
86 85 31 fnmpti 
 |-  ( z e. K |-> ( ( u .+ z ) .- u ) ) Fn K
87 fnfvelrn 
 |-  ( ( ( z e. K |-> ( ( u .+ z ) .- u ) ) Fn K /\ ( w .+ u ) e. K ) -> ( ( z e. K |-> ( ( u .+ z ) .- u ) ) ` ( w .+ u ) ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
88 86 68 87 sylancr 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( ( z e. K |-> ( ( u .+ z ) .- u ) ) ` ( w .+ u ) ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
89 84 88 eqeltrrd 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) /\ ( w .+ u ) e. K ) -> ( u .+ w ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) )
90 89 ex 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( ( w .+ u ) e. K -> ( u .+ w ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) ) )
91 67 90 impbid 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( ( u .+ w ) e. ran ( z e. K |-> ( ( u .+ z ) .- u ) ) <-> ( w .+ u ) e. K ) )
92 39 91 bitrd 
 |-  ( ( ( ph /\ u e. X ) /\ ( ( u .(+) K ) = K /\ w e. X ) ) -> ( ( u .+ w ) e. K <-> ( w .+ u ) e. K ) )
93 92 anassrs 
 |-  ( ( ( ( ph /\ u e. X ) /\ ( u .(+) K ) = K ) /\ w e. X ) -> ( ( u .+ w ) e. K <-> ( w .+ u ) e. K ) )
94 93 ralrimiva 
 |-  ( ( ( ph /\ u e. X ) /\ ( u .(+) K ) = K ) -> A. w e. X ( ( u .+ w ) e. K <-> ( w .+ u ) e. K ) )
95 10 elnmz 
 |-  ( u e. N <-> ( u e. X /\ A. w e. X ( ( u .+ w ) e. K <-> ( w .+ u ) e. K ) ) )
96 35 94 95 sylanbrc 
 |-  ( ( ( ph /\ u e. X ) /\ ( u .(+) K ) = K ) -> u e. N )
97 34 96 impbida 
 |-  ( ( ph /\ u e. X ) -> ( u e. N <-> ( u .(+) K ) = K ) )
98 97 rabbi2dva 
 |-  ( ph -> ( X i^i N ) = { u e. X | ( u .(+) K ) = K } )
99 13 98 eqtr3id 
 |-  ( ph -> N = { u e. X | ( u .(+) K ) = K } )
100 9 99 eqtr4id 
 |-  ( ph -> H = N )