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