Proof of Theorem ablfacrp2
Step | Hyp | Ref
| Expression |
1 | | ablfacrp.2 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐵) = (𝑀 · 𝑁)) |
2 | | ablfacrp.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | 2 | nnnn0d 11351 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
4 | | ablfacrp.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 4 | nnnn0d 11351 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | 3, 5 | nn0mulcld 11356 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑁) ∈
ℕ0) |
7 | 1, 6 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → (#‘𝐵) ∈
ℕ0) |
8 | | ablfacrp.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
9 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐺)
∈ V |
10 | 8, 9 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐵 ∈ V |
11 | | hashclb 13149 |
. . . . . . 7
⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔
(#‘𝐵) ∈
ℕ0)) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ (𝐵 ∈ Fin ↔
(#‘𝐵) ∈
ℕ0) |
13 | 7, 12 | sylibr 224 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ Fin) |
14 | | ablfacrp.k |
. . . . . 6
⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} |
15 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ⊆ 𝐵 |
16 | 14, 15 | eqsstri 3635 |
. . . . 5
⊢ 𝐾 ⊆ 𝐵 |
17 | | ssfi 8180 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ 𝐾 ⊆ 𝐵) → 𝐾 ∈ Fin) |
18 | 13, 16, 17 | sylancl 694 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Fin) |
19 | | hashcl 13147 |
. . . 4
⊢ (𝐾 ∈ Fin →
(#‘𝐾) ∈
ℕ0) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝜑 → (#‘𝐾) ∈
ℕ0) |
21 | | ablfacrp.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ Abel) |
22 | 2 | nnzd 11481 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
23 | | ablfacrp.o |
. . . . . . . . 9
⊢ 𝑂 = (od‘𝐺) |
24 | 23, 8 | oddvdssubg 18258 |
. . . . . . . 8
⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
25 | 21, 22, 24 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺)) |
26 | 14, 25 | syl5eqel 2705 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
27 | 8 | lagsubg 17656 |
. . . . . 6
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (#‘𝐾) ∥ (#‘𝐵)) |
28 | 26, 13, 27 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (#‘𝐾) ∥ (#‘𝐵)) |
29 | 2 | nncnd 11036 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
30 | 4 | nncnd 11036 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
31 | 29, 30 | mulcomd 10061 |
. . . . . 6
⊢ (𝜑 → (𝑀 · 𝑁) = (𝑁 · 𝑀)) |
32 | 1, 31 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (#‘𝐵) = (𝑁 · 𝑀)) |
33 | 28, 32 | breqtrd 4679 |
. . . 4
⊢ (𝜑 → (#‘𝐾) ∥ (𝑁 · 𝑀)) |
34 | | ablfacrp.l |
. . . . 5
⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} |
35 | | ablfacrp.1 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) |
36 | 8, 23, 14, 34, 21, 2, 4, 35, 1 | ablfacrplem 18464 |
. . . 4
⊢ (𝜑 → ((#‘𝐾) gcd 𝑁) = 1) |
37 | 20 | nn0zd 11480 |
. . . . 5
⊢ (𝜑 → (#‘𝐾) ∈ ℤ) |
38 | 4 | nnzd 11481 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
39 | | coprmdvds 15366 |
. . . . 5
⊢
(((#‘𝐾) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑀 ∈
ℤ) → (((#‘𝐾) ∥ (𝑁 · 𝑀) ∧ ((#‘𝐾) gcd 𝑁) = 1) → (#‘𝐾) ∥ 𝑀)) |
40 | 37, 38, 22, 39 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (((#‘𝐾) ∥ (𝑁 · 𝑀) ∧ ((#‘𝐾) gcd 𝑁) = 1) → (#‘𝐾) ∥ 𝑀)) |
41 | 33, 36, 40 | mp2and 715 |
. . 3
⊢ (𝜑 → (#‘𝐾) ∥ 𝑀) |
42 | 23, 8 | oddvdssubg 18258 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺)) |
43 | 21, 38, 42 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺)) |
44 | 34, 43 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ (SubGrp‘𝐺)) |
45 | 8 | lagsubg 17656 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (#‘𝐿) ∥ (#‘𝐵)) |
46 | 44, 13, 45 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐿) ∥ (#‘𝐵)) |
47 | 46, 1 | breqtrd 4679 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐿) ∥ (𝑀 · 𝑁)) |
48 | | gcdcom 15235 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
49 | 22, 38, 48 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
50 | 49, 35 | eqtr3d 2658 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 gcd 𝑀) = 1) |
51 | 8, 23, 34, 14, 21, 4, 2, 50, 32 | ablfacrplem 18464 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝐿) gcd 𝑀) = 1) |
52 | | ssrab2 3687 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ⊆ 𝐵 |
53 | 34, 52 | eqsstri 3635 |
. . . . . . . . . . 11
⊢ 𝐿 ⊆ 𝐵 |
54 | | ssfi 8180 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ 𝐿 ⊆ 𝐵) → 𝐿 ∈ Fin) |
55 | 13, 53, 54 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ Fin) |
56 | | hashcl 13147 |
. . . . . . . . . 10
⊢ (𝐿 ∈ Fin →
(#‘𝐿) ∈
ℕ0) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐿) ∈
ℕ0) |
58 | 57 | nn0zd 11480 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐿) ∈ ℤ) |
59 | | coprmdvds 15366 |
. . . . . . . 8
⊢
(((#‘𝐿) ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (((#‘𝐿) ∥ (𝑀 · 𝑁) ∧ ((#‘𝐿) gcd 𝑀) = 1) → (#‘𝐿) ∥ 𝑁)) |
60 | 58, 22, 38, 59 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (((#‘𝐿) ∥ (𝑀 · 𝑁) ∧ ((#‘𝐿) gcd 𝑀) = 1) → (#‘𝐿) ∥ 𝑁)) |
61 | 47, 51, 60 | mp2and 715 |
. . . . . 6
⊢ (𝜑 → (#‘𝐿) ∥ 𝑁) |
62 | | dvdscmul 15008 |
. . . . . . 7
⊢
(((#‘𝐿) ∈
ℤ ∧ 𝑁 ∈
ℤ ∧ 𝑀 ∈
ℤ) → ((#‘𝐿) ∥ 𝑁 → (𝑀 · (#‘𝐿)) ∥ (𝑀 · 𝑁))) |
63 | 58, 38, 22, 62 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → ((#‘𝐿) ∥ 𝑁 → (𝑀 · (#‘𝐿)) ∥ (𝑀 · 𝑁))) |
64 | 61, 63 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝑀 · (#‘𝐿)) ∥ (𝑀 · 𝑁)) |
65 | | eqid 2622 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
66 | | eqid 2622 |
. . . . . . . . . 10
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
67 | 8, 23, 14, 34, 21, 2, 4, 35, 1,
65, 66 | ablfacrp 18465 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾 ∩ 𝐿) = {(0g‘𝐺)} ∧ (𝐾(LSSum‘𝐺)𝐿) = 𝐵)) |
68 | 67 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → (𝐾(LSSum‘𝐺)𝐿) = 𝐵) |
69 | 68 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝐾(LSSum‘𝐺)𝐿)) = (#‘𝐵)) |
70 | | eqid 2622 |
. . . . . . . 8
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
71 | 67 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∩ 𝐿) = {(0g‘𝐺)}) |
72 | 70, 21, 26, 44 | ablcntzd 18260 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ⊆ ((Cntz‘𝐺)‘𝐿)) |
73 | 66, 65, 70, 26, 44, 71, 72, 18, 55 | lsmhash 18118 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝐾(LSSum‘𝐺)𝐿)) = ((#‘𝐾) · (#‘𝐿))) |
74 | 69, 73 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → (#‘𝐵) = ((#‘𝐾) · (#‘𝐿))) |
75 | 74, 1 | eqtr3d 2658 |
. . . . 5
⊢ (𝜑 → ((#‘𝐾) · (#‘𝐿)) = (𝑀 · 𝑁)) |
76 | 64, 75 | breqtrrd 4681 |
. . . 4
⊢ (𝜑 → (𝑀 · (#‘𝐿)) ∥ ((#‘𝐾) · (#‘𝐿))) |
77 | 65 | subg0cl 17602 |
. . . . . . . 8
⊢ (𝐿 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝐿) |
78 | | ne0i 3921 |
. . . . . . . 8
⊢
((0g‘𝐺) ∈ 𝐿 → 𝐿 ≠ ∅) |
79 | 44, 77, 78 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ≠ ∅) |
80 | | hashnncl 13157 |
. . . . . . . 8
⊢ (𝐿 ∈ Fin →
((#‘𝐿) ∈ ℕ
↔ 𝐿 ≠
∅)) |
81 | 55, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝐿) ∈ ℕ ↔ 𝐿 ≠ ∅)) |
82 | 79, 81 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → (#‘𝐿) ∈ ℕ) |
83 | 82 | nnne0d 11065 |
. . . . 5
⊢ (𝜑 → (#‘𝐿) ≠ 0) |
84 | | dvdsmulcr 15011 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧
(#‘𝐾) ∈ ℤ
∧ ((#‘𝐿) ∈
ℤ ∧ (#‘𝐿)
≠ 0)) → ((𝑀
· (#‘𝐿))
∥ ((#‘𝐾)
· (#‘𝐿))
↔ 𝑀 ∥
(#‘𝐾))) |
85 | 22, 37, 58, 83, 84 | syl112anc 1330 |
. . . 4
⊢ (𝜑 → ((𝑀 · (#‘𝐿)) ∥ ((#‘𝐾) · (#‘𝐿)) ↔ 𝑀 ∥ (#‘𝐾))) |
86 | 76, 85 | mpbid 222 |
. . 3
⊢ (𝜑 → 𝑀 ∥ (#‘𝐾)) |
87 | | dvdseq 15036 |
. . 3
⊢
((((#‘𝐾)
∈ ℕ0 ∧ 𝑀 ∈ ℕ0) ∧
((#‘𝐾) ∥ 𝑀 ∧ 𝑀 ∥ (#‘𝐾))) → (#‘𝐾) = 𝑀) |
88 | 20, 3, 41, 86, 87 | syl22anc 1327 |
. 2
⊢ (𝜑 → (#‘𝐾) = 𝑀) |
89 | | dvdsmulc 15009 |
. . . . . . 7
⊢
(((#‘𝐾) ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) → ((#‘𝐾) ∥ 𝑀 → ((#‘𝐾) · 𝑁) ∥ (𝑀 · 𝑁))) |
90 | 37, 22, 38, 89 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → ((#‘𝐾) ∥ 𝑀 → ((#‘𝐾) · 𝑁) ∥ (𝑀 · 𝑁))) |
91 | 41, 90 | mpd 15 |
. . . . 5
⊢ (𝜑 → ((#‘𝐾) · 𝑁) ∥ (𝑀 · 𝑁)) |
92 | 91, 75 | breqtrrd 4681 |
. . . 4
⊢ (𝜑 → ((#‘𝐾) · 𝑁) ∥ ((#‘𝐾) · (#‘𝐿))) |
93 | 88, 2 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → (#‘𝐾) ∈ ℕ) |
94 | 93 | nnne0d 11065 |
. . . . 5
⊢ (𝜑 → (#‘𝐾) ≠ 0) |
95 | | dvdscmulr 15010 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧
(#‘𝐿) ∈ ℤ
∧ ((#‘𝐾) ∈
ℤ ∧ (#‘𝐾)
≠ 0)) → (((#‘𝐾) · 𝑁) ∥ ((#‘𝐾) · (#‘𝐿)) ↔ 𝑁 ∥ (#‘𝐿))) |
96 | 38, 58, 37, 94, 95 | syl112anc 1330 |
. . . 4
⊢ (𝜑 → (((#‘𝐾) · 𝑁) ∥ ((#‘𝐾) · (#‘𝐿)) ↔ 𝑁 ∥ (#‘𝐿))) |
97 | 92, 96 | mpbid 222 |
. . 3
⊢ (𝜑 → 𝑁 ∥ (#‘𝐿)) |
98 | | dvdseq 15036 |
. . 3
⊢
((((#‘𝐿)
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧
((#‘𝐿) ∥ 𝑁 ∧ 𝑁 ∥ (#‘𝐿))) → (#‘𝐿) = 𝑁) |
99 | 57, 5, 61, 97, 98 | syl22anc 1327 |
. 2
⊢ (𝜑 → (#‘𝐿) = 𝑁) |
100 | 88, 99 | jca 554 |
1
⊢ (𝜑 → ((#‘𝐾) = 𝑀 ∧ (#‘𝐿) = 𝑁)) |