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

Metamath Proof Explorer

Theorem pgpprm

Description: Reverse closure for the first argument of pGrp . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Assertion pgpprm ⊢ P pGrp G → P ∈ ℙ

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base G = Base G
2 eqid ⊢ od ⁡ G = od ⁡ G
3 1 2 ispgp ⊢ P pGrp G ↔ P ∈ ℙ ∧ G ∈ Grp ∧ ∀ x ∈ Base G ∃ n ∈ ℕ 0 od ⁡ G ⁡ x = P n
4 3 simp1bi ⊢ P pGrp G → P ∈ ℙ