Step | Hyp | Ref
| Expression |
1 | | ablfac1.f |
. 2
⊢ (𝜑 → 𝐵 ∈ Fin) |
2 | | ablfac1.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
3 | 2 | dprdssv 18238 |
. . 3
⊢ (𝐺 DProd 𝑆) ⊆ 𝐵 |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑆) ⊆ 𝐵) |
5 | | ssfi 8065 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd 𝑆) ⊆ 𝐵) → (𝐺 DProd 𝑆) ∈ Fin) |
6 | 1, 3, 5 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd 𝑆) ∈ Fin) |
7 | | hashcl 13009 |
. . . . 5
⊢ ((𝐺 DProd 𝑆) ∈ Fin → (#‘(𝐺 DProd 𝑆)) ∈
ℕ0) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → (#‘(𝐺 DProd 𝑆)) ∈
ℕ0) |
9 | | hashcl 13009 |
. . . . 5
⊢ (𝐵 ∈ Fin →
(#‘𝐵) ∈
ℕ0) |
10 | 1, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (#‘𝐵) ∈
ℕ0) |
11 | | ablfac1.o |
. . . . . . 7
⊢ 𝑂 = (od‘𝐺) |
12 | | ablfac1.s |
. . . . . . 7
⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) |
13 | | ablfac1.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Abel) |
14 | | ablfac1.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ℙ) |
15 | 2, 11, 12, 13, 1, 14 | ablfac1b 18292 |
. . . . . 6
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
16 | | dprdsubg 18246 |
. . . . . 6
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) |
18 | 2 | lagsubg 17479 |
. . . . 5
⊢ (((𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (#‘(𝐺 DProd 𝑆)) ∥ (#‘𝐵)) |
19 | 17, 1, 18 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (#‘(𝐺 DProd 𝑆)) ∥ (#‘𝐵)) |
20 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑞 → (𝑤 ∥ (#‘𝐵) ↔ 𝑞 ∥ (#‘𝐵))) |
21 | | ablfac1c.d |
. . . . . . . . . . 11
⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} |
22 | 20, 21 | elrab2 3333 |
. . . . . . . . . 10
⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (#‘𝐵))) |
23 | | ablfac1.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
24 | 23 | sseld 3567 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑞 ∈ 𝐷 → 𝑞 ∈ 𝐴)) |
25 | 22, 24 | syl5bir 232 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑞 ∈ ℙ ∧ 𝑞 ∥ (#‘𝐵)) → 𝑞 ∈ 𝐴)) |
26 | 25 | impl 648 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑞 ∥ (#‘𝐵)) → 𝑞 ∈ 𝐴) |
27 | 2, 11, 12, 13, 1, 14 | ablfac1a 18291 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
28 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝐺)
∈ V |
29 | 2, 28 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 ∈ V |
30 | 29 | rabex 4740 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ V |
31 | 30, 12 | dmmpti 5936 |
. . . . . . . . . . . . . . . . 17
⊢ dom 𝑆 = 𝐴 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝑆 = 𝐴) |
33 | 15, 32 | dprdf2 18229 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
34 | 33 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
35 | 15 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑆) |
36 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑆 = 𝐴) |
37 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴) |
38 | 35, 36, 37 | dprdub 18247 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ (𝐺 DProd 𝑆)) |
39 | 17 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) |
40 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ↾s (𝐺 DProd 𝑆)) = (𝐺 ↾s (𝐺 DProd 𝑆)) |
41 | 40 | subsubg 17440 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺) → ((𝑆‘𝑞) ∈ (SubGrp‘(𝐺 ↾s (𝐺 DProd 𝑆))) ↔ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑞) ⊆ (𝐺 DProd 𝑆)))) |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑆‘𝑞) ∈ (SubGrp‘(𝐺 ↾s (𝐺 DProd 𝑆))) ↔ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑞) ⊆ (𝐺 DProd 𝑆)))) |
43 | 34, 38, 42 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘(𝐺 ↾s (𝐺 DProd 𝑆)))) |
44 | 40 | subgbas 17421 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺) → (𝐺 DProd 𝑆) = (Base‘(𝐺 ↾s (𝐺 DProd 𝑆)))) |
45 | 39, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd 𝑆) = (Base‘(𝐺 ↾s (𝐺 DProd 𝑆)))) |
46 | 6 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd 𝑆) ∈ Fin) |
47 | 45, 46 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (Base‘(𝐺 ↾s (𝐺 DProd 𝑆))) ∈ Fin) |
48 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Base‘(𝐺
↾s (𝐺
DProd 𝑆))) =
(Base‘(𝐺
↾s (𝐺
DProd 𝑆))) |
49 | 48 | lagsubg 17479 |
. . . . . . . . . . . . 13
⊢ (((𝑆‘𝑞) ∈ (SubGrp‘(𝐺 ↾s (𝐺 DProd 𝑆))) ∧ (Base‘(𝐺 ↾s (𝐺 DProd 𝑆))) ∈ Fin) → (#‘(𝑆‘𝑞)) ∥ (#‘(Base‘(𝐺 ↾s (𝐺 DProd 𝑆))))) |
50 | 43, 47, 49 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑆‘𝑞)) ∥ (#‘(Base‘(𝐺 ↾s (𝐺 DProd 𝑆))))) |
51 | 45 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝐺 DProd 𝑆)) = (#‘(Base‘(𝐺 ↾s (𝐺 DProd 𝑆))))) |
52 | 50, 51 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑆‘𝑞)) ∥ (#‘(𝐺 DProd 𝑆))) |
53 | 27, 52 | eqbrtrrd 4607 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘(𝐺 DProd 𝑆))) |
54 | 14 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ) |
55 | 8 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘(𝐺 DProd 𝑆)) ∈ ℤ) |
56 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝐺 DProd 𝑆)) ∈ ℤ) |
57 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → 𝑞 ∈ ℙ) |
58 | | ablgrp 18021 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
59 | 2 | grpbn0 17274 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
60 | 13, 58, 59 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ ∅) |
61 | | hashnncl 13018 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin →
((#‘𝐵) ∈ ℕ
↔ 𝐵 ≠
∅)) |
62 | 1, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((#‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
63 | 60, 62 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘𝐵) ∈ ℕ) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (#‘𝐵) ∈
ℕ) |
65 | 57, 64 | pccld 15393 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (#‘𝐵)) ∈
ℕ0) |
66 | 54, 65 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ∈
ℕ0) |
67 | | pcdvdsb 15411 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ ℙ ∧
(#‘(𝐺 DProd 𝑆)) ∈ ℤ ∧ (𝑞 pCnt (#‘𝐵)) ∈ ℕ0) →
((𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆))) ↔ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘(𝐺 DProd 𝑆)))) |
68 | 54, 56, 66, 67 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆))) ↔ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘(𝐺 DProd 𝑆)))) |
69 | 53, 68 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
70 | 69 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
71 | 26, 70 | syldan 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ 𝑞 ∥ (#‘𝐵)) → (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
72 | | pceq0 15413 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧
(#‘𝐵) ∈ ℕ)
→ ((𝑞 pCnt
(#‘𝐵)) = 0 ↔
¬ 𝑞 ∥
(#‘𝐵))) |
73 | 57, 64, 72 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt (#‘𝐵)) = 0 ↔ ¬ 𝑞 ∥ (#‘𝐵))) |
74 | 73 | biimpar 501 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 ∥ (#‘𝐵)) → (𝑞 pCnt (#‘𝐵)) = 0) |
75 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
76 | 75 | subg0cl 17425 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd 𝑆)) |
77 | | ne0i 3880 |
. . . . . . . . . . . . . 14
⊢
((0g‘𝐺) ∈ (𝐺 DProd 𝑆) → (𝐺 DProd 𝑆) ≠ ∅) |
78 | 17, 76, 77 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 DProd 𝑆) ≠ ∅) |
79 | | hashnncl 13018 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 DProd 𝑆) ∈ Fin → ((#‘(𝐺 DProd 𝑆)) ∈ ℕ ↔ (𝐺 DProd 𝑆) ≠ ∅)) |
80 | 6, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((#‘(𝐺 DProd 𝑆)) ∈ ℕ ↔ (𝐺 DProd 𝑆) ≠ ∅)) |
81 | 78, 80 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘(𝐺 DProd 𝑆)) ∈ ℕ) |
82 | 81 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (#‘(𝐺 DProd 𝑆)) ∈ ℕ) |
83 | 57, 82 | pccld 15393 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (#‘(𝐺 DProd 𝑆))) ∈
ℕ0) |
84 | 83 | nn0ge0d 11231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → 0 ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
85 | 84 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 ∥ (#‘𝐵)) → 0 ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
86 | 74, 85 | eqbrtrd 4605 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ ℙ) ∧ ¬ 𝑞 ∥ (#‘𝐵)) → (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
87 | 71, 86 | pm2.61dan 828 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
88 | 87 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑞 ∈ ℙ (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆)))) |
89 | 10 | nn0zd 11356 |
. . . . . 6
⊢ (𝜑 → (#‘𝐵) ∈ ℤ) |
90 | | pc2dvds 15421 |
. . . . . 6
⊢
(((#‘𝐵) ∈
ℤ ∧ (#‘(𝐺
DProd 𝑆)) ∈ ℤ)
→ ((#‘𝐵) ∥
(#‘(𝐺 DProd 𝑆)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆))))) |
91 | 89, 55, 90 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((#‘𝐵) ∥ (#‘(𝐺 DProd 𝑆)) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt (#‘𝐵)) ≤ (𝑞 pCnt (#‘(𝐺 DProd 𝑆))))) |
92 | 88, 91 | mpbird 246 |
. . . 4
⊢ (𝜑 → (#‘𝐵) ∥ (#‘(𝐺 DProd 𝑆))) |
93 | | dvdseq 14874 |
. . . 4
⊢
((((#‘(𝐺 DProd
𝑆)) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) ∧
((#‘(𝐺 DProd 𝑆)) ∥ (#‘𝐵) ∧ (#‘𝐵) ∥ (#‘(𝐺 DProd 𝑆)))) → (#‘(𝐺 DProd 𝑆)) = (#‘𝐵)) |
94 | 8, 10, 19, 92, 93 | syl22anc 1319 |
. . 3
⊢ (𝜑 → (#‘(𝐺 DProd 𝑆)) = (#‘𝐵)) |
95 | | hashen 12997 |
. . . 4
⊢ (((𝐺 DProd 𝑆) ∈ Fin ∧ 𝐵 ∈ Fin) → ((#‘(𝐺 DProd 𝑆)) = (#‘𝐵) ↔ (𝐺 DProd 𝑆) ≈ 𝐵)) |
96 | 6, 1, 95 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((#‘(𝐺 DProd 𝑆)) = (#‘𝐵) ↔ (𝐺 DProd 𝑆) ≈ 𝐵)) |
97 | 94, 96 | mpbid 221 |
. 2
⊢ (𝜑 → (𝐺 DProd 𝑆) ≈ 𝐵) |
98 | | fisseneq 8056 |
. 2
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd 𝑆) ⊆ 𝐵 ∧ (𝐺 DProd 𝑆) ≈ 𝐵) → (𝐺 DProd 𝑆) = 𝐵) |
99 | 1, 4, 97, 98 | syl3anc 1318 |
1
⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵) |