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 24 rexeqdv 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> ( E. g e. K ( ( od ` ( G |`s K ) ) ` g ) = p <-> E. g e. ( Base ` ( G |`s K ) ) ( ( od ` ( G |`s K ) ) ` g ) = p ) )
47 45 46 mpbird 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> E. g e. K ( ( od ` ( G |`s K ) ) ` g ) = p )
48 20 2 43 subgod 
 |-  ( ( K e. ( SubGrp ` G ) /\ g e. K ) -> ( O ` g ) = ( ( od ` ( G |`s K ) ) ` g ) )
49 19 48 sylan 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( O ` g ) = ( ( od ` ( G |`s K ) ) ` g ) )
50 fveq2 
 |-  ( x = g -> ( O ` x ) = ( O ` g ) )
51 50 breq1d 
 |-  ( x = g -> ( ( O ` x ) || M <-> ( O ` g ) || M ) )
52 51 3 elrab2 
 |-  ( g e. K <-> ( g e. B /\ ( O ` g ) || M ) )
53 52 simprbi 
 |-  ( g e. K -> ( O ` g ) || M )
54 53 adantl 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( O ` g ) || M )
55 49 54 eqbrtrrd 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( ( od ` ( G |`s K ) ) ` g ) || M )
56 breq1 
 |-  ( ( ( od ` ( G |`s K ) ) ` g ) = p -> ( ( ( od ` ( G |`s K ) ) ` g ) || M <-> p || M ) )
57 55 56 syl5ibcom 
 |-  ( ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) /\ g e. K ) -> ( ( ( od ` ( G |`s K ) ) ` g ) = p -> p || M ) )
58 57 rexlimdva 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> ( E. g e. K ( ( od ` ( G |`s K ) ) ` g ) = p -> p || M ) )
59 47 58 mpd 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || ( # ` K ) ) -> p || M )
60 59 ex 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( # ` K ) -> p || M ) )
61 60 anim1d 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || ( # ` K ) /\ p || N ) -> ( p || M /\ p || N ) ) )
62 prmz 
 |-  ( p e. Prime -> p e. ZZ )
63 62 adantl 
 |-  ( ( ph /\ p e. Prime ) -> p e. ZZ )
64 hashcl 
 |-  ( K e. Fin -> ( # ` K ) e. NN0 )
65 35 64 syl 
 |-  ( ph -> ( # ` K ) e. NN0 )
66 65 nn0zd 
 |-  ( ph -> ( # ` K ) e. ZZ )
67 66 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( # ` K ) e. ZZ )
68 7 nnzd 
 |-  ( ph -> N e. ZZ )
69 68 adantr 
 |-  ( ( ph /\ p e. Prime ) -> N e. ZZ )
70 dvdsgcdb 
 |-  ( ( p e. ZZ /\ ( # ` K ) e. ZZ /\ N e. ZZ ) -> ( ( p || ( # ` K ) /\ p || N ) <-> p || ( ( # ` K ) gcd N ) ) )
71 63 67 69 70 syl3anc 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || ( # ` K ) /\ p || N ) <-> p || ( ( # ` K ) gcd N ) ) )
72 15 adantr 
 |-  ( ( ph /\ p e. Prime ) -> M e. ZZ )
73 dvdsgcdb 
 |-  ( ( p e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( p || M /\ p || N ) <-> p || ( M gcd N ) ) )
74 63 72 69 73 syl3anc 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || M /\ p || N ) <-> p || ( M gcd N ) ) )
75 61 71 74 3imtr3d 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( ( # ` K ) gcd N ) -> p || ( M gcd N ) ) )
76 14 75 mtod 
 |-  ( ( ph /\ p e. Prime ) -> -. p || ( ( # ` K ) gcd N ) )
77 76 nrexdv 
 |-  ( ph -> -. E. p e. Prime p || ( ( # ` K ) gcd N ) )
78 exprmfct 
 |-  ( ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) -> E. p e. Prime p || ( ( # ` K ) gcd N ) )
79 77 78 nsyl 
 |-  ( ph -> -. ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) )
80 7 nnne0d 
 |-  ( ph -> N =/= 0 )
81 simpr 
 |-  ( ( ( # ` K ) = 0 /\ N = 0 ) -> N = 0 )
82 81 necon3ai 
 |-  ( N =/= 0 -> -. ( ( # ` K ) = 0 /\ N = 0 ) )
83 80 82 syl 
 |-  ( ph -> -. ( ( # ` K ) = 0 /\ N = 0 ) )
84 gcdn0cl 
 |-  ( ( ( ( # ` K ) e. ZZ /\ N e. ZZ ) /\ -. ( ( # ` K ) = 0 /\ N = 0 ) ) -> ( ( # ` K ) gcd N ) e. NN )
85 66 68 83 84 syl21anc 
 |-  ( ph -> ( ( # ` K ) gcd N ) e. NN )
86 elnn1uz2 
 |-  ( ( ( # ` K ) gcd N ) e. NN <-> ( ( ( # ` K ) gcd N ) = 1 \/ ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) ) )
87 85 86 sylib 
 |-  ( ph -> ( ( ( # ` K ) gcd N ) = 1 \/ ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) ) )
88 87 ord 
 |-  ( ph -> ( -. ( ( # ` K ) gcd N ) = 1 -> ( ( # ` K ) gcd N ) e. ( ZZ>= ` 2 ) ) )
89 79 88 mt3d 
 |-  ( ph -> ( ( # ` K ) gcd N ) = 1 )