This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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