Metamath Proof Explorer

Theorem ispgp

Description: A group is a P -group if every element has some power of P as its order. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses ispgp.1 ⊢ X = Base G
ispgp.2 ⊢ O = od ⁡ G
Assertion ispgp ⊢ P pGrp G ↔ P ∈ ℙ ∧ G ∈ Grp ∧ ∀ x ∈ X ∃ n ∈ ℕ 0 O ⁡ x = P n

Proof

Step Hyp Ref Expression
1 ispgp.1 ⊢ X = Base G
2 ispgp.2 ⊢ O = od ⁡ G
3 simpr ⊢ p = P ∧ g = G → g = G
4 3 fveq2d ⊢ p = P ∧ g = G → Base g = Base G
5 4 1 eqtr4di ⊢ p = P ∧ g = G → Base g = X
6 3 fveq2d ⊢ p = P ∧ g = G → od ⁡ g = od ⁡ G
7 6 2 eqtr4di ⊢ p = P ∧ g = G → od ⁡ g = O
8 7 fveq1d ⊢ p = P ∧ g = G → od ⁡ g ⁡ x = O ⁡ x
9 simpl ⊢ p = P ∧ g = G → p = P
10 9 oveq1d ⊢ p = P ∧ g = G → p n = P n
11 8 10 eqeq12d ⊢ p = P ∧ g = G → od ⁡ g ⁡ x = p n ↔ O ⁡ x = P n
12 11 rexbidv ⊢ p = P ∧ g = G → ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n ↔ ∃ n ∈ ℕ 0 O ⁡ x = P n
13 5 12 raleqbidv ⊢ p = P ∧ g = G → ∀ x ∈ Base g ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n ↔ ∀ x ∈ X ∃ n ∈ ℕ 0 O ⁡ x = P n
14 df-pgp ⊢ pGrp = p g | p ∈ ℙ ∧ g ∈ Grp ∧ ∀ x ∈ Base g ∃ n ∈ ℕ 0 od ⁡ g ⁡ x = p n
15 13 14 brab2a ⊢ P pGrp G ↔ P ∈ ℙ ∧ G ∈ Grp ∧ ∀ x ∈ X ∃ n ∈ ℕ 0 O ⁡ x = P n
16 df-3an ⊢ P ∈ ℙ ∧ G ∈ Grp ∧ ∀ x ∈ X ∃ n ∈ ℕ 0 O ⁡ x = P n ↔ P ∈ ℙ ∧ G ∈ Grp ∧ ∀ x ∈ X ∃ n ∈ ℕ 0 O ⁡ x = P n
17 15 16 bitr4i ⊢ P pGrp G ↔ P ∈ ℙ ∧ G ∈ Grp ∧ ∀ x ∈ X ∃ n ∈ ℕ 0 O ⁡ x = P n