This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Groups p-Groups and Sylow groups; Sylow's theorems 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 ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od g x = p n
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cpgp class pGrp
1
vp setvar p
2
vg setvar g
3
1
cv setvar p
4
cprime class ℙ
5
3 4
wcel wff p ∈ ℙ
6
2
cv setvar g
7
cgrp class Grp
8
6 7
wcel wff g ∈ Grp
9
5 8
wa wff p ∈ ℙ ∧ g ∈ Grp
10
vx setvar x
11
cbs class Base
12
6 11
cfv class Base g
13
vn setvar n
14
cn0 class ℕ 0
15
cod class od
16
6 15
cfv class od g
17
10
cv setvar x
18
17 16
cfv class od g x
19
cexp class ^
20
13
cv setvar n
21
3 20 19
co class p n
22
18 21
wceq wff od g x = p n
23
22 13 14
wrex wff ∃ n ∈ ℕ 0 od g x = p n
24
23 10 12
wral wff ∀ x ∈ Base g ∃ n ∈ ℕ 0 od g x = p n
25
9 24
wa wff p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od g x = p n
26
25 1 2
copab class p g | p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od g x = p n
27
0 26
wceq wff pGrp = p g | p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od g x = p n