Metamath Proof Explorer

Theorem pgpfi2

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

Ref Expression
Hypothesis pgpfi.1 
|- X = ( Base ` G )
Assertion pgpfi2 
|- ( ( G e. Grp /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pgpfi.1 
 |-  X = ( Base ` G )
2 1 pgpfi 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ E. n e. NN0 ( # ` X ) = ( P ^ n ) ) ) )
3 id 
 |-  ( P e. Prime -> P e. Prime )
4 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
5 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
6 4 5 syl5ibrcom 
 |-  ( G e. Grp -> ( X e. Fin -> ( # ` X ) e. NN ) )
7 6 imp 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( # ` X ) e. NN )
8 pcprmpw 
 |-  ( ( P e. Prime /\ ( # ` X ) e. NN ) -> ( E. n e. NN0 ( # ` X ) = ( P ^ n ) <-> ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) )
9 3 7 8 syl2anr 
 |-  ( ( ( G e. Grp /\ X e. Fin ) /\ P e. Prime ) -> ( E. n e. NN0 ( # ` X ) = ( P ^ n ) <-> ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) )
10 9 pm5.32da 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( ( P e. Prime /\ E. n e. NN0 ( # ` X ) = ( P ^ n ) ) <-> ( P e. Prime /\ ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
11 2 10 bitrd 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )