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