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

Metamath Proof Explorer

Theorem pgpfi2

Description: Alternate version of pgpfi . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypothesis pgpfi.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion pgpfi2 ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pgpfi.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 1 pgpfi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ) )
3 id ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℙ )
4 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
5 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
6 4 5 syl5ibrcom ⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ ) )
7 6 imp ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
8 pcprmpw ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
9 3 7 8 syl2anr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ 𝑃 ∈ ℙ ) → ( ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ↔ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) )
10 9 pm5.32da ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( ( 𝑃 ∈ ℙ ∧ ∃ 𝑛 ∈ ℕ0 ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ 𝑛 ) ) ↔ ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) )
11 2 10 bitrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝑃 pGrp 𝐺 ↔ ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝑋 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ) ) ) )