Metamath Proof Explorer

Theorem pgphash

Description: The order of a p-group. (Contributed by Mario Carneiro, 27-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 pgpfi.1 
 |-  X = ( Base ` G )
2 simpl 
 |-  ( ( P pGrp G /\ X e. Fin ) -> P pGrp G )
3 pgpgrp 
 |-  ( P pGrp G -> G e. Grp )
4 1 pgpfi2 
 |-  ( ( G e. Grp /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
5 3 4 sylan 
 |-  ( ( P pGrp G /\ X e. Fin ) -> ( P pGrp G <-> ( P e. Prime /\ ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) ) )
6 2 5 mpbid 
 |-  ( ( P pGrp G /\ X e. Fin ) -> ( P e. Prime /\ ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) ) )
7 6 simprd 
 |-  ( ( P pGrp G /\ X e. Fin ) -> ( # ` X ) = ( P ^ ( P pCnt ( # ` X ) ) ) )