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 = { ⟨ 𝑝 , 𝑔 ⟩ ∣ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝𝑛 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpgp pGrp
1 vp 𝑝
2 vg 𝑔
3 1 cv 𝑝
4 cprime
5 3 4 wcel 𝑝 ∈ ℙ
6 2 cv 𝑔
7 cgrp Grp
8 6 7 wcel 𝑔 ∈ Grp
9 5 8 wa ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp )
10 vx 𝑥
11 cbs Base
12 6 11 cfv ( Base ‘ 𝑔 )
13 vn 𝑛
14 cn0 0
15 cod od
16 6 15 cfv ( od ‘ 𝑔 )
17 10 cv 𝑥
18 17 16 cfv ( ( od ‘ 𝑔 ) ‘ 𝑥 )
19 cexp
20 13 cv 𝑛
21 3 20 19 co ( 𝑝𝑛 )
22 18 21 wceq ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝𝑛 )
23 22 13 14 wrex 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝𝑛 )
24 23 10 12 wral 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝𝑛 )
25 9 24 wa ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝𝑛 ) )
26 25 1 2 copab { ⟨ 𝑝 , 𝑔 ⟩ ∣ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝𝑛 ) ) }
27 0 26 wceq pGrp = { ⟨ 𝑝 , 𝑔 ⟩ ∣ ( ( 𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ∃ 𝑛 ∈ ℕ0 ( ( od ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝𝑛 ) ) }