Metamath Proof Explorer

Theorem ablfacrp2

Description: The factors K , L of ablfacrp have the expected orders (which allows for repeated application to decompose G into subgroups of prime-power order). Lemma 6.1C.2 of Shapiro, p. 199. (Contributed by Mario Carneiro, 21-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 ablfacrp2 
|- ( ph -> ( ( # ` K ) = M /\ ( # ` L ) = N ) )

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 6 nnnn0d 
 |-  ( ph -> M e. NN0 )
11 7 nnnn0d 
 |-  ( ph -> N e. NN0 )
12 10 11 nn0mulcld 
 |-  ( ph -> ( M x. N ) e. NN0 )
13 9 12 eqeltrd 
 |-  ( ph -> ( # ` B ) e. NN0 )
14 1 fvexi 
 |-  B e. _V
15 hashclb 
 |-  ( B e. _V -> ( B e. Fin <-> ( # ` B ) e. NN0 ) )
16 14 15 ax-mp 
 |-  ( B e. Fin <-> ( # ` B ) e. NN0 )
17 13 16 sylibr 
 |-  ( ph -> B e. Fin )
18 3 ssrab3 
 |-  K C_ B
19 ssfi 
 |-  ( ( B e. Fin /\ K C_ B ) -> K e. Fin )
20 17 18 19 sylancl 
 |-  ( ph -> K e. Fin )
21 hashcl 
 |-  ( K e. Fin -> ( # ` K ) e. NN0 )
22 20 21 syl 
 |-  ( ph -> ( # ` K ) e. NN0 )
23 6 nnzd 
 |-  ( ph -> M e. ZZ )
24 2 1 oddvdssubg 
 |-  ( ( G e. Abel /\ M e. ZZ ) -> { x e. B | ( O ` x ) || M } e. ( SubGrp ` G ) )
25 5 23 24 syl2anc 
 |-  ( ph -> { x e. B | ( O ` x ) || M } e. ( SubGrp ` G ) )
26 3 25 eqeltrid 
 |-  ( ph -> K e. ( SubGrp ` G ) )
27 1 lagsubg 
 |-  ( ( K e. ( SubGrp ` G ) /\ B e. Fin ) -> ( # ` K ) || ( # ` B ) )
28 26 17 27 syl2anc 
 |-  ( ph -> ( # ` K ) || ( # ` B ) )
29 6 nncnd 
 |-  ( ph -> M e. CC )
30 7 nncnd 
 |-  ( ph -> N e. CC )
31 29 30 mulcomd 
 |-  ( ph -> ( M x. N ) = ( N x. M ) )
32 9 31 eqtrd 
 |-  ( ph -> ( # ` B ) = ( N x. M ) )
33 28 32 breqtrd 
 |-  ( ph -> ( # ` K ) || ( N x. M ) )
34 1 2 3 4 5 6 7 8 9 ablfacrplem 
 |-  ( ph -> ( ( # ` K ) gcd N ) = 1 )
35 22 nn0zd 
 |-  ( ph -> ( # ` K ) e. ZZ )
36 7 nnzd 
 |-  ( ph -> N e. ZZ )
37 coprmdvds 
 |-  ( ( ( # ` K ) e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( ( ( # ` K ) || ( N x. M ) /\ ( ( # ` K ) gcd N ) = 1 ) -> ( # ` K ) || M ) )
38 35 36 23 37 syl3anc 
 |-  ( ph -> ( ( ( # ` K ) || ( N x. M ) /\ ( ( # ` K ) gcd N ) = 1 ) -> ( # ` K ) || M ) )
39 33 34 38 mp2and 
 |-  ( ph -> ( # ` K ) || M )
40 2 1 oddvdssubg 
 |-  ( ( G e. Abel /\ N e. ZZ ) -> { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) )
41 5 36 40 syl2anc 
 |-  ( ph -> { x e. B | ( O ` x ) || N } e. ( SubGrp ` G ) )
42 4 41 eqeltrid 
 |-  ( ph -> L e. ( SubGrp ` G ) )
43 1 lagsubg 
 |-  ( ( L e. ( SubGrp ` G ) /\ B e. Fin ) -> ( # ` L ) || ( # ` B ) )
44 42 17 43 syl2anc 
 |-  ( ph -> ( # ` L ) || ( # ` B ) )
45 44 9 breqtrd 
 |-  ( ph -> ( # ` L ) || ( M x. N ) )
46 23 36 gcdcomd 
 |-  ( ph -> ( M gcd N ) = ( N gcd M ) )
47 46 8 eqtr3d 
 |-  ( ph -> ( N gcd M ) = 1 )
48 1 2 4 3 5 7 6 47 32 ablfacrplem 
 |-  ( ph -> ( ( # ` L ) gcd M ) = 1 )
49 4 ssrab3 
 |-  L C_ B
50 ssfi 
 |-  ( ( B e. Fin /\ L C_ B ) -> L e. Fin )
51 17 49 50 sylancl 
 |-  ( ph -> L e. Fin )
52 hashcl 
 |-  ( L e. Fin -> ( # ` L ) e. NN0 )
53 51 52 syl 
 |-  ( ph -> ( # ` L ) e. NN0 )
54 53 nn0zd 
 |-  ( ph -> ( # ` L ) e. ZZ )
55 coprmdvds 
 |-  ( ( ( # ` L ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( # ` L ) || ( M x. N ) /\ ( ( # ` L ) gcd M ) = 1 ) -> ( # ` L ) || N ) )
56 54 23 36 55 syl3anc 
 |-  ( ph -> ( ( ( # ` L ) || ( M x. N ) /\ ( ( # ` L ) gcd M ) = 1 ) -> ( # ` L ) || N ) )
57 45 48 56 mp2and 
 |-  ( ph -> ( # ` L ) || N )
58 dvdscmul 
 |-  ( ( ( # ` L ) e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( ( # ` L ) || N -> ( M x. ( # ` L ) ) || ( M x. N ) ) )
59 54 36 23 58 syl3anc 
 |-  ( ph -> ( ( # ` L ) || N -> ( M x. ( # ` L ) ) || ( M x. N ) ) )
60 57 59 mpd 
 |-  ( ph -> ( M x. ( # ` L ) ) || ( M x. N ) )
61 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
62 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
63 1 2 3 4 5 6 7 8 9 61 62 ablfacrp 
 |-  ( ph -> ( ( K i^i L ) = { ( 0g ` G ) } /\ ( K ( LSSum ` G ) L ) = B ) )
64 63 simprd 
 |-  ( ph -> ( K ( LSSum ` G ) L ) = B )
65 64 fveq2d 
 |-  ( ph -> ( # ` ( K ( LSSum ` G ) L ) ) = ( # ` B ) )
66 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
67 63 simpld 
 |-  ( ph -> ( K i^i L ) = { ( 0g ` G ) } )
68 66 5 26 42 ablcntzd 
 |-  ( ph -> K C_ ( ( Cntz ` G ) ` L ) )
69 62 61 66 26 42 67 68 20 51 lsmhash 
 |-  ( ph -> ( # ` ( K ( LSSum ` G ) L ) ) = ( ( # ` K ) x. ( # ` L ) ) )
70 65 69 eqtr3d 
 |-  ( ph -> ( # ` B ) = ( ( # ` K ) x. ( # ` L ) ) )
71 70 9 eqtr3d 
 |-  ( ph -> ( ( # ` K ) x. ( # ` L ) ) = ( M x. N ) )
72 60 71 breqtrrd 
 |-  ( ph -> ( M x. ( # ` L ) ) || ( ( # ` K ) x. ( # ` L ) ) )
73 61 subg0cl 
 |-  ( L e. ( SubGrp ` G ) -> ( 0g ` G ) e. L )
74 ne0i 
 |-  ( ( 0g ` G ) e. L -> L =/= (/) )
75 42 73 74 3syl 
 |-  ( ph -> L =/= (/) )
76 hashnncl 
 |-  ( L e. Fin -> ( ( # ` L ) e. NN <-> L =/= (/) ) )
77 51 76 syl 
 |-  ( ph -> ( ( # ` L ) e. NN <-> L =/= (/) ) )
78 75 77 mpbird 
 |-  ( ph -> ( # ` L ) e. NN )
79 78 nnne0d 
 |-  ( ph -> ( # ` L ) =/= 0 )
80 dvdsmulcr 
 |-  ( ( M e. ZZ /\ ( # ` K ) e. ZZ /\ ( ( # ` L ) e. ZZ /\ ( # ` L ) =/= 0 ) ) -> ( ( M x. ( # ` L ) ) || ( ( # ` K ) x. ( # ` L ) ) <-> M || ( # ` K ) ) )
81 23 35 54 79 80 syl112anc 
 |-  ( ph -> ( ( M x. ( # ` L ) ) || ( ( # ` K ) x. ( # ` L ) ) <-> M || ( # ` K ) ) )
82 72 81 mpbid 
 |-  ( ph -> M || ( # ` K ) )
83 dvdseq 
 |-  ( ( ( ( # ` K ) e. NN0 /\ M e. NN0 ) /\ ( ( # ` K ) || M /\ M || ( # ` K ) ) ) -> ( # ` K ) = M )
84 22 10 39 82 83 syl22anc 
 |-  ( ph -> ( # ` K ) = M )
85 dvdsmulc 
 |-  ( ( ( # ` K ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( # ` K ) || M -> ( ( # ` K ) x. N ) || ( M x. N ) ) )
86 35 23 36 85 syl3anc 
 |-  ( ph -> ( ( # ` K ) || M -> ( ( # ` K ) x. N ) || ( M x. N ) ) )
87 39 86 mpd 
 |-  ( ph -> ( ( # ` K ) x. N ) || ( M x. N ) )
88 87 71 breqtrrd 
 |-  ( ph -> ( ( # ` K ) x. N ) || ( ( # ` K ) x. ( # ` L ) ) )
89 84 6 eqeltrd 
 |-  ( ph -> ( # ` K ) e. NN )
90 89 nnne0d 
 |-  ( ph -> ( # ` K ) =/= 0 )
91 dvdscmulr 
 |-  ( ( N e. ZZ /\ ( # ` L ) e. ZZ /\ ( ( # ` K ) e. ZZ /\ ( # ` K ) =/= 0 ) ) -> ( ( ( # ` K ) x. N ) || ( ( # ` K ) x. ( # ` L ) ) <-> N || ( # ` L ) ) )
92 36 54 35 90 91 syl112anc 
 |-  ( ph -> ( ( ( # ` K ) x. N ) || ( ( # ` K ) x. ( # ` L ) ) <-> N || ( # ` L ) ) )
93 88 92 mpbid 
 |-  ( ph -> N || ( # ` L ) )
94 dvdseq 
 |-  ( ( ( ( # ` L ) e. NN0 /\ N e. NN0 ) /\ ( ( # ` L ) || N /\ N || ( # ` L ) ) ) -> ( # ` L ) = N )
95 53 11 57 93 94 syl22anc 
 |-  ( ph -> ( # ` L ) = N )
96 84 95 jca 
 |-  ( ph -> ( ( # ` K ) = M /\ ( # ` L ) = N ) )