Theorem slwispgp

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

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

Proof

Step	Hyp	Ref	Expression
1		slwispgp.1	⊢ 𝑆 = ( 𝐺 ↾s 𝐾 )
2		isslw	⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ↔ ( 𝑃 ∈ ℙ ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ) )
3	2	simp3bi	⊢ ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) → ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) )
4		sseq2	⊢ ( 𝑘 = 𝐾 → ( 𝐻 ⊆ 𝑘 ↔ 𝐻 ⊆ 𝐾 ) )
5		oveq2	⊢ ( 𝑘 = 𝐾 → ( 𝐺 ↾s 𝑘 ) = ( 𝐺 ↾s 𝐾 ) )
6	5 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( 𝐺 ↾s 𝑘 ) = 𝑆 )
7	6	breq2d	⊢ ( 𝑘 = 𝐾 → ( 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ↔ 𝑃 pGrp 𝑆 ) )
8	4 7	anbi12d	⊢ ( 𝑘 = 𝐾 → ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ) )
9		eqeq2	⊢ ( 𝑘 = 𝐾 → ( 𝐻 = 𝑘 ↔ 𝐻 = 𝐾 ) )
10	8 9	bibi12d	⊢ ( 𝑘 = 𝐾 → ( ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ↔ ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) ) )
11	10	rspccva	⊢ ( ( ∀ 𝑘 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp ( 𝐺 ↾s 𝑘 ) ) ↔ 𝐻 = 𝑘 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) )
12	3 11	sylan	⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) )