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