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