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

Metamath Proof Explorer

Theorem subgslw

Description: A Sylow subgroup that is contained in a larger subgroup is also Sylow with respect to the subgroup. (The converse need not be true.) (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypothesis subgslw.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
Assertion subgslw ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → 𝐾 ∈ ( 𝑃 pSyl 𝐻 ) )

Proof

Step Hyp Ref Expression
1 subgslw.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
2 slwprm ⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝑃 ∈ ℙ )
3 2 3ad2ant2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → 𝑃 ∈ ℙ )
4 slwsubg ⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
5 4 3ad2ant2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
6 simp3 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → 𝐾 ⊆ 𝑆 )
7 1 subsubg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐾 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
8 7 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → ( 𝐾 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ) )
9 5 6 8 mpbir2and ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → 𝐾 ∈ ( SubGrp ‘ 𝐻 ) )
10 1 oveq1i ⊢ ( 𝐻 ↾s 𝑥 ) = ( ( 𝐺 ↾s 𝑆 ) ↾s 𝑥 )
11 simpl1 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
12 1 subsubg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ⊆ 𝑆 ) ) )
13 12 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → ( 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ⊆ 𝑆 ) ) )
14 13 simplbda ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝑥 ⊆ 𝑆 )
15 ressabs ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ⊆ 𝑆 ) → ( ( 𝐺 ↾s 𝑆 ) ↾s 𝑥 ) = ( 𝐺 ↾s 𝑥 ) )
16 11 14 15 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → ( ( 𝐺 ↾s 𝑆 ) ↾s 𝑥 ) = ( 𝐺 ↾s 𝑥 ) )
17 10 16 eqtrid ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → ( 𝐻 ↾s 𝑥 ) = ( 𝐺 ↾s 𝑥 ) )
18 17 breq2d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → ( 𝑃 pGrp ( 𝐻 ↾s 𝑥 ) ↔ 𝑃 pGrp ( 𝐺 ↾s 𝑥 ) ) )
19 18 anbi2d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → ( ( 𝐾 ⊆ 𝑥 ∧ 𝑃 pGrp ( 𝐻 ↾s 𝑥 ) ) ↔ ( 𝐾 ⊆ 𝑥 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑥 ) ) ) )
20 simpl2 ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
21 13 simprbda ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → 𝑥 ∈ ( SubGrp ‘ 𝐺 ) )
22 eqid ⊢ ( 𝐺 ↾s 𝑥 ) = ( 𝐺 ↾s 𝑥 )
23 22 slwispgp ⊢ ( ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐾 ⊆ 𝑥 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑥 ) ) ↔ 𝐾 = 𝑥 ) )
24 20 21 23 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → ( ( 𝐾 ⊆ 𝑥 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑥 ) ) ↔ 𝐾 = 𝑥 ) )
25 19 24 bitrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ) → ( ( 𝐾 ⊆ 𝑥 ∧ 𝑃 pGrp ( 𝐻 ↾s 𝑥 ) ) ↔ 𝐾 = 𝑥 ) )
26 25 ralrimiva ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → ∀ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ( ( 𝐾 ⊆ 𝑥 ∧ 𝑃 pGrp ( 𝐻 ↾s 𝑥 ) ) ↔ 𝐾 = 𝑥 ) )
27 isslw ⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐻 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐾 ∈ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑥 ∈ ( SubGrp ‘ 𝐻 ) ( ( 𝐾 ⊆ 𝑥 ∧ 𝑃 pGrp ( 𝐻 ↾s 𝑥 ) ) ↔ 𝐾 = 𝑥 ) ) )
28 3 9 26 27 syl3anbrc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ⊆ 𝑆 ) → 𝐾 ∈ ( 𝑃 pSyl 𝐻 ) )