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 P pSyl G P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k

Proof

Step Hyp Ref Expression
1 df-slw pSyl = p , g Grp h SubGrp g | k SubGrp g h k p pGrp g 𝑠 k h = k
2 1 elmpocl H P pSyl G P G Grp
3 simp1 P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k P
4 subgrcl H SubGrp G G Grp
5 4 3ad2ant2 P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k G Grp
6 3 5 jca P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k P G 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 𝑠 k = G 𝑠 k
11 9 10 breq12d p = P g = G p pGrp g 𝑠 k P pGrp G 𝑠 k
12 11 anbi2d p = P g = G h k p pGrp g 𝑠 k h k P pGrp G 𝑠 k
13 12 bibi1d p = P g = G h k p pGrp g 𝑠 k h = k h k P pGrp G 𝑠 k h = k
14 8 13 raleqbidv p = P g = G k SubGrp g h k p pGrp g 𝑠 k h = k k SubGrp G h k P pGrp G 𝑠 k h = k
15 8 14 rabeqbidv p = P g = G h SubGrp g | k SubGrp g h k p pGrp g 𝑠 k h = k = h SubGrp G | k SubGrp G h k P pGrp G 𝑠 k h = k
16 fvex SubGrp G V
17 16 rabex h SubGrp G | k SubGrp G h k P pGrp G 𝑠 k h = k V
18 15 1 17 ovmpoa P G Grp P pSyl G = h SubGrp G | k SubGrp G h k P pGrp G 𝑠 k h = k
19 18 eleq2d P G Grp H P pSyl G H h SubGrp G | k SubGrp G h k P pGrp G 𝑠 k h = k
20 cleq1lem h = H h k P pGrp G 𝑠 k H k P pGrp G 𝑠 k
21 eqeq1 h = H h = k H = k
22 20 21 bibi12d h = H h k P pGrp G 𝑠 k h = k H k P pGrp G 𝑠 k H = k
23 22 ralbidv h = H k SubGrp G h k P pGrp G 𝑠 k h = k k SubGrp G H k P pGrp G 𝑠 k H = k
24 23 elrab H h SubGrp G | k SubGrp G h k P pGrp G 𝑠 k h = k H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k
25 19 24 bitrdi P G Grp H P pSyl G H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k
26 simpl P G Grp P
27 26 biantrurd P G Grp H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k
28 25 27 bitrd P G Grp H P pSyl G P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k
29 3anass P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k
30 28 29 bitr4di P G Grp H P pSyl G P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k
31 2 6 30 pm5.21nii H P pSyl G P H SubGrp G k SubGrp G H k P pGrp G 𝑠 k H = k