Theorem ablfac1a

Description: The factors of ablfac1b are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	ablfac1.b	$$⊢B={\mathrm{Base}}_G$$
	ablfac1.o	$$⊢O=\mathrm{od}\left(G\right)$$
	ablfac1.s	$$⊢S=\left(p\in A⟼\left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}\right)$$
	ablfac1.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablfac1.f	$$⊢\phi \to B\in \mathrm{Fin}$$
	ablfac1.1	$$⊢\phi \to A\subseteq \mathbb{P}$$
Assertion	ablfac1a	$$⊢\left(\phi \wedge P\in A\right)\to \left|S\left(P\right)\right|=P^{P\mathrm{pCnt}\left|B\right|}$$

Proof

Step	Hyp	Ref	Expression
1		ablfac1.b	$$⊢B={\mathrm{Base}}_G$$
2		ablfac1.o	$$⊢O=\mathrm{od}\left(G\right)$$
3		ablfac1.s	$$⊢S=\left(p\in A⟼\left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}\right)$$
4		ablfac1.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		ablfac1.f	$$⊢\phi \to B\in \mathrm{Fin}$$
6		ablfac1.1	$$⊢\phi \to A\subseteq \mathbb{P}$$
7		id	$$⊢p=P\to p=P$$
8		oveq1	$$⊢p=P\to p\mathrm{pCnt}\left|B\right|=P\mathrm{pCnt}\left|B\right|$$
9	7 8	oveq12d	$$⊢p=P\to p^{p\mathrm{pCnt}\left|B\right|}=P^{P\mathrm{pCnt}\left|B\right|}$$
10	9	breq2d	$$⊢p=P\to \left(O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\leftrightarrow O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right)$$
11	10	rabbidv	$$⊢p=P\to \left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}=\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}$$
12	1	fvexi	$$⊢B\in \mathrm{V}$$
13	12	rabex	$$⊢\left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}\in \mathrm{V}$$
14	11 3 13	fvmpt3i	$$⊢P\in A\to S\left(P\right)=\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}$$
15	14	adantl	$$⊢\left(\phi \wedge P\in A\right)\to S\left(P\right)=\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}$$
16	15	fveq2d	$$⊢\left(\phi \wedge P\in A\right)\to \left|S\left(P\right)\right|=\left|\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}\right|$$
17		eqid	$$⊢\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}=\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}$$
18		eqid	$$⊢\left\{x\in B|O\left(x\right)\parallel \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)\right\}=\left\{x\in B|O\left(x\right)\parallel \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)\right\}$$
19	4	adantr	$$⊢\left(\phi \wedge P\in A\right)\to G\in \mathrm{Abel}$$
20		eqid	$$⊢P^{P\mathrm{pCnt}\left|B\right|}=P^{P\mathrm{pCnt}\left|B\right|}$$
21		eqid	$$⊢\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}=\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}$$
22	1 2 3 4 5 6 20 21	ablfac1lem	$$⊢\left(\phi \wedge P\in A\right)\to \left(\left(P^{P\mathrm{pCnt}\left|B\right|}\in \mathbb{N}\wedge \frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\in \mathbb{N}\right)\wedge P^{P\mathrm{pCnt}\left|B\right|}\gcd \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)=1\wedge \left|B\right|=P^{P\mathrm{pCnt}\left|B\right|}\left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)\right)$$
23	22	simp1d	$$⊢\left(\phi \wedge P\in A\right)\to \left(P^{P\mathrm{pCnt}\left|B\right|}\in \mathbb{N}\wedge \frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\in \mathbb{N}\right)$$
24	23	simpld	$$⊢\left(\phi \wedge P\in A\right)\to P^{P\mathrm{pCnt}\left|B\right|}\in \mathbb{N}$$
25	23	simprd	$$⊢\left(\phi \wedge P\in A\right)\to \frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\in \mathbb{N}$$
26	22	simp2d	$$⊢\left(\phi \wedge P\in A\right)\to P^{P\mathrm{pCnt}\left|B\right|}\gcd \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)=1$$
27	22	simp3d	$$⊢\left(\phi \wedge P\in A\right)\to \left|B\right|=P^{P\mathrm{pCnt}\left|B\right|}\left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)$$
28	1 2 17 18 19 24 25 26 27	ablfacrp2	$$⊢\left(\phi \wedge P\in A\right)\to \left(\left|\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}\right|=P^{P\mathrm{pCnt}\left|B\right|}\wedge \left|\left\{x\in B|O\left(x\right)\parallel \left(\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)\right\}\right|=\frac{\left|B\right|}{P^{P\mathrm{pCnt}\left|B\right|}}\right)$$
29	28	simpld	$$⊢\left(\phi \wedge P\in A\right)\to \left|\left\{x\in B|O\left(x\right)\parallel P^{P\mathrm{pCnt}\left|B\right|}\right\}\right|=P^{P\mathrm{pCnt}\left|B\right|}$$
30	16 29	eqtrd	$$⊢\left(\phi \wedge P\in A\right)\to \left|S\left(P\right)\right|=P^{P\mathrm{pCnt}\left|B\right|}$$