Metamath Proof Explorer

Theorem subgpgp

Description: A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Assertion subgpgp ( ( 𝑃 pGrp 𝐺 ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑆 ) )

Proof

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 𝑆 ) )