Metamath Proof Explorer

Theorem sylow2b

Description: Sylow's second theorem. Any P -group H is a subgroup of a conjugated P -group K of order P ^ n || ( #X ) with n maximal. This is usually stated under the assumption that K is a Sylow subgroup, but we use a slightly different definition, whose equivalence to this one requires this theorem. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses sylow2b.x 
|- X = ( Base ` G )
sylow2b.xf 
|- ( ph -> X e. Fin )
sylow2b.h 
|- ( ph -> H e. ( SubGrp ` G ) )
sylow2b.k 
|- ( ph -> K e. ( SubGrp ` G ) )
sylow2b.a 
|- .+ = ( +g ` G )
sylow2b.hp 
|- ( ph -> P pGrp ( G |`s H ) )
sylow2b.kn 
|- ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
sylow2b.d 
|- .- = ( -g ` G )
Assertion sylow2b 
|- ( ph -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )

Proof

Step Hyp Ref Expression
1 sylow2b.x 
 |-  X = ( Base ` G )
2 sylow2b.xf 
 |-  ( ph -> X e. Fin )
3 sylow2b.h 
 |-  ( ph -> H e. ( SubGrp ` G ) )
4 sylow2b.k 
 |-  ( ph -> K e. ( SubGrp ` G ) )
5 sylow2b.a 
 |-  .+ = ( +g ` G )
6 sylow2b.hp 
 |-  ( ph -> P pGrp ( G |`s H ) )
7 sylow2b.kn 
 |-  ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
8 sylow2b.d 
 |-  .- = ( -g ` G )
9 eqid 
 |-  ( G ~QG K ) = ( G ~QG K )
10 oveq2 
 |-  ( s = z -> ( u .+ s ) = ( u .+ z ) )
11 10 cbvmptv 
 |-  ( s e. v |-> ( u .+ s ) ) = ( z e. v |-> ( u .+ z ) )
12 oveq1 
 |-  ( u = x -> ( u .+ z ) = ( x .+ z ) )
13 12 mpteq2dv 
 |-  ( u = x -> ( z e. v |-> ( u .+ z ) ) = ( z e. v |-> ( x .+ z ) ) )
14 11 13 eqtrid 
 |-  ( u = x -> ( s e. v |-> ( u .+ s ) ) = ( z e. v |-> ( x .+ z ) ) )
15 14 rneqd 
 |-  ( u = x -> ran ( s e. v |-> ( u .+ s ) ) = ran ( z e. v |-> ( x .+ z ) ) )
16 mpteq1 
 |-  ( v = y -> ( z e. v |-> ( x .+ z ) ) = ( z e. y |-> ( x .+ z ) ) )
17 16 rneqd 
 |-  ( v = y -> ran ( z e. v |-> ( x .+ z ) ) = ran ( z e. y |-> ( x .+ z ) ) )
18 15 17 cbvmpov 
 |-  ( u e. H , v e. ( X /. ( G ~QG K ) ) |-> ran ( s e. v |-> ( u .+ s ) ) ) = ( x e. H , y e. ( X /. ( G ~QG K ) ) |-> ran ( z e. y |-> ( x .+ z ) ) )
19 1 2 3 4 5 9 18 6 7 8 sylow2blem3 
 |-  ( ph -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )