This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pgpfi1

Description: A finite group with order a power of a prime P is a P -group. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Hypothesis pgpfi1.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion pgpfi1 ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) → 𝑃 pGrp 𝐺 ) )

Proof

Step Hyp Ref Expression
1 pgpfi1.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → 𝑃 ∈ ℙ )
3 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → 𝐺 ∈ Grp )
4 simpll3 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑁 ∈ ℕ0 )
5 3 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐺 ∈ Grp )
6 simplr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) )
7 2 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ ℙ )
8 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
9 7 8 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ ℕ )
10 9 4 nnexpcld ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 ↑ 𝑁 ) ∈ ℕ )
11 10 nnnn0d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 ↑ 𝑁 ) ∈ ℕ0 )
12 6 11 eqeltrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
13 1 fvexi ⊢ 𝑋 ∈ V
14 hashclb ⊢ ( 𝑋 ∈ V → ( 𝑋 ∈ Fin ↔ ( ♯ ‘ 𝑋 ) ∈ ℕ0 ) )
15 13 14 ax-mp ⊢ ( 𝑋 ∈ Fin ↔ ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
16 12 15 sylibr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ Fin )
17 simpr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
18 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
19 1 18 oddvds2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
20 5 16 17 19 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
21 20 6 breqtrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑁 ) )
22 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑁 ) )
23 22 breq2d ⊢ ( 𝑛 = 𝑁 → ( ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑁 ) ) )
24 23 rspcev ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) )
25 4 21 24 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) )
26 1 18 odcl2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ )
27 5 16 17 26 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ )
28 pcprmpw2 ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
29 pcprmpw ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
30 28 29 bitr4d ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
31 7 27 30 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
32 25 31 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) )
33 32 ralrimiva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) )
34 1 18 ispgp ⊢ ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑃 ↑ 𝑛 ) ) )
35 2 3 33 34 syl3anbrc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) ) → 𝑃 pGrp 𝐺 )
36 35 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑁 ) → 𝑃 pGrp 𝐺 ) )