Metamath Proof Explorer

Theorem slwispgp

Description: Defining property of a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis slwispgp.1 ⊢ S = G ↾ 𝑠 K
Assertion slwispgp ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G → H ⊆ K ∧ P pGrp S ↔ H = K

Proof

Step Hyp Ref Expression
1 slwispgp.1 ⊢ S = G ↾ 𝑠 K
2 isslw ⊢ H ∈ P pSyl G ↔ P ∈ ℙ ∧ H ∈ SubGrp ⁡ G ∧ ∀ k ∈ SubGrp ⁡ G H ⊆ k ∧ P pGrp G ↾ 𝑠 k ↔ H = k
3 2 simp3bi ⊢ H ∈ P pSyl G → ∀ k ∈ SubGrp ⁡ G H ⊆ k ∧ P pGrp G ↾ 𝑠 k ↔ H = k
4 sseq2 ⊢ k = K → H ⊆ k ↔ H ⊆ K
5 oveq2 ⊢ k = K → G ↾ 𝑠 k = G ↾ 𝑠 K
6 5 1 eqtr4di ⊢ k = K → G ↾ 𝑠 k = S
7 6 breq2d ⊢ k = K → P pGrp G ↾ 𝑠 k ↔ P pGrp S
8 4 7 anbi12d ⊢ k = K → H ⊆ k ∧ P pGrp G ↾ 𝑠 k ↔ H ⊆ K ∧ P pGrp S
9 eqeq2 ⊢ k = K → H = k ↔ H = K
10 8 9 bibi12d ⊢ k = K → H ⊆ k ∧ P pGrp G ↾ 𝑠 k ↔ H = k ↔ H ⊆ K ∧ P pGrp S ↔ H = K
11 10 rspccva ⊢ ∀ k ∈ SubGrp ⁡ G H ⊆ k ∧ P pGrp G ↾ 𝑠 k ↔ H = k ∧ K ∈ SubGrp ⁡ G → H ⊆ K ∧ P pGrp S ↔ H = K
12 3 11 sylan ⊢ H ∈ P pSyl G ∧ K ∈ SubGrp ⁡ G → H ⊆ K ∧ P pGrp S ↔ H = K