Description: Sylow's second theorem. Putting together the results of sylow2a and the orbit-stabilizer theorem to show that P does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some g e. X with h g K = g K for all h e. H . This implies that invg ( g ) h g e. K , so h is in the conjugated subgroup g K invg ( g ) . (Contributed by Mario Carneiro, 18-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sylow2b.x | |
|
sylow2b.xf | |
||
sylow2b.h | |
||
sylow2b.k | |
||
sylow2b.a | |
||
sylow2b.r | |
||
sylow2b.m | |
||
sylow2blem3.hp | |
||
sylow2blem3.kn | |
||
sylow2blem3.d | |
||
Assertion | sylow2blem3 | |