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
|- B = ( Base ` G )
ablfac1.o
|- O = ( od ` G )
ablfac1.s
|- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
ablfac1.g
|- ( ph -> G e. Abel )
ablfac1.f
|- ( ph -> B e. Fin )
ablfac1.1
|- ( ph -> A C_ Prime )
Assertion ablfac1a
|- ( ( ph /\ P e. A ) -> ( # ` ( S ` P ) ) = ( P ^ ( P pCnt ( # ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 ablfac1.b
 |-  B = ( Base ` G )
2 ablfac1.o
 |-  O = ( od ` G )
3 ablfac1.s
 |-  S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
4 ablfac1.g
 |-  ( ph -> G e. Abel )
5 ablfac1.f
 |-  ( ph -> B e. Fin )
6 ablfac1.1
 |-  ( ph -> A C_ Prime )
7 id
 |-  ( p = P -> p = P )
8 oveq1
 |-  ( p = P -> ( p pCnt ( # ` B ) ) = ( P pCnt ( # ` B ) ) )
9 7 8 oveq12d
 |-  ( p = P -> ( p ^ ( p pCnt ( # ` B ) ) ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
10 9 breq2d
 |-  ( p = P -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) ) )
11 10 rabbidv
 |-  ( p = P -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } = { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) } )
12 1 fvexi
 |-  B e. _V
13 12 rabex
 |-  { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
14 11 3 13 fvmpt3i
 |-  ( P e. A -> ( S ` P ) = { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) } )
15 14 adantl
 |-  ( ( ph /\ P e. A ) -> ( S ` P ) = { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) } )
16 15 fveq2d
 |-  ( ( ph /\ P e. A ) -> ( # ` ( S ` P ) ) = ( # ` { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) } ) )
17 eqid
 |-  { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) } = { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) }
18 eqid
 |-  { x e. B | ( O ` x ) || ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) } = { x e. B | ( O ` x ) || ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) }
19 4 adantr
 |-  ( ( ph /\ P e. A ) -> G e. Abel )
20 eqid
 |-  ( P ^ ( P pCnt ( # ` B ) ) ) = ( P ^ ( P pCnt ( # ` B ) ) )
21 eqid
 |-  ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) = ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) )
22 1 2 3 4 5 6 20 21 ablfac1lem
 |-  ( ( ph /\ P e. A ) -> ( ( ( P ^ ( P pCnt ( # ` B ) ) ) e. NN /\ ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) e. NN ) /\ ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) ) = 1 /\ ( # ` B ) = ( ( P ^ ( P pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) ) ) )
23 22 simp1d
 |-  ( ( ph /\ P e. A ) -> ( ( P ^ ( P pCnt ( # ` B ) ) ) e. NN /\ ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) e. NN ) )
24 23 simpld
 |-  ( ( ph /\ P e. A ) -> ( P ^ ( P pCnt ( # ` B ) ) ) e. NN )
25 23 simprd
 |-  ( ( ph /\ P e. A ) -> ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) e. NN )
26 22 simp2d
 |-  ( ( ph /\ P e. A ) -> ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) ) = 1 )
27 22 simp3d
 |-  ( ( ph /\ P e. A ) -> ( # ` B ) = ( ( P ^ ( P pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) ) )
28 1 2 17 18 19 24 25 26 27 ablfacrp2
 |-  ( ( ph /\ P e. A ) -> ( ( # ` { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) } ) = ( P ^ ( P pCnt ( # ` B ) ) ) /\ ( # ` { x e. B | ( O ` x ) || ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) } ) = ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) ) )
29 28 simpld
 |-  ( ( ph /\ P e. A ) -> ( # ` { x e. B | ( O ` x ) || ( P ^ ( P pCnt ( # ` B ) ) ) } ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
30 16 29 eqtrd
 |-  ( ( ph /\ P e. A ) -> ( # ` ( S ` P ) ) = ( P ^ ( P pCnt ( # ` B ) ) ) )