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

Definition df-pgp 18740
 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 18736 . 2 class pGrp
2 vp . . . . . . 7 setvar 𝑝
32cv 1538 . . . . . 6 class 𝑝
4 cprime 16082 . . . . . 6 class
53, 4wcel 2112 . . . . 5 wff 𝑝 ∈ ℙ
6 vg . . . . . . 7 setvar 𝑔
76cv 1538 . . . . . 6 class 𝑔
8 cgrp 18184 . . . . . 6 class Grp
97, 8wcel 2112 . . . . 5 wff 𝑔 ∈ Grp
105, 9wa 399 . . . 4 wff (𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp)
11 vx . . . . . . . . 9 setvar 𝑥
1211cv 1538 . . . . . . . 8 class 𝑥
13 cod 18734 . . . . . . . . 9 class od
147, 13cfv 6341 . . . . . . . 8 class (od‘𝑔)
1512, 14cfv 6341 . . . . . . 7 class ((od‘𝑔)‘𝑥)
16 vn . . . . . . . . 9 setvar 𝑛
1716cv 1538 . . . . . . . 8 class 𝑛
18 cexp 13493 . . . . . . . 8 class
193, 17, 18co 7157 . . . . . . 7 class (𝑝𝑛)
2015, 19wceq 1539 . . . . . 6 wff ((od‘𝑔)‘𝑥) = (𝑝𝑛)
21 cn0 11948 . . . . . 6 class 0
2220, 16, 21wrex 3072 . . . . 5 wff 𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛)
23 cbs 16556 . . . . . 6 class Base
247, 23cfv 6341 . . . . 5 class (Base‘𝑔)
2522, 11, 24wral 3071 . . . 4 wff 𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛)
2610, 25wa 399 . . 3 wff ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛))
2726, 2, 6copab 5099 . 2 class {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛))}
281, 27wceq 1539 1 wff pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝𝑛))}
 Colors of variables: wff setvar class This definition is referenced by:  ispgp  18799
 Copyright terms: Public domain W3C validator