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 ) ) ) )