Theorem ablfac1a

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

	Ref	Expression
Hypotheses	ablfac1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablfac1.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	ablfac1.s	⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
	ablfac1.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablfac1.f	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	ablfac1.1	⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
Assertion	ablfac1a	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑆 ‘ 𝑃 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ablfac1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablfac1.o	⊢ 𝑂 = ( od ‘ 𝐺 )
3		ablfac1.s	⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
4		ablfac1.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
5		ablfac1.f	⊢ ( 𝜑 → 𝐵 ∈ Fin )
6		ablfac1.1	⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
7		id	⊢ ( 𝑝 = 𝑃 → 𝑝 = 𝑃 )
8		oveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) = ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) )
9	7 8	oveq12d	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )
10	9	breq2d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) )
11	10	rabbidv	⊢ ( 𝑝 = 𝑃 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
12	1	fvexi	⊢ 𝐵 ∈ V
13	12	rabex	⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ V
14	11 3 13	fvmpt3i	⊢ ( 𝑃 ∈ 𝐴 → ( 𝑆 ‘ 𝑃 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑃 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
16	15	fveq2d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑆 ‘ 𝑃 ) ) = ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) )
17		eqid	⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) }
18		eqid	⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) }
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → 𝐺 ∈ Abel )
20		eqid	⊢ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) )
21		eqid	⊢ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )
22	1 2 3 4 5 6 20 21	ablfac1lem	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℕ ) ∧ ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) = 1 ∧ ( ♯ ‘ 𝐵 ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) ) )
23	22	simp1d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℕ ) )
24	23	simpld	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ )
25	23	simprd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℕ )
26	22	simp2d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) = 1 )
27	22	simp3d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
28	1 2 17 18 19 24 25 26 27	ablfacrp2	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ∧ ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ) = ( ( ♯ ‘ 𝐵 ) / ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
29	28	simpld	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )
30	16 29	eqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑆 ‘ 𝑃 ) ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) )