pgphash

Description: The order of a p-group. (Contributed by Mario Carneiro, 27-Apr-2016)

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

Step	Hyp	Ref	Expression
1		pgpfi.1	$⊢ X = {Base}_{G}$
2		simpl	$⊢ (P pGrp G \land X \in Fin) \to P pGrp G$
3		pgpgrp	$⊢ P pGrp G \to G \in Grp$
4	1	pgpfi2	$⊢ (G \in Grp \land X \in Fin) \to (P pGrp G \leftrightarrow (P \in ℙ \land \|X\| = P^{P pCnt \|X\|}))$
5	3 4	sylan	$⊢ (P pGrp G \land X \in Fin) \to (P pGrp G \leftrightarrow (P \in ℙ \land \|X\| = P^{P pCnt \|X\|}))$
6	2 5	mpbid	$⊢ (P pGrp G \land X \in Fin) \to (P \in ℙ \land \|X\| = P^{P pCnt \|X\|})$
7	6	simprd	$⊢ (P pGrp G \land X \in Fin) \to \|X\| = P^{P pCnt \|X\|}$

Metamath Proof Explorer