Theorem pgphash

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

	Ref	Expression
Hypothesis	pgpfi.1	$$⊢X={\mathrm{Base}}_G$$
Assertion	pgphash	$$⊢\left(P\mathrm{pGrp}G\wedge X\in \mathrm{Fin}\right)\to \left|X\right|=P^{P\mathrm{pCnt}\left|X\right|}$$

Proof

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