Proof of Theorem ablfacrp2
Step | Hyp | Ref
| Expression |
1 | | ablfacrp.2 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) |
2 | | ablfacrp.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | 2 | nnnn0d 11958 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
4 | | ablfacrp.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 4 | nnnn0d 11958 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | 3, 5 | nn0mulcld 11963 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑁) ∈
ℕ0) |
7 | 1, 6 | eqeltrd 2916 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) |
8 | | ablfacrp.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
9 | 8 | fvexi 6687 |
. . . . . . 7
⊢ 𝐵 ∈ V |
10 | | hashclb 13722 |
. . . . . . 7
⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0)) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ (𝐵 ∈ Fin ↔
(♯‘𝐵) ∈
ℕ0) |
12 | 7, 11 | sylibr 236 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ Fin) |
13 | | ablfacrp.k |
. . . . . 6
⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} |
14 | 13 | ssrab3 4060 |
. . . . 5
⊢ 𝐾 ⊆ 𝐵 |
15 | | ssfi 8741 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ 𝐾 ⊆ 𝐵) → 𝐾 ∈ Fin) |
16 | 12, 14, 15 | sylancl 588 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Fin) |
17 | | hashcl 13720 |
. . . 4
⊢ (𝐾 ∈ Fin →
(♯‘𝐾) ∈
ℕ0) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → (♯‘𝐾) ∈
ℕ0) |
19 | | ablfacrp.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Abel) |
20 | 2 | nnzd 12089 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
21 | | ablfacrp.o |
. . . . . . . . 9
⊢ 𝑂 = (od‘𝐺) |
22 | 21, 8 | oddvdssubg 18978 |
. . . . . . . 8
⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
23 | 19, 20, 22 | syl2anc 586 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
24 | 13, 23 | eqeltrid 2920 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
25 | 8 | lagsubg 18345 |
. . . . . 6
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘𝐾) ∥ (♯‘𝐵)) |
26 | 24, 12, 25 | syl2anc 586 |
. . . . 5
⊢ (𝜑 → (♯‘𝐾) ∥ (♯‘𝐵)) |
27 | 2 | nncnd 11657 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
28 | 4 | nncnd 11657 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
29 | 27, 28 | mulcomd 10665 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
30 | 1, 29 | eqtrd 2859 |
. . . . 5
⊢ (𝜑 → (♯‘𝐵) = (𝑁 · 𝑀)) |
31 | 26, 30 | breqtrd 5095 |
. . . 4
⊢ (𝜑 → (♯‘𝐾) ∥ (𝑁 · 𝑀)) |
32 | | ablfacrp.l |
. . . . 5
⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} |
33 | | ablfacrp.1 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
34 | 8, 21, 13, 32, 19, 2, 4, 33, 1 | ablfacrplem 19190 |
. . . 4
⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1) |
35 | 18 | nn0zd 12088 |
. . . . 5
⊢ (𝜑 → (♯‘𝐾) ∈
ℤ) |
36 | 4 | nnzd 12089 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
37 | | coprmdvds 16000 |
. . . . 5
⊢
(((♯‘𝐾)
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 𝑀
∈ ℤ) → (((♯‘𝐾) ∥ (𝑁 · 𝑀) ∧ ((♯‘𝐾) gcd 𝑁) = 1) → (♯‘𝐾) ∥ 𝑀)) |
38 | 35, 36, 20, 37 | syl3anc 1367 |
. . . 4
⊢ (𝜑 → (((♯‘𝐾) ∥ (𝑁 · 𝑀) ∧ ((♯‘𝐾) gcd 𝑁) = 1) → (♯‘𝐾) ∥ 𝑀)) |
39 | 31, 34, 38 | mp2and 697 |
. . 3
⊢ (𝜑 → (♯‘𝐾) ∥ 𝑀) |
40 | 21, 8 | oddvdssubg 18978 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺)) |
41 | 19, 36, 40 | syl2anc 586 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺)) |
42 | 32, 41 | eqeltrid 2920 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ (SubGrp‘𝐺)) |
43 | 8 | lagsubg 18345 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘𝐿) ∥ (♯‘𝐵)) |
44 | 42, 12, 43 | syl2anc 586 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐿) ∥ (♯‘𝐵)) |
45 | 44, 1 | breqtrd 5095 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐿) ∥ (𝑀 · 𝑁)) |
46 | | gcdcom 15865 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
47 | 20, 36, 46 | syl2anc 586 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
48 | 47, 33 | eqtr3d 2861 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 gcd 𝑀) = 1) |
49 | 8, 21, 32, 13, 19, 4, 2, 48, 30 | ablfacrplem 19190 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝐿) gcd 𝑀) = 1) |
50 | 32 | ssrab3 4060 |
. . . . . . . . . . 11
⊢ 𝐿 ⊆ 𝐵 |
51 | | ssfi 8741 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ 𝐿 ⊆ 𝐵) → 𝐿 ∈ Fin) |
52 | 12, 50, 51 | sylancl 588 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ Fin) |
53 | | hashcl 13720 |
. . . . . . . . . 10
⊢ (𝐿 ∈ Fin →
(♯‘𝐿) ∈
ℕ0) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐿) ∈
ℕ0) |
55 | 54 | nn0zd 12088 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐿) ∈
ℤ) |
56 | | coprmdvds 16000 |
. . . . . . . 8
⊢
(((♯‘𝐿)
∈ ℤ ∧ 𝑀
∈ ℤ ∧ 𝑁
∈ ℤ) → (((♯‘𝐿) ∥ (𝑀 · 𝑁) ∧ ((♯‘𝐿) gcd 𝑀) = 1) → (♯‘𝐿) ∥ 𝑁)) |
57 | 55, 20, 36, 56 | syl3anc 1367 |
. . . . . . 7
⊢ (𝜑 → (((♯‘𝐿) ∥ (𝑀 · 𝑁) ∧ ((♯‘𝐿) gcd 𝑀) = 1) → (♯‘𝐿) ∥ 𝑁)) |
58 | 45, 49, 57 | mp2and 697 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐿) ∥ 𝑁) |
59 | | dvdscmul 15639 |
. . . . . . 7
⊢
(((♯‘𝐿)
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 𝑀
∈ ℤ) → ((♯‘𝐿) ∥ 𝑁 → (𝑀 · (♯‘𝐿)) ∥ (𝑀 · 𝑁))) |
60 | 55, 36, 20, 59 | syl3anc 1367 |
. . . . . 6
⊢ (𝜑 → ((♯‘𝐿) ∥ 𝑁 → (𝑀 · (♯‘𝐿)) ∥ (𝑀 · 𝑁))) |
61 | 58, 60 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝑀 · (♯‘𝐿)) ∥ (𝑀 · 𝑁)) |
62 | | eqid 2824 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
63 | | eqid 2824 |
. . . . . . . . . 10
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
64 | 8, 21, 13, 32, 19, 2, 4, 33, 1,
62, 63 | ablfacrp 19191 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾 ∩ 𝐿) = {(0g‘𝐺)} ∧ (𝐾(LSSum‘𝐺)𝐿) = 𝐵)) |
65 | 64 | simprd 498 |
. . . . . . . 8
⊢ (𝜑 → (𝐾(LSSum‘𝐺)𝐿) = 𝐵) |
66 | 65 | fveq2d 6677 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐾(LSSum‘𝐺)𝐿)) = (♯‘𝐵)) |
67 | | eqid 2824 |
. . . . . . . 8
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
68 | 64 | simpld 497 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∩ 𝐿) = {(0g‘𝐺)}) |
69 | 67, 19, 24, 42 | ablcntzd 18980 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ⊆ ((Cntz‘𝐺)‘𝐿)) |
70 | 63, 62, 67, 24, 42, 68, 69, 16, 52 | lsmhash 18834 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐾(LSSum‘𝐺)𝐿)) = ((♯‘𝐾) · (♯‘𝐿))) |
71 | 66, 70 | eqtr3d 2861 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐵) = ((♯‘𝐾) · (♯‘𝐿))) |
72 | 71, 1 | eqtr3d 2861 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐾) · (♯‘𝐿)) = (𝑀 · 𝑁)) |
73 | 61, 72 | breqtrrd 5097 |
. . . 4
⊢ (𝜑 → (𝑀 · (♯‘𝐿)) ∥ ((♯‘𝐾) · (♯‘𝐿))) |
74 | 62 | subg0cl 18290 |
. . . . . . . 8
⊢ (𝐿 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝐿) |
75 | | ne0i 4303 |
. . . . . . . 8
⊢
((0g‘𝐺) ∈ 𝐿 → 𝐿 ≠ ∅) |
76 | 42, 74, 75 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ≠ ∅) |
77 | | hashnncl 13730 |
. . . . . . . 8
⊢ (𝐿 ∈ Fin →
((♯‘𝐿) ∈
ℕ ↔ 𝐿 ≠
∅)) |
78 | 52, 77 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝐿) ∈ ℕ ↔ 𝐿 ≠ ∅)) |
79 | 76, 78 | mpbird 259 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐿) ∈
ℕ) |
80 | 79 | nnne0d 11690 |
. . . . 5
⊢ (𝜑 → (♯‘𝐿) ≠ 0) |
81 | | dvdsmulcr 15642 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧
(♯‘𝐾) ∈
ℤ ∧ ((♯‘𝐿) ∈ ℤ ∧ (♯‘𝐿) ≠ 0)) → ((𝑀 · (♯‘𝐿)) ∥ ((♯‘𝐾) · (♯‘𝐿)) ↔ 𝑀 ∥ (♯‘𝐾))) |
82 | 20, 35, 55, 80, 81 | syl112anc 1370 |
. . . 4
⊢ (𝜑 → ((𝑀 · (♯‘𝐿)) ∥ ((♯‘𝐾) · (♯‘𝐿)) ↔ 𝑀 ∥ (♯‘𝐾))) |
83 | 73, 82 | mpbid 234 |
. . 3
⊢ (𝜑 → 𝑀 ∥ (♯‘𝐾)) |
84 | | dvdseq 15667 |
. . 3
⊢
((((♯‘𝐾)
∈ ℕ0 ∧ 𝑀 ∈ ℕ0) ∧
((♯‘𝐾) ∥
𝑀 ∧ 𝑀 ∥ (♯‘𝐾))) → (♯‘𝐾) = 𝑀) |
85 | 18, 3, 39, 83, 84 | syl22anc 836 |
. 2
⊢ (𝜑 → (♯‘𝐾) = 𝑀) |
86 | | dvdsmulc 15640 |
. . . . . . 7
⊢
(((♯‘𝐾)
∈ ℤ ∧ 𝑀
∈ ℤ ∧ 𝑁
∈ ℤ) → ((♯‘𝐾) ∥ 𝑀 → ((♯‘𝐾) · 𝑁) ∥ (𝑀 · 𝑁))) |
87 | 35, 20, 36, 86 | syl3anc 1367 |
. . . . . 6
⊢ (𝜑 → ((♯‘𝐾) ∥ 𝑀 → ((♯‘𝐾) · 𝑁) ∥ (𝑀 · 𝑁))) |
88 | 39, 87 | mpd 15 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐾) · 𝑁) ∥ (𝑀 · 𝑁)) |
89 | 88, 72 | breqtrrd 5097 |
. . . 4
⊢ (𝜑 → ((♯‘𝐾) · 𝑁) ∥ ((♯‘𝐾) · (♯‘𝐿))) |
90 | 85, 2 | eqeltrd 2916 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐾) ∈
ℕ) |
91 | 90 | nnne0d 11690 |
. . . . 5
⊢ (𝜑 → (♯‘𝐾) ≠ 0) |
92 | | dvdscmulr 15641 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝐿) ∈
ℤ ∧ ((♯‘𝐾) ∈ ℤ ∧ (♯‘𝐾) ≠ 0)) →
(((♯‘𝐾)
· 𝑁) ∥
((♯‘𝐾) ·
(♯‘𝐿)) ↔
𝑁 ∥
(♯‘𝐿))) |
93 | 36, 55, 35, 91, 92 | syl112anc 1370 |
. . . 4
⊢ (𝜑 → (((♯‘𝐾) · 𝑁) ∥ ((♯‘𝐾) · (♯‘𝐿)) ↔ 𝑁 ∥ (♯‘𝐿))) |
94 | 89, 93 | mpbid 234 |
. . 3
⊢ (𝜑 → 𝑁 ∥ (♯‘𝐿)) |
95 | | dvdseq 15667 |
. . 3
⊢
((((♯‘𝐿)
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧
((♯‘𝐿) ∥
𝑁 ∧ 𝑁 ∥ (♯‘𝐿))) → (♯‘𝐿) = 𝑁) |
96 | 54, 5, 58, 94, 95 | syl22anc 836 |
. 2
⊢ (𝜑 → (♯‘𝐿) = 𝑁) |
97 | 85, 96 | jca 514 |
1
⊢ (𝜑 → ((♯‘𝐾) = 𝑀 ∧ (♯‘𝐿) = 𝑁)) |