Step |
Hyp |
Ref |
Expression |
1 |
|
slwispgp.1 |
⊢ 𝑆 = ( 𝐺 ↾s 𝐾 ) |
2 |
|
simp3 |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ⊊ 𝐾 ) |
3 |
2
|
pssned |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ≠ 𝐾 ) |
4 |
2
|
pssssd |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → 𝐻 ⊆ 𝐾 ) |
5 |
4
|
biantrurd |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( 𝑃 pGrp 𝑆 ↔ ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ) ) |
6 |
1
|
slwispgp |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) ) |
7 |
6
|
3adant3 |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( ( 𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆 ) ↔ 𝐻 = 𝐾 ) ) |
8 |
5 7
|
bitrd |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( 𝑃 pGrp 𝑆 ↔ 𝐻 = 𝐾 ) ) |
9 |
8
|
necon3bbid |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ( ¬ 𝑃 pGrp 𝑆 ↔ 𝐻 ≠ 𝐾 ) ) |
10 |
3 9
|
mpbird |
⊢ ( ( 𝐻 ∈ ( 𝑃 pSyl 𝐺 ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐻 ⊊ 𝐾 ) → ¬ 𝑃 pGrp 𝑆 ) |