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	syl5eq	|- ( 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 ) ) )