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 ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 df-slw pSyl = ( 𝑝 ∈ ℙ , 𝑔 ∈ Grp ↦ { ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( 𝑘𝑝 pGrp ( 𝑔s 𝑘 ) ) ↔ = 𝑘 ) } )
2 1 elmpocl ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) )
3 simp1 ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) → 𝑃 ∈ ℙ )
4 subgrcl ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
5 4 3ad2ant2 ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) → 𝐺 ∈ Grp )
6 3 5 jca ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) → ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) )
7 simpr ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
8 7 fveq2d ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → ( SubGrp ‘ 𝑔 ) = ( SubGrp ‘ 𝐺 ) )
9 simpl ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → 𝑝 = 𝑃 )
10 7 oveq1d ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → ( 𝑔s 𝑘 ) = ( 𝐺s 𝑘 ) )
11 9 10 breq12d ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → ( 𝑝 pGrp ( 𝑔s 𝑘 ) ↔ 𝑃 pGrp ( 𝐺s 𝑘 ) ) )
12 11 anbi2d ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → ( ( 𝑘𝑝 pGrp ( 𝑔s 𝑘 ) ) ↔ ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ) )
13 12 bibi1d ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → ( ( ( 𝑘𝑝 pGrp ( 𝑔s 𝑘 ) ) ↔ = 𝑘 ) ↔ ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) ) )
14 8 13 raleqbidv ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → ( ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( 𝑘𝑝 pGrp ( 𝑔s 𝑘 ) ) ↔ = 𝑘 ) ↔ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) ) )
15 8 14 rabeqbidv ( ( 𝑝 = 𝑃𝑔 = 𝐺 ) → { ∈ ( SubGrp ‘ 𝑔 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝑔 ) ( ( 𝑘𝑝 pGrp ( 𝑔s 𝑘 ) ) ↔ = 𝑘 ) } = { ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) } )
16 fvex ( SubGrp ‘ 𝐺 ) ∈ V
17 16 rabex { ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) } ∈ V
18 15 1 17 ovmpoa ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝑃 pSyl 𝐺 ) = { ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) } )
19 18 eleq2d ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ 𝐻 ∈ { ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) } ) )
20 cleq1lem ( = 𝐻 → ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ) )
21 eqeq1 ( = 𝐻 → ( = 𝑘𝐻 = 𝑘 ) )
22 20 21 bibi12d ( = 𝐻 → ( ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) ↔ ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
23 22 ralbidv ( = 𝐻 → ( ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) ↔ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
24 23 elrab ( 𝐻 ∈ { ∈ ( SubGrp ‘ 𝐺 ) ∣ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ = 𝑘 ) } ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
25 19 24 bitrdi ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) )
26 simpl ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → 𝑃 ∈ ℙ )
27 26 biantrurd ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ↔ ( 𝑃 ∈ ℙ ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) ) )
28 25 27 bitrd ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) ) )
29 3anass ( ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ↔ ( 𝑃 ∈ ℙ ∧ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) )
30 28 29 bitr4di ( ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ) → ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) ) )
31 2 6 30 pm5.21nii ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻𝑘𝑃 pGrp ( 𝐺s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )