MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pgp Structured version   Visualization version   GIF version

Definition df-pgp 17871
Description: Define the set of p-groups, which are groups such that every element has a power of 𝑝 as its order. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by AV, 5-Oct-2020.)
Assertion
Ref Expression
df-pgp pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛))}
Distinct variable group:   𝑔,𝑛,𝑝,𝑥

Detailed syntax breakdown of Definition df-pgp
StepHypRef Expression
1 cpgp 17867 . 2 class pGrp
2 vp . . . . . . 7 setvar 𝑝
32cv 1479 . . . . . 6 class 𝑝
4 cprime 15309 . . . . . 6 class
53, 4wcel 1987 . . . . 5 wff 𝑝 ∈ ℙ
6 vg . . . . . . 7 setvar 𝑔
76cv 1479 . . . . . 6 class 𝑔
8 cgrp 17343 . . . . . 6 class Grp
97, 8wcel 1987 . . . . 5 wff 𝑔 ∈ Grp
105, 9wa 384 . . . 4 wff (𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp)
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1479 . . . . . . . 8 class 𝑥
13 cod 17865 . . . . . . . . 9 class od
147, 13cfv 5847 . . . . . . . 8 class (od‘𝑔)
1512, 14cfv 5847 . . . . . . 7 class ((od‘𝑔)‘𝑥)
16 vn . . . . . . . . 9 setvar 𝑛
1716cv 1479 . . . . . . . 8 class 𝑛
18 cexp 12800 . . . . . . . 8 class
193, 17, 18co 6604 . . . . . . 7 class (𝑝𝑛)
2015, 19wceq 1480 . . . . . 6 wff ((od‘𝑔)‘𝑥) = (𝑝𝑛)
21 cn0 11236 . . . . . 6 class 0
2220, 16, 21wrex 2908 . . . . 5 wff 𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛)
23 cbs 15781 . . . . . 6 class Base
247, 23cfv 5847 . . . . 5 class (Base‘𝑔)
2522, 11, 24wral 2907 . . . 4 wff 𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛)
2610, 25wa 384 . . 3 wff ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛))
2726, 2, 6copab 4672 . 2 class {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛))}
281, 27wceq 1480 1 wff pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛))}
Colors of variables: wff setvar class
This definition is referenced by:  ispgp  17928
  Copyright terms: Public domain W3C validator