Metamath Proof Explorer


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 ( ♯ ‘ 𝐵 ) ) ) )