pgpfi2

Description: Alternate version of pgpfi . (Contributed by Mario Carneiro, 27-Apr-2016)

		Ref	Expression
	Hypothesis	pgpfi.1	$⊢ X = {Base}_{G}$
	Assertion	pgpfi2	$⊢ (G \in Grp \land X \in Fin) \to (P pGrp G \leftrightarrow (P \in ℙ \land \|X\| = P^{P pCnt \|X\|}))$

Step	Hyp	Ref	Expression
1		pgpfi.1	$⊢ X = {Base}_{G}$
2	1	pgpfi	$⊢ (G \in Grp \land X \in Fin) \to (P pGrp G \leftrightarrow (P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}))$
3		id	$⊢ P \in ℙ \to P \in ℙ$
4	1	grpbn0	$⊢ G \in Grp \to X \neq \emptyset$
5		hashnncl	$⊢ X \in Fin \to (\|X\| \in ℕ \leftrightarrow X \neq \emptyset)$
6	4 5	syl5ibrcom	$⊢ G \in Grp \to (X \in Fin \to \|X\| \in ℕ)$
7	6	imp	$⊢ (G \in Grp \land X \in Fin) \to \|X\| \in ℕ$
8		pcprmpw	$⊢ (P \in ℙ \land \|X\| \in ℕ) \to (\exists n \in ℕ_{0} \|X\| = P^{n} \leftrightarrow \|X\| = P^{P pCnt \|X\|})$
9	3 7 8	syl2anr	$⊢ ((G \in Grp \land X \in Fin) \land P \in ℙ) \to (\exists n \in ℕ_{0} \|X\| = P^{n} \leftrightarrow \|X\| = P^{P pCnt \|X\|})$
10	9	pm5.32da	$⊢ (G \in Grp \land X \in Fin) \to ((P \in ℙ \land \exists n \in ℕ_{0} \|X\| = P^{n}) \leftrightarrow (P \in ℙ \land \|X\| = P^{P pCnt \|X\|}))$
11	2 10	bitrd	$⊢ (G \in Grp \land X \in Fin) \to (P pGrp G \leftrightarrow (P \in ℙ \land \|X\| = P^{P pCnt \|X\|}))$

Metamath Proof Explorer