Step |
Hyp |
Ref |
Expression |
1 |
|
pgpprm |
⊢ ( 𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ ) |
2 |
1
|
adantr |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 ∈ ℙ ) |
3 |
|
eqid |
⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 ) |
4 |
3
|
subggrp |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp ) |
5 |
4
|
adantl |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
7 |
|
eqid |
⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 ) |
8 |
6 7
|
ispgp |
⊢ ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
9 |
8
|
simp3bi |
⊢ ( 𝑃 pGrp 𝐺 → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) |
10 |
9
|
adantr |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) |
11 |
6
|
subgss |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
13 |
|
ssralv |
⊢ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
14 |
12 13
|
syl |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
15 |
|
eqid |
⊢ ( od ‘ ( 𝐺 ↾s 𝑆 ) ) = ( od ‘ ( 𝐺 ↾s 𝑆 ) ) |
16 |
3 7 15
|
subgod |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) ) |
17 |
16
|
adantll |
⊢ ( ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) ) |
18 |
17
|
eqeq1d |
⊢ ( ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
19 |
18
|
rexbidv |
⊢ ( ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
20 |
19
|
ralbidva |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ∀ 𝑥 ∈ 𝑆 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ↔ ∀ 𝑥 ∈ 𝑆 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
21 |
14 20
|
sylibd |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
22 |
10 21
|
mpd |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) |
23 |
3
|
subgbas |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
24 |
23
|
adantl |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) |
25 |
24
|
raleqdv |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ∀ 𝑥 ∈ 𝑆 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
26 |
22 25
|
mpbid |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) |
27 |
|
eqid |
⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) |
28 |
27 15
|
ispgp |
⊢ ( 𝑃 pGrp ( 𝐺 ↾s 𝑆 ) ↔ ( 𝑃 ∈ ℙ ∧ ( 𝐺 ↾s 𝑆 ) ∈ Grp ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) ) |
29 |
2 5 26 28
|
syl3anbrc |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑆 ) ) |