Metamath Proof Explorer

Theorem subgslw

Description: A Sylow subgroup that is contained in a larger subgroup is also Sylow with respect to the subgroup. (The converse need not be true.) (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypothesis subgslw.1 
|- H = ( G |`s S )
Assertion subgslw 
|- ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> K e. ( P pSyl H ) )

Proof

Step Hyp Ref Expression
1 subgslw.1 
 |-  H = ( G |`s S )
2 slwprm 
 |-  ( K e. ( P pSyl G ) -> P e. Prime )
3 2 3ad2ant2 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> P e. Prime )
4 slwsubg 
 |-  ( K e. ( P pSyl G ) -> K e. ( SubGrp ` G ) )
5 4 3ad2ant2 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> K e. ( SubGrp ` G ) )
6 simp3 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> K C_ S )
7 1 subsubg 
 |-  ( S e. ( SubGrp ` G ) -> ( K e. ( SubGrp ` H ) <-> ( K e. ( SubGrp ` G ) /\ K C_ S ) ) )
8 7 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> ( K e. ( SubGrp ` H ) <-> ( K e. ( SubGrp ` G ) /\ K C_ S ) ) )
9 5 6 8 mpbir2and 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> K e. ( SubGrp ` H ) )
10 1 oveq1i 
 |-  ( H |`s x ) = ( ( G |`s S ) |`s x )
11 simpl1 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> S e. ( SubGrp ` G ) )
12 1 subsubg 
 |-  ( S e. ( SubGrp ` G ) -> ( x e. ( SubGrp ` H ) <-> ( x e. ( SubGrp ` G ) /\ x C_ S ) ) )
13 12 3ad2ant1 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> ( x e. ( SubGrp ` H ) <-> ( x e. ( SubGrp ` G ) /\ x C_ S ) ) )
14 13 simplbda 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> x C_ S )
15 ressabs 
 |-  ( ( S e. ( SubGrp ` G ) /\ x C_ S ) -> ( ( G |`s S ) |`s x ) = ( G |`s x ) )
16 11 14 15 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> ( ( G |`s S ) |`s x ) = ( G |`s x ) )
17 10 16 eqtrid 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> ( H |`s x ) = ( G |`s x ) )
18 17 breq2d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> ( P pGrp ( H |`s x ) <-> P pGrp ( G |`s x ) ) )
19 18 anbi2d 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> ( ( K C_ x /\ P pGrp ( H |`s x ) ) <-> ( K C_ x /\ P pGrp ( G |`s x ) ) ) )
20 simpl2 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> K e. ( P pSyl G ) )
21 13 simprbda 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> x e. ( SubGrp ` G ) )
22 eqid 
 |-  ( G |`s x ) = ( G |`s x )
23 22 slwispgp 
 |-  ( ( K e. ( P pSyl G ) /\ x e. ( SubGrp ` G ) ) -> ( ( K C_ x /\ P pGrp ( G |`s x ) ) <-> K = x ) )
24 20 21 23 syl2anc 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> ( ( K C_ x /\ P pGrp ( G |`s x ) ) <-> K = x ) )
25 19 24 bitrd 
 |-  ( ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) /\ x e. ( SubGrp ` H ) ) -> ( ( K C_ x /\ P pGrp ( H |`s x ) ) <-> K = x ) )
26 25 ralrimiva 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> A. x e. ( SubGrp ` H ) ( ( K C_ x /\ P pGrp ( H |`s x ) ) <-> K = x ) )
27 isslw 
 |-  ( K e. ( P pSyl H ) <-> ( P e. Prime /\ K e. ( SubGrp ` H ) /\ A. x e. ( SubGrp ` H ) ( ( K C_ x /\ P pGrp ( H |`s x ) ) <-> K = x ) ) )
28 3 9 26 27 syl3anbrc 
 |-  ( ( S e. ( SubGrp ` G ) /\ K e. ( P pSyl G ) /\ K C_ S ) -> K e. ( P pSyl H ) )