Metamath Proof Explorer


Theorem isslw

Description: The property of being a Sylow subgroup. A Sylow P -subgroup is a P -group which has no proper supersets that are also P -groups. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Assertion isslw
|- ( H e. ( P pSyl G ) <-> ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) )

Proof

Step Hyp Ref Expression
1 df-slw
 |-  pSyl = ( p e. Prime , g e. Grp |-> { h e. ( SubGrp ` g ) | A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) } )
2 1 elmpocl
 |-  ( H e. ( P pSyl G ) -> ( P e. Prime /\ G e. Grp ) )
3 simp1
 |-  ( ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) -> P e. Prime )
4 subgrcl
 |-  ( H e. ( SubGrp ` G ) -> G e. Grp )
5 4 3ad2ant2
 |-  ( ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) -> G e. Grp )
6 3 5 jca
 |-  ( ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) -> ( P e. Prime /\ G e. Grp ) )
7 simpr
 |-  ( ( p = P /\ g = G ) -> g = G )
8 7 fveq2d
 |-  ( ( p = P /\ g = G ) -> ( SubGrp ` g ) = ( SubGrp ` G ) )
9 simpl
 |-  ( ( p = P /\ g = G ) -> p = P )
10 7 oveq1d
 |-  ( ( p = P /\ g = G ) -> ( g |`s k ) = ( G |`s k ) )
11 9 10 breq12d
 |-  ( ( p = P /\ g = G ) -> ( p pGrp ( g |`s k ) <-> P pGrp ( G |`s k ) ) )
12 11 anbi2d
 |-  ( ( p = P /\ g = G ) -> ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> ( h C_ k /\ P pGrp ( G |`s k ) ) ) )
13 12 bibi1d
 |-  ( ( p = P /\ g = G ) -> ( ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) <-> ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) ) )
14 8 13 raleqbidv
 |-  ( ( p = P /\ g = G ) -> ( A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) <-> A. k e. ( SubGrp ` G ) ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) ) )
15 8 14 rabeqbidv
 |-  ( ( p = P /\ g = G ) -> { h e. ( SubGrp ` g ) | A. k e. ( SubGrp ` g ) ( ( h C_ k /\ p pGrp ( g |`s k ) ) <-> h = k ) } = { h e. ( SubGrp ` G ) | A. k e. ( SubGrp ` G ) ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) } )
16 fvex
 |-  ( SubGrp ` G ) e. _V
17 16 rabex
 |-  { h e. ( SubGrp ` G ) | A. k e. ( SubGrp ` G ) ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) } e. _V
18 15 1 17 ovmpoa
 |-  ( ( P e. Prime /\ G e. Grp ) -> ( P pSyl G ) = { h e. ( SubGrp ` G ) | A. k e. ( SubGrp ` G ) ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) } )
19 18 eleq2d
 |-  ( ( P e. Prime /\ G e. Grp ) -> ( H e. ( P pSyl G ) <-> H e. { h e. ( SubGrp ` G ) | A. k e. ( SubGrp ` G ) ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) } ) )
20 cleq1lem
 |-  ( h = H -> ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> ( H C_ k /\ P pGrp ( G |`s k ) ) ) )
21 eqeq1
 |-  ( h = H -> ( h = k <-> H = k ) )
22 20 21 bibi12d
 |-  ( h = H -> ( ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) <-> ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) )
23 22 ralbidv
 |-  ( h = H -> ( A. k e. ( SubGrp ` G ) ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) <-> A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) )
24 23 elrab
 |-  ( H e. { h e. ( SubGrp ` G ) | A. k e. ( SubGrp ` G ) ( ( h C_ k /\ P pGrp ( G |`s k ) ) <-> h = k ) } <-> ( H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) )
25 19 24 bitrdi
 |-  ( ( P e. Prime /\ G e. Grp ) -> ( H e. ( P pSyl G ) <-> ( H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) ) )
26 simpl
 |-  ( ( P e. Prime /\ G e. Grp ) -> P e. Prime )
27 26 biantrurd
 |-  ( ( P e. Prime /\ G e. Grp ) -> ( ( H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) <-> ( P e. Prime /\ ( H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) ) ) )
28 25 27 bitrd
 |-  ( ( P e. Prime /\ G e. Grp ) -> ( H e. ( P pSyl G ) <-> ( P e. Prime /\ ( H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) ) ) )
29 3anass
 |-  ( ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) <-> ( P e. Prime /\ ( H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) ) )
30 28 29 bitr4di
 |-  ( ( P e. Prime /\ G e. Grp ) -> ( H e. ( P pSyl G ) <-> ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) ) )
31 2 6 30 pm5.21nii
 |-  ( H e. ( P pSyl G ) <-> ( P e. Prime /\ H e. ( SubGrp ` G ) /\ A. k e. ( SubGrp ` G ) ( ( H C_ k /\ P pGrp ( G |`s k ) ) <-> H = k ) ) )