Metamath Proof Explorer

Theorem ablfac1c

Description: The factors of ablfac1b cover the entire group. (Contributed by Mario Carneiro, 21-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 )
ablfac1c.d 
|- D = { w e. Prime | w || ( # ` B ) }
ablfac1.2 
|- ( ph -> D C_ A )
Assertion ablfac1c 
|- ( ph -> ( G DProd S ) = 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 ablfac1c.d 
 |-  D = { w e. Prime | w || ( # ` B ) }
8 ablfac1.2 
 |-  ( ph -> D C_ A )
9 1 dprdssv 
 |-  ( G DProd S ) C_ B
10 9 a1i 
 |-  ( ph -> ( G DProd S ) C_ B )
11 ssfi 
 |-  ( ( B e. Fin /\ ( G DProd S ) C_ B ) -> ( G DProd S ) e. Fin )
12 5 9 11 sylancl 
 |-  ( ph -> ( G DProd S ) e. Fin )
13 hashcl 
 |-  ( ( G DProd S ) e. Fin -> ( # ` ( G DProd S ) ) e. NN0 )
14 12 13 syl 
 |-  ( ph -> ( # ` ( G DProd S ) ) e. NN0 )
15 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
16 5 15 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
17 1 2 3 4 5 6 ablfac1b 
 |-  ( ph -> G dom DProd S )
18 dprdsubg 
 |-  ( G dom DProd S -> ( G DProd S ) e. ( SubGrp ` G ) )
19 17 18 syl 
 |-  ( ph -> ( G DProd S ) e. ( SubGrp ` G ) )
20 1 lagsubg 
 |-  ( ( ( G DProd S ) e. ( SubGrp ` G ) /\ B e. Fin ) -> ( # ` ( G DProd S ) ) || ( # ` B ) )
21 19 5 20 syl2anc 
 |-  ( ph -> ( # ` ( G DProd S ) ) || ( # ` B ) )
22 breq1 
 |-  ( w = q -> ( w || ( # ` B ) <-> q || ( # ` B ) ) )
23 22 7 elrab2 
 |-  ( q e. D <-> ( q e. Prime /\ q || ( # ` B ) ) )
24 8 sseld 
 |-  ( ph -> ( q e. D -> q e. A ) )
25 23 24 syl5bir 
 |-  ( ph -> ( ( q e. Prime /\ q || ( # ` B ) ) -> q e. A ) )
26 25 impl 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || ( # ` B ) ) -> q e. A )
27 1 2 3 4 5 6 ablfac1a 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) = ( q ^ ( q pCnt ( # ` B ) ) ) )
28 1 fvexi 
 |-  B e. _V
29 28 rabex 
 |-  { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
30 29 3 dmmpti 
 |-  dom S = A
31 30 a1i 
 |-  ( ph -> dom S = A )
32 17 31 dprdf2 
 |-  ( ph -> S : A --> ( SubGrp ` G ) )
33 32 ffvelrnda 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) e. ( SubGrp ` G ) )
34 17 adantr 
 |-  ( ( ph /\ q e. A ) -> G dom DProd S )
35 30 a1i 
 |-  ( ( ph /\ q e. A ) -> dom S = A )
36 simpr 
 |-  ( ( ph /\ q e. A ) -> q e. A )
37 34 35 36 dprdub 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) C_ ( G DProd S ) )
38 19 adantr 
 |-  ( ( ph /\ q e. A ) -> ( G DProd S ) e. ( SubGrp ` G ) )
39 eqid 
 |-  ( G |`s ( G DProd S ) ) = ( G |`s ( G DProd S ) )
40 39 subsubg 
 |-  ( ( G DProd S ) e. ( SubGrp ` G ) -> ( ( S ` q ) e. ( SubGrp ` ( G |`s ( G DProd S ) ) ) <-> ( ( S ` q ) e. ( SubGrp ` G ) /\ ( S ` q ) C_ ( G DProd S ) ) ) )
41 38 40 syl 
 |-  ( ( ph /\ q e. A ) -> ( ( S ` q ) e. ( SubGrp ` ( G |`s ( G DProd S ) ) ) <-> ( ( S ` q ) e. ( SubGrp ` G ) /\ ( S ` q ) C_ ( G DProd S ) ) ) )
42 33 37 41 mpbir2and 
 |-  ( ( ph /\ q e. A ) -> ( S ` q ) e. ( SubGrp ` ( G |`s ( G DProd S ) ) ) )
43 39 subgbas 
 |-  ( ( G DProd S ) e. ( SubGrp ` G ) -> ( G DProd S ) = ( Base ` ( G |`s ( G DProd S ) ) ) )
44 38 43 syl 
 |-  ( ( ph /\ q e. A ) -> ( G DProd S ) = ( Base ` ( G |`s ( G DProd S ) ) ) )
45 12 adantr 
 |-  ( ( ph /\ q e. A ) -> ( G DProd S ) e. Fin )
46 44 45 eqeltrrd 
 |-  ( ( ph /\ q e. A ) -> ( Base ` ( G |`s ( G DProd S ) ) ) e. Fin )
47 eqid 
 |-  ( Base ` ( G |`s ( G DProd S ) ) ) = ( Base ` ( G |`s ( G DProd S ) ) )
48 47 lagsubg 
 |-  ( ( ( S ` q ) e. ( SubGrp ` ( G |`s ( G DProd S ) ) ) /\ ( Base ` ( G |`s ( G DProd S ) ) ) e. Fin ) -> ( # ` ( S ` q ) ) || ( # ` ( Base ` ( G |`s ( G DProd S ) ) ) ) )
49 42 46 48 syl2anc 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) || ( # ` ( Base ` ( G |`s ( G DProd S ) ) ) ) )
50 44 fveq2d 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( G DProd S ) ) = ( # ` ( Base ` ( G |`s ( G DProd S ) ) ) ) )
51 49 50 breqtrrd 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( S ` q ) ) || ( # ` ( G DProd S ) ) )
52 27 51 eqbrtrrd 
 |-  ( ( ph /\ q e. A ) -> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` ( G DProd S ) ) )
53 6 sselda 
 |-  ( ( ph /\ q e. A ) -> q e. Prime )
54 14 nn0zd 
 |-  ( ph -> ( # ` ( G DProd S ) ) e. ZZ )
55 54 adantr 
 |-  ( ( ph /\ q e. A ) -> ( # ` ( G DProd S ) ) e. ZZ )
56 simpr 
 |-  ( ( ph /\ q e. Prime ) -> q e. Prime )
57 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
58 1 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
59 4 57 58 3syl 
 |-  ( ph -> B =/= (/) )
60 hashnncl 
 |-  ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
61 5 60 syl 
 |-  ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
62 59 61 mpbird 
 |-  ( ph -> ( # ` B ) e. NN )
63 62 adantr 
 |-  ( ( ph /\ q e. Prime ) -> ( # ` B ) e. NN )
64 56 63 pccld 
 |-  ( ( ph /\ q e. Prime ) -> ( q pCnt ( # ` B ) ) e. NN0 )
65 53 64 syldan 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) e. NN0 )
66 pcdvdsb 
 |-  ( ( q e. Prime /\ ( # ` ( G DProd S ) ) e. ZZ /\ ( q pCnt ( # ` B ) ) e. NN0 ) -> ( ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) <-> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` ( G DProd S ) ) ) )
67 53 55 65 66 syl3anc 
 |-  ( ( ph /\ q e. A ) -> ( ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) <-> ( q ^ ( q pCnt ( # ` B ) ) ) || ( # ` ( G DProd S ) ) ) )
68 52 67 mpbird 
 |-  ( ( ph /\ q e. A ) -> ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
69 68 adantlr 
 |-  ( ( ( ph /\ q e. Prime ) /\ q e. A ) -> ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
70 26 69 syldan 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || ( # ` B ) ) -> ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
71 pceq0 
 |-  ( ( q e. Prime /\ ( # ` B ) e. NN ) -> ( ( q pCnt ( # ` B ) ) = 0 <-> -. q || ( # ` B ) ) )
72 56 63 71 syl2anc 
 |-  ( ( ph /\ q e. Prime ) -> ( ( q pCnt ( # ` B ) ) = 0 <-> -. q || ( # ` B ) ) )
73 72 biimpar 
 |-  ( ( ( ph /\ q e. Prime ) /\ -. q || ( # ` B ) ) -> ( q pCnt ( # ` B ) ) = 0 )
74 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
75 74 subg0cl 
 |-  ( ( G DProd S ) e. ( SubGrp ` G ) -> ( 0g ` G ) e. ( G DProd S ) )
76 ne0i 
 |-  ( ( 0g ` G ) e. ( G DProd S ) -> ( G DProd S ) =/= (/) )
77 19 75 76 3syl 
 |-  ( ph -> ( G DProd S ) =/= (/) )
78 hashnncl 
 |-  ( ( G DProd S ) e. Fin -> ( ( # ` ( G DProd S ) ) e. NN <-> ( G DProd S ) =/= (/) ) )
79 12 78 syl 
 |-  ( ph -> ( ( # ` ( G DProd S ) ) e. NN <-> ( G DProd S ) =/= (/) ) )
80 77 79 mpbird 
 |-  ( ph -> ( # ` ( G DProd S ) ) e. NN )
81 80 adantr 
 |-  ( ( ph /\ q e. Prime ) -> ( # ` ( G DProd S ) ) e. NN )
82 56 81 pccld 
 |-  ( ( ph /\ q e. Prime ) -> ( q pCnt ( # ` ( G DProd S ) ) ) e. NN0 )
83 82 nn0ge0d 
 |-  ( ( ph /\ q e. Prime ) -> 0 <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
84 83 adantr 
 |-  ( ( ( ph /\ q e. Prime ) /\ -. q || ( # ` B ) ) -> 0 <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
85 73 84 eqbrtrd 
 |-  ( ( ( ph /\ q e. Prime ) /\ -. q || ( # ` B ) ) -> ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
86 70 85 pm2.61dan 
 |-  ( ( ph /\ q e. Prime ) -> ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
87 86 ralrimiva 
 |-  ( ph -> A. q e. Prime ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) )
88 16 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
89 pc2dvds 
 |-  ( ( ( # ` B ) e. ZZ /\ ( # ` ( G DProd S ) ) e. ZZ ) -> ( ( # ` B ) || ( # ` ( G DProd S ) ) <-> A. q e. Prime ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) ) )
90 88 54 89 syl2anc 
 |-  ( ph -> ( ( # ` B ) || ( # ` ( G DProd S ) ) <-> A. q e. Prime ( q pCnt ( # ` B ) ) <_ ( q pCnt ( # ` ( G DProd S ) ) ) ) )
91 87 90 mpbird 
 |-  ( ph -> ( # ` B ) || ( # ` ( G DProd S ) ) )
92 dvdseq 
 |-  ( ( ( ( # ` ( G DProd S ) ) e. NN0 /\ ( # ` B ) e. NN0 ) /\ ( ( # ` ( G DProd S ) ) || ( # ` B ) /\ ( # ` B ) || ( # ` ( G DProd S ) ) ) ) -> ( # ` ( G DProd S ) ) = ( # ` B ) )
93 14 16 21 91 92 syl22anc 
 |-  ( ph -> ( # ` ( G DProd S ) ) = ( # ` B ) )
94 hashen 
 |-  ( ( ( G DProd S ) e. Fin /\ B e. Fin ) -> ( ( # ` ( G DProd S ) ) = ( # ` B ) <-> ( G DProd S ) ~~ B ) )
95 12 5 94 syl2anc 
 |-  ( ph -> ( ( # ` ( G DProd S ) ) = ( # ` B ) <-> ( G DProd S ) ~~ B ) )
96 93 95 mpbid 
 |-  ( ph -> ( G DProd S ) ~~ B )
97 fisseneq 
 |-  ( ( B e. Fin /\ ( G DProd S ) C_ B /\ ( G DProd S ) ~~ B ) -> ( G DProd S ) = B )
98 5 10 96 97 syl3anc 
 |-  ( ph -> ( G DProd S ) = B )