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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfacrp.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfacrp.k ⊢ 𝐾 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 }
ablfacrp.l ⊢ 𝐿 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 }
ablfacrp.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfacrp.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
ablfacrp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ablfacrp.1 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
ablfacrp.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) )
Assertion ablfacrp2 ( 𝜑 → ( ( ♯ ‘ 𝐾 ) = 𝑀 ∧ ( ♯ ‘ 𝐿 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 ablfacrp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfacrp.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 ablfacrp.k ⊢ 𝐾 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 }
4 ablfacrp.l ⊢ 𝐿 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 }
5 ablfacrp.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
6 ablfacrp.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 ablfacrp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8 ablfacrp.1 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
9 ablfacrp.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) )
10 6 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
11 7 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 10 11 nn0mulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℕ0 )
13 9 12 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
14 1 fvexi ⊢ 𝐵 ∈ V
15 hashclb ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) )
16 14 15 ax-mp ⊢ ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
17 13 16 sylibr ⊢ ( 𝜑 → 𝐵 ∈ Fin )
18 3 ssrab3 ⊢ 𝐾 ⊆ 𝐵
19 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐾 ⊆ 𝐵 ) → 𝐾 ∈ Fin )
20 17 18 19 sylancl ⊢ ( 𝜑 → 𝐾 ∈ Fin )
21 hashcl ⊢ ( 𝐾 ∈ Fin → ( ♯ ‘ 𝐾 ) ∈ ℕ0 )
22 20 21 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℕ0 )
23 6 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
24 2 1 oddvdssubg ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∈ ( SubGrp ‘ 𝐺 ) )
25 5 23 24 syl2anc ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∈ ( SubGrp ‘ 𝐺 ) )
26 3 25 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
27 1 lagsubg ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝐵 ) )
28 26 17 27 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∥ ( ♯ ‘ 𝐵 ) )
29 6 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
30 7 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
31 29 30 mulcomd ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) = ( 𝑁 · 𝑀 ) )
32 9 31 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑁 · 𝑀 ) )
33 28 32 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∥ ( 𝑁 · 𝑀 ) )
34 1 2 3 4 5 6 7 8 9 ablfacrplem ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 )
35 22 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℤ )
36 7 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
37 coprmdvds ⊢ ( ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ( ♯ ‘ 𝐾 ) ∥ ( 𝑁 · 𝑀 ) ∧ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 ) → ( ♯ ‘ 𝐾 ) ∥ 𝑀 ) )
38 35 36 23 37 syl3anc ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐾 ) ∥ ( 𝑁 · 𝑀 ) ∧ ( ( ♯ ‘ 𝐾 ) gcd 𝑁 ) = 1 ) → ( ♯ ‘ 𝐾 ) ∥ 𝑀 ) )
39 33 34 38 mp2and ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∥ 𝑀 )
40 2 1 oddvdssubg ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) )
41 5 36 40 syl2anc ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) )
42 4 41 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ ( SubGrp ‘ 𝐺 ) )
43 1 lagsubg ⊢ ( ( 𝐿 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐿 ) ∥ ( ♯ ‘ 𝐵 ) )
44 42 17 43 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) ∥ ( ♯ ‘ 𝐵 ) )
45 44 9 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) ∥ ( 𝑀 · 𝑁 ) )
46 23 36 gcdcomd ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = ( 𝑁 gcd 𝑀 ) )
47 46 8 eqtr3d ⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = 1 )
48 1 2 4 3 5 7 6 47 32 ablfacrplem ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐿 ) gcd 𝑀 ) = 1 )
49 4 ssrab3 ⊢ 𝐿 ⊆ 𝐵
50 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐿 ⊆ 𝐵 ) → 𝐿 ∈ Fin )
51 17 49 50 sylancl ⊢ ( 𝜑 → 𝐿 ∈ Fin )
52 hashcl ⊢ ( 𝐿 ∈ Fin → ( ♯ ‘ 𝐿 ) ∈ ℕ0 )
53 51 52 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) ∈ ℕ0 )
54 53 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) ∈ ℤ )
55 coprmdvds ⊢ ( ( ( ♯ ‘ 𝐿 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ♯ ‘ 𝐿 ) ∥ ( 𝑀 · 𝑁 ) ∧ ( ( ♯ ‘ 𝐿 ) gcd 𝑀 ) = 1 ) → ( ♯ ‘ 𝐿 ) ∥ 𝑁 ) )
56 54 23 36 55 syl3anc ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐿 ) ∥ ( 𝑀 · 𝑁 ) ∧ ( ( ♯ ‘ 𝐿 ) gcd 𝑀 ) = 1 ) → ( ♯ ‘ 𝐿 ) ∥ 𝑁 ) )
57 45 48 56 mp2and ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) ∥ 𝑁 )
58 dvdscmul ⊢ ( ( ( ♯ ‘ 𝐿 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( ♯ ‘ 𝐿 ) ∥ 𝑁 → ( 𝑀 · ( ♯ ‘ 𝐿 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
59 54 36 23 58 syl3anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐿 ) ∥ 𝑁 → ( 𝑀 · ( ♯ ‘ 𝐿 ) ) ∥ ( 𝑀 · 𝑁 ) ) )
60 57 59 mpd ⊢ ( 𝜑 → ( 𝑀 · ( ♯ ‘ 𝐿 ) ) ∥ ( 𝑀 · 𝑁 ) )
61 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
62 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
63 1 2 3 4 5 6 7 8 9 61 62 ablfacrp ⊢ ( 𝜑 → ( ( 𝐾 ∩ 𝐿 ) = { ( 0g ‘ 𝐺 ) } ∧ ( 𝐾 ( LSSum ‘ 𝐺 ) 𝐿 ) = 𝐵 ) )
64 63 simprd ⊢ ( 𝜑 → ( 𝐾 ( LSSum ‘ 𝐺 ) 𝐿 ) = 𝐵 )
65 64 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐾 ( LSSum ‘ 𝐺 ) 𝐿 ) ) = ( ♯ ‘ 𝐵 ) )
66 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
67 63 simpld ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐿 ) = { ( 0g ‘ 𝐺 ) } )
68 66 5 26 42 ablcntzd ⊢ ( 𝜑 → 𝐾 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ 𝐿 ) )
69 62 61 66 26 42 67 68 20 51 lsmhash ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐾 ( LSSum ‘ 𝐺 ) 𝐿 ) ) = ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) )
70 65 69 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) )
71 70 9 eqtr3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) = ( 𝑀 · 𝑁 ) )
72 60 71 breqtrrd ⊢ ( 𝜑 → ( 𝑀 · ( ♯ ‘ 𝐿 ) ) ∥ ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) )
73 61 subg0cl ⊢ ( 𝐿 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝐿 )
74 ne0i ⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝐿 → 𝐿 ≠ ∅ )
75 42 73 74 3syl ⊢ ( 𝜑 → 𝐿 ≠ ∅ )
76 hashnncl ⊢ ( 𝐿 ∈ Fin → ( ( ♯ ‘ 𝐿 ) ∈ ℕ ↔ 𝐿 ≠ ∅ ) )
77 51 76 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐿 ) ∈ ℕ ↔ 𝐿 ≠ ∅ ) )
78 75 77 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) ∈ ℕ )
79 78 nnne0d ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) ≠ 0 )
80 dvdsmulcr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐿 ) ∈ ℤ ∧ ( ♯ ‘ 𝐿 ) ≠ 0 ) ) → ( ( 𝑀 · ( ♯ ‘ 𝐿 ) ) ∥ ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) ↔ 𝑀 ∥ ( ♯ ‘ 𝐾 ) ) )
81 23 35 54 79 80 syl112anc ⊢ ( 𝜑 → ( ( 𝑀 · ( ♯ ‘ 𝐿 ) ) ∥ ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) ↔ 𝑀 ∥ ( ♯ ‘ 𝐾 ) ) )
82 72 81 mpbid ⊢ ( 𝜑 → 𝑀 ∥ ( ♯ ‘ 𝐾 ) )
83 dvdseq ⊢ ( ( ( ( ♯ ‘ 𝐾 ) ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝐾 ) ∥ 𝑀 ∧ 𝑀 ∥ ( ♯ ‘ 𝐾 ) ) ) → ( ♯ ‘ 𝐾 ) = 𝑀 )
84 22 10 39 82 83 syl22anc ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) = 𝑀 )
85 dvdsmulc ⊢ ( ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ♯ ‘ 𝐾 ) ∥ 𝑀 → ( ( ♯ ‘ 𝐾 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
86 35 23 36 85 syl3anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) ∥ 𝑀 → ( ( ♯ ‘ 𝐾 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
87 39 86 mpd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) )
88 87 71 breqtrrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) · 𝑁 ) ∥ ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) )
89 84 6 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ∈ ℕ )
90 89 nnne0d ⊢ ( 𝜑 → ( ♯ ‘ 𝐾 ) ≠ 0 )
91 dvdscmulr ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝐿 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐾 ) ∈ ℤ ∧ ( ♯ ‘ 𝐾 ) ≠ 0 ) ) → ( ( ( ♯ ‘ 𝐾 ) · 𝑁 ) ∥ ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) ↔ 𝑁 ∥ ( ♯ ‘ 𝐿 ) ) )
92 36 54 35 90 91 syl112anc ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐾 ) · 𝑁 ) ∥ ( ( ♯ ‘ 𝐾 ) · ( ♯ ‘ 𝐿 ) ) ↔ 𝑁 ∥ ( ♯ ‘ 𝐿 ) ) )
93 88 92 mpbid ⊢ ( 𝜑 → 𝑁 ∥ ( ♯ ‘ 𝐿 ) )
94 dvdseq ⊢ ( ( ( ( ♯ ‘ 𝐿 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝐿 ) ∥ 𝑁 ∧ 𝑁 ∥ ( ♯ ‘ 𝐿 ) ) ) → ( ♯ ‘ 𝐿 ) = 𝑁 )
95 53 11 57 93 94 syl22anc ⊢ ( 𝜑 → ( ♯ ‘ 𝐿 ) = 𝑁 )
96 84 95 jca ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐾 ) = 𝑀 ∧ ( ♯ ‘ 𝐿 ) = 𝑁 ) )