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 ( ♯ ‘ 𝑋 ) ) ) ) ) )