This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑔 ) ‘ 𝑥 ) = ( 𝑝 ↑ 𝑛 ) ) }