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 ) ) )