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

Metamath Proof Explorer

Theorem ispgp

Description: A group is a P -group if every element has some power of P as its order. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses ispgp.1 
|- X = ( Base ` G )
ispgp.2 
|- O = ( od ` G )
Assertion ispgp 
|- ( P pGrp G <-> ( P e. Prime /\ G e. Grp /\ A. x e. X E. n e. NN0 ( O ` x ) = ( P ^ n ) ) )

Proof

Step Hyp Ref Expression
1 ispgp.1 
 |-  X = ( Base ` G )
2 ispgp.2 
 |-  O = ( od ` G )
3 simpr 
 |-  ( ( p = P /\ g = G ) -> g = G )
4 3 fveq2d 
 |-  ( ( p = P /\ g = G ) -> ( Base ` g ) = ( Base ` G ) )
5 4 1 eqtr4di 
 |-  ( ( p = P /\ g = G ) -> ( Base ` g ) = X )
6 3 fveq2d 
 |-  ( ( p = P /\ g = G ) -> ( od ` g ) = ( od ` G ) )
7 6 2 eqtr4di 
 |-  ( ( p = P /\ g = G ) -> ( od ` g ) = O )
8 7 fveq1d 
 |-  ( ( p = P /\ g = G ) -> ( ( od ` g ) ` x ) = ( O ` x ) )
9 simpl 
 |-  ( ( p = P /\ g = G ) -> p = P )
10 9 oveq1d 
 |-  ( ( p = P /\ g = G ) -> ( p ^ n ) = ( P ^ n ) )
11 8 10 eqeq12d 
 |-  ( ( p = P /\ g = G ) -> ( ( ( od ` g ) ` x ) = ( p ^ n ) <-> ( O ` x ) = ( P ^ n ) ) )
12 11 rexbidv 
 |-  ( ( p = P /\ g = G ) -> ( E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) <-> E. n e. NN0 ( O ` x ) = ( P ^ n ) ) )
13 5 12 raleqbidv 
 |-  ( ( p = P /\ g = G ) -> ( A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) <-> A. x e. X E. n e. NN0 ( O ` x ) = ( P ^ n ) ) )
14 df-pgp 
 |-  pGrp = { <. p , g >. | ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) ) }
15 13 14 brab2a 
 |-  ( P pGrp G <-> ( ( P e. Prime /\ G e. Grp ) /\ A. x e. X E. n e. NN0 ( O ` x ) = ( P ^ n ) ) )
16 df-3an 
 |-  ( ( P e. Prime /\ G e. Grp /\ A. x e. X E. n e. NN0 ( O ` x ) = ( P ^ n ) ) <-> ( ( P e. Prime /\ G e. Grp ) /\ A. x e. X E. n e. NN0 ( O ` x ) = ( P ^ n ) ) )
17 15 16 bitr4i 
 |-  ( P pGrp G <-> ( P e. Prime /\ G e. Grp /\ A. x e. X E. n e. NN0 ( O ` x ) = ( P ^ n ) ) )