This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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