Metamath Proof Explorer

Theorem pgpprm

Description: Reverse closure for the first argument of pGrp . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Assertion pgpprm 
|- ( P pGrp G -> P e. Prime )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( od ` G ) = ( od ` G )
3 1 2 ispgp 
 |-  ( P pGrp G <-> ( P e. Prime /\ G e. Grp /\ A. x e. ( Base ` G ) E. n e. NN0 ( ( od ` G ) ` x ) = ( P ^ n ) ) )
4 3 simp1bi 
 |-  ( P pGrp G -> P e. Prime )