Metamath Proof Explorer

Theorem ablfacrplem

Description: Lemma for ablfacrp2 . (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses ablfacrp.b 
|- B = ( Base ` G )
ablfacrp.o 
|- O = ( od ` G )
ablfacrp.k 
|- K = { x e. B | ( O ` x ) || M }
ablfacrp.l 
|- L = { x e. B | ( O ` x ) || N }
ablfacrp.g 
|- ( ph -> G e. Abel )
ablfacrp.m 
|- ( ph -> M e. NN )
ablfacrp.n 
|- ( ph -> N e. NN )
ablfacrp.1 
|- ( ph -> ( M gcd N ) = 1 )
ablfacrp.2 
|- ( ph -> ( # ` B ) = ( M x. N ) )
Assertion ablfacrplem 
|- ( ph -> ( ( # ` K ) gcd N ) = 1 )

Proof

Step Hyp Ref Expression
1 ablfacrp.b 
 |-  B = ( Base ` G )
2 ablfacrp.o 
 |-  O = ( od ` G )
3 ablfacrp.k 
 |-  K = { x e. B | ( O ` x ) || M }
4 ablfacrp.l 
 |-  L = { x e. B | ( O ` x ) || N }
5 ablfacrp.g 
 |-  ( ph -> G e. Abel )
6 ablfacrp.m 
 |-  ( ph -> M e. NN )
7 ablfacrp.n 
 |-  ( ph -> N e. NN )
8 ablfacrp.1 
 |-  ( ph -> ( M gcd N ) = 1 )
9 ablfacrp.2 
 |-  ( ph -> ( # ` B ) = ( M x. N ) )
10 nprmdvds1 
 |-  ( p e. Prime -> -. p || 1 )
11 10 adantl 
 |-  ( ( ph /\ p e. Prime ) -> -. p || 1 )
12 8 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( M gcd N ) = 1 )
13 12 breq2d 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( M gcd N ) <-> p || 1 ) )
14 11 13 mtbird 
 |-  ( ( ph /\ p e. Prime ) -> -. p || ( M gcd N ) )
15 6 nnzd 
 |-  ( ph -> M e. ZZ )
16 2 1 oddvdssubg 
 |-  ( ( G e. Abel /\ M e. ZZ ) -> { x e. B | ( O ` x ) || M } e. ( SubGrp ` G ) )
17 5 15 16 syl2anc 
 |-  ( ph -> { x e. B | ( O ` x ) || M } e. ( SubGrp ` G ) )
18 3 17 eqeltrid 
 |-  ( ph -> K e. ( SubGrp ` G ) )
19 18 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> K e. ( SubGrp ` G ) )
20 eqid 
 |-  ( G |`s K ) = ( G |`s K )
21 20 subggrp 
 |-  ( K e. ( SubGrp ` G ) -> ( G |`s K ) e. Grp )
22 19 21 syl 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> ( G |`s K ) e. Grp )
23 20 subgbas 
 |-  ( K e. ( SubGrp ` G ) -> K = ( Base ` ( G |`s K ) ) )
24 19 23 syl 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> K = ( Base ` ( G |`s K ) ) )
25 6 nnnn0d 
 |-  ( ph -> M e. NN0 )
26 7 nnnn0d 
 |-  ( ph -> N e. NN0 )
27 25 26 nn0mulcld 
 |-  ( ph -> ( M x. N ) e. NN0 )
28 9 27 eqeltrd 
 |-  ( ph -> ( # ` B ) e. NN0 )
29 1 fvexi 
 |-  B e. _V
30 hashclb 
 |-  ( B e. _V -> ( B e. Fin <-> ( # ` B ) e. NN0 ) )
31 29 30 ax-mp 
 |-  ( B e. Fin <-> ( # ` B ) e. NN0 )
32 28 31 sylibr 
 |-  ( ph -> B e. Fin )
33 3 ssrab3 
 |-  K C_ B
34 ssfi 
 |-  ( ( B e. Fin /\ K C_ B ) -> K e. Fin )
35 32 33 34 sylancl 
 |-  ( ph -> K e. Fin )
36 35 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> K e. Fin )
37 24 36 eqeltrrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> ( Base ` ( G |`s K ) ) e. Fin )
38 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> p e. Prime )
39 simpr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> p || ( # ` K ) )
40 24 fveq2d 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> ( # ` K ) = ( # ` ( Base ` ( G |`s K ) ) ) )
41 39 40 breqtrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> p || ( # ` ( Base ` ( G |`s K ) ) ) )
42 eqid 
 |-  ( Base ` ( G |`s K ) ) = ( Base ` ( G |`s K ) )
43 eqid 
 |-  ( od ` ( G |`s K ) ) = ( od ` ( G |`s K ) )
44 42 43 odcau 
 |-  ( ( ( ( G |`s K ) e. Grp /\ ( Base ` ( G |`s K ) ) e. Fin /\ p e. Prime ) /\ p || ( # ` ( Base ` ( G |`s K ) ) ) ) -> E. g e. ( Base ` ( G |`s K ) ) ( ( od ` ( G |`s K ) ) ` g ) = p )
45 22 37 38 41 44 syl31anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> E. g e. ( Base ` ( G |`s K ) ) ( ( od ` ( G |`s K ) ) ` g ) = p )
46 45 24 rexeqtrrdv 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> E. g e. K ( ( od ` ( G |`s K ) ) ` g ) = p )
47 20 2 43 subgod 
 |-  ( ( K e. ( SubGrp ` G ) /\ g e. K ) -> ( O ` g ) = ( ( od ` ( G |`s K ) ) ` g ) )
48 19 47 sylan 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( O ` g ) = ( ( od ` ( G |`s K ) ) ` g ) )
49 fveq2 
 |-  ( x = g -> ( O ` x ) = ( O ` g ) )
50 49 breq1d 
 |-  ( x = g -> ( ( O ` x ) || M <-> ( O ` g ) || M ) )
51 50 3 elrab2 
 |-  ( g e. K <-> ( g e. B /\ ( O ` g ) || M ) )
52 51 simprbi 
 |-  ( g e. K -> ( O ` g ) || M )
53 52 adantl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( O ` g ) || M )
54 48 53 eqbrtrrd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( ( od ` ( G |`s K ) ) ` g ) || M )
55 breq1 
 |-  ( ( ( od ` ( G |`s K ) ) ` g ) = p -> ( ( ( od ` ( G |`s K ) ) ` g ) || M <-> p || M ) )
56 54 55 syl5ibcom 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( ( ( od ` ( G |`s K ) ) ` g ) = p -> p || M ) )
57 56 rexlimdva 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> ( E. g e. K ( ( od ` ( G |`s K ) ) ` g ) = p -> p || M ) )
58 46 57 mpd 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> p || M )
59 58 ex 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( # ` K ) -> p || M ) )
60 59 anim1d 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || ( # ` K ) /\ p || N ) -> ( p || M /\ p || N ) ) )
61 prmz 
 |-  ( p e. Prime -> p e. ZZ )
62 61 adantl 
 |-  ( ( ph /\ p e. Prime ) -> p e. ZZ )
63 hashcl 
 |-  ( K e. Fin -> ( # ` K ) e. NN0 )
64 35 63 syl 
 |-  ( ph -> ( # ` K ) e. NN0 )
65 64 nn0zd 
 |-  ( ph -> ( # ` K ) e. ZZ )
66 65 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( # ` K ) e. ZZ )
67 7 nnzd 
 |-  ( ph -> N e. ZZ )
68 67 adantr 
 |-  ( ( ph /\ p e. Prime ) -> N e. ZZ )
69 dvdsgcdb 
 |-  ( ( p e. ZZ /\ ( # ` K ) e. ZZ /\ N e. ZZ ) -> ( ( p || ( # ` K ) /\ p || N ) <-> p || ( ( # ` K ) gcd N ) ) )
70 62 66 68 69 syl3anc 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || ( # ` K ) /\ p || N ) <-> p || ( ( # ` K ) gcd N ) ) )
71 15 adantr 
 |-  ( ( ph /\ p e. Prime ) -> M e. ZZ )
72 dvdsgcdb 
 |-  ( ( p e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( p || M /\ p || N ) <-> p || ( M gcd N ) ) )
73 62 71 68 72 syl3anc 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || M /\ p || N ) <-> p || ( M gcd N ) ) )
74 60 70 73 3imtr3d 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( ( # ` K ) gcd N ) -> p || ( M gcd N ) ) )
75 14 74 mtod 
 |-  ( ( ph /\ p e. Prime ) -> -. p || ( ( # ` K ) gcd N ) )
76 75 nrexdv 
 |-  ( ph -> -. E. p e. Prime p || ( ( # ` K ) gcd N ) )
77 exprmfct 
 |-  ( ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( ( # ` K ) gcd N ) )
78 76 77 nsyl 
 |-  ( ph -> -. ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) )
79 7 nnne0d 
 |-  ( ph -> N =/= 0 )
80 simpr 
 |-  ( ( ( # ` K ) = 0 /\ N = 0 ) -> N = 0 )
81 80 necon3ai 
 |-  ( N =/= 0 -> -. ( ( # ` K ) = 0 /\ N = 0 ) )
82 79 81 syl 
 |-  ( ph -> -. ( ( # ` K ) = 0 /\ N = 0 ) )
83 gcdn0cl 
 |-  ( ( ( ( # ` K ) e. ZZ /\ N e. ZZ ) /\ -. ( ( # ` K ) = 0 /\ N = 0 ) ) -> ( ( # ` K ) gcd N ) e. NN )
84 65 67 82 83 syl21anc 
 |-  ( ph -> ( ( # ` K ) gcd N ) e. NN )
85 elnn1uz2 
 |-  ( ( ( # ` K ) gcd N ) e. NN <-> ( ( ( # ` K ) gcd N ) = 1 \/ ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) ) )
86 84 85 sylib 
 |-  ( ph -> ( ( ( # ` K ) gcd N ) = 1 \/ ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) ) )
87 86 ord 
 |-  ( ph -> ( -. ( ( # ` K ) gcd N ) = 1 -> ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) ) )
88 78 87 mt3d 
 |-  ( ph -> ( ( # ` K ) gcd N ) = 1 )