Metamath Proof Explorer

Definition df-pgp

Description: Define the set of p-groups, which are groups such that every element has a power of p as its order. (Contributed by Mario Carneiro, 15-Jan-2015) (Revised by AV, 5-Oct-2020)

Ref Expression
Assertion 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpgp 
 |-  pGrp
1 vp 
 |-  p
2 vg 
 |-  g
3 1 cv 
 |-  p
4 cprime 
 |-  Prime
5 3 4 wcel 
 |-  p e. Prime
6 2 cv 
 |-  g
7 cgrp 
 |-  Grp
8 6 7 wcel 
 |-  g e. Grp
9 5 8 wa 
 |-  ( p e. Prime /\ g e. Grp )
10 vx 
 |-  x
11 cbs 
 |-  Base
12 6 11 cfv 
 |-  ( Base ` g )
13 vn 
 |-  n
14 cn0 
 |-  NN0
15 cod 
 |-  od
16 6 15 cfv 
 |-  ( od ` g )
17 10 cv 
 |-  x
18 17 16 cfv 
 |-  ( ( od ` g ) ` x )
19 cexp 
 |-  ^
20 13 cv 
 |-  n
21 3 20 19 co 
 |-  ( p ^ n )
22 18 21 wceq 
 |-  ( ( od ` g ) ` x ) = ( p ^ n )
23 22 13 14 wrex 
 |-  E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n )
24 23 10 12 wral 
 |-  A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n )
25 9 24 wa 
 |-  ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) )
26 25 1 2 copab 
 |-  { <. p , g >. | ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) ) }
27 0 26 wceq 
 |-  pGrp = { <. p , g >. | ( ( p e. Prime /\ g e. Grp ) /\ A. x e. ( Base ` g ) E. n e. NN0 ( ( od ` g ) ` x ) = ( p ^ n ) ) }