Metamath Proof Explorer

Theorem ablfac1lem

Description: Lemma for ablfac1b . Satisfy the assumptions of ablfacrp. (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 )
ablfac1.m 
|- M = ( P ^ ( P pCnt ( # ` B ) ) )
ablfac1.n 
|- N = ( ( # ` B ) / M )
Assertion ablfac1lem 
|- ( ( ph /\ P e. A ) -> ( ( M e. NN /\ N e. NN ) /\ ( M gcd N ) = 1 /\ ( # ` B ) = ( M x. N ) ) )

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 ablfac1.m 
 |-  M = ( P ^ ( P pCnt ( # ` B ) ) )
8 ablfac1.n 
 |-  N = ( ( # ` B ) / M )
9 6 sselda 
 |-  ( ( ph /\ P e. A ) -> P e. Prime )
10 prmnn 
 |-  ( P e. Prime -> P e. NN )
11 9 10 syl 
 |-  ( ( ph /\ P e. A ) -> P e. NN )
12 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
13 1 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
14 4 12 13 3syl 
 |-  ( ph -> B =/= (/) )
15 hashnncl 
 |-  ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
16 5 15 syl 
 |-  ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
17 14 16 mpbird 
 |-  ( ph -> ( # ` B ) e. NN )
18 17 adantr 
 |-  ( ( ph /\ P e. A ) -> ( # ` B ) e. NN )
19 9 18 pccld 
 |-  ( ( ph /\ P e. A ) -> ( P pCnt ( # ` B ) ) e. NN0 )
20 11 19 nnexpcld 
 |-  ( ( ph /\ P e. A ) -> ( P ^ ( P pCnt ( # ` B ) ) ) e. NN )
21 7 20 eqeltrid 
 |-  ( ( ph /\ P e. A ) -> M e. NN )
22 pcdvds 
 |-  ( ( P e. Prime /\ ( # ` B ) e. NN ) -> ( P ^ ( P pCnt ( # ` B ) ) ) || ( # ` B ) )
23 9 18 22 syl2anc 
 |-  ( ( ph /\ P e. A ) -> ( P ^ ( P pCnt ( # ` B ) ) ) || ( # ` B ) )
24 7 23 eqbrtrid 
 |-  ( ( ph /\ P e. A ) -> M || ( # ` B ) )
25 nndivdvds 
 |-  ( ( ( # ` B ) e. NN /\ M e. NN ) -> ( M || ( # ` B ) <-> ( ( # ` B ) / M ) e. NN ) )
26 18 21 25 syl2anc 
 |-  ( ( ph /\ P e. A ) -> ( M || ( # ` B ) <-> ( ( # ` B ) / M ) e. NN ) )
27 24 26 mpbid 
 |-  ( ( ph /\ P e. A ) -> ( ( # ` B ) / M ) e. NN )
28 8 27 eqeltrid 
 |-  ( ( ph /\ P e. A ) -> N e. NN )
29 21 28 jca 
 |-  ( ( ph /\ P e. A ) -> ( M e. NN /\ N e. NN ) )
30 7 oveq1i 
 |-  ( M gcd N ) = ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd N )
31 pcndvds2 
 |-  ( ( P e. Prime /\ ( # ` B ) e. NN ) -> -. P || ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) )
32 9 18 31 syl2anc 
 |-  ( ( ph /\ P e. A ) -> -. P || ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) )
33 7 oveq2i 
 |-  ( ( # ` B ) / M ) = ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) )
34 8 33 eqtri 
 |-  N = ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) )
35 34 breq2i 
 |-  ( P || N <-> P || ( ( # ` B ) / ( P ^ ( P pCnt ( # ` B ) ) ) ) )
36 32 35 sylnibr 
 |-  ( ( ph /\ P e. A ) -> -. P || N )
37 28 nnzd 
 |-  ( ( ph /\ P e. A ) -> N e. ZZ )
38 coprm 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. P || N <-> ( P gcd N ) = 1 ) )
39 9 37 38 syl2anc 
 |-  ( ( ph /\ P e. A ) -> ( -. P || N <-> ( P gcd N ) = 1 ) )
40 36 39 mpbid 
 |-  ( ( ph /\ P e. A ) -> ( P gcd N ) = 1 )
41 prmz 
 |-  ( P e. Prime -> P e. ZZ )
42 9 41 syl 
 |-  ( ( ph /\ P e. A ) -> P e. ZZ )
43 rpexp1i 
 |-  ( ( P e. ZZ /\ N e. ZZ /\ ( P pCnt ( # ` B ) ) e. NN0 ) -> ( ( P gcd N ) = 1 -> ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd N ) = 1 ) )
44 42 37 19 43 syl3anc 
 |-  ( ( ph /\ P e. A ) -> ( ( P gcd N ) = 1 -> ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd N ) = 1 ) )
45 40 44 mpd 
 |-  ( ( ph /\ P e. A ) -> ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd N ) = 1 )
46 30 45 syl5eq 
 |-  ( ( ph /\ P e. A ) -> ( M gcd N ) = 1 )
47 8 oveq2i 
 |-  ( M x. N ) = ( M x. ( ( # ` B ) / M ) )
48 18 nncnd 
 |-  ( ( ph /\ P e. A ) -> ( # ` B ) e. CC )
49 21 nncnd 
 |-  ( ( ph /\ P e. A ) -> M e. CC )
50 21 nnne0d 
 |-  ( ( ph /\ P e. A ) -> M =/= 0 )
51 48 49 50 divcan2d 
 |-  ( ( ph /\ P e. A ) -> ( M x. ( ( # ` B ) / M ) ) = ( # ` B ) )
52 47 51 eqtr2id 
 |-  ( ( ph /\ P e. A ) -> ( # ` B ) = ( M x. N ) )
53 29 46 52 3jca 
 |-  ( ( ph /\ P e. A ) -> ( ( M e. NN /\ N e. NN ) /\ ( M gcd N ) = 1 /\ ( # ` B ) = ( M x. N ) ) )