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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow2b.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow2b.h	⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
	sylow2b.k	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
	sylow2b.a	⊢ + = ( +g ‘ 𝐺 )
	sylow2b.hp	⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) )
	sylow2b.kn	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
	sylow2b.d	⊢ − = ( -g ‘ 𝐺 )
Assertion	sylow2b	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sylow2b.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow2b.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		sylow2b.h	⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
4		sylow2b.k	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
5		sylow2b.a	⊢ + = ( +g ‘ 𝐺 )
6		sylow2b.hp	⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾s 𝐻 ) )
7		sylow2b.kn	⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) )
8		sylow2b.d	⊢ − = ( -g ‘ 𝐺 )
9		eqid	⊢ ( 𝐺 ~QG 𝐾 ) = ( 𝐺 ~QG 𝐾 )
10		oveq2	⊢ ( 𝑠 = 𝑧 → ( 𝑢 + 𝑠 ) = ( 𝑢 + 𝑧 ) )
11	10	cbvmptv	⊢ ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 + 𝑠 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑢 + 𝑧 ) )
12		oveq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 + 𝑧 ) = ( 𝑥 + 𝑧 ) )
13	12	mpteq2dv	⊢ ( 𝑢 = 𝑥 → ( 𝑧 ∈ 𝑣 ↦ ( 𝑢 + 𝑧 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 + 𝑧 ) ) )
14	11 13	eqtrid	⊢ ( 𝑢 = 𝑥 → ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 + 𝑠 ) ) = ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 + 𝑧 ) ) )
15	14	rneqd	⊢ ( 𝑢 = 𝑥 → ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 + 𝑠 ) ) = ran ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 + 𝑧 ) ) )
16		mpteq1	⊢ ( 𝑣 = 𝑦 → ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
17	16	rneqd	⊢ ( 𝑣 = 𝑦 → ran ( 𝑧 ∈ 𝑣 ↦ ( 𝑥 + 𝑧 ) ) = ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
18	15 17	cbvmpov	⊢ ( 𝑢 ∈ 𝐻 , 𝑣 ∈ ( 𝑋 / ( 𝐺 ~QG 𝐾 ) ) ↦ ran ( 𝑠 ∈ 𝑣 ↦ ( 𝑢 + 𝑠 ) ) ) = ( 𝑥 ∈ 𝐻 , 𝑦 ∈ ( 𝑋 / ( 𝐺 ~QG 𝐾 ) ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
19	1 2 3 4 5 9 18 6 7 8	sylow2blem3	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝑋 𝐻 ⊆ ran ( 𝑥 ∈ 𝐾 ↦ ( ( 𝑔 + 𝑥 ) − 𝑔 ) ) )