Step | Hyp | Ref
| Expression |
1 | | ablfac1eu.1 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) |
2 | 1 | simpld 482 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
3 | | ablfac1eu.2 |
. . . 4
⊢ (𝜑 → dom 𝑇 = 𝐴) |
4 | 2, 3 | dprdf2 18614 |
. . 3
⊢ (𝜑 → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
5 | 4 | ffnd 6185 |
. 2
⊢ (𝜑 → 𝑇 Fn 𝐴) |
6 | | ablfac1.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
7 | | ablfac1.o |
. . . . 5
⊢ 𝑂 = (od‘𝐺) |
8 | | ablfac1.s |
. . . . 5
⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) |
9 | | ablfac1.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ Abel) |
10 | | ablfac1.f |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ Fin) |
11 | | ablfac1.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℙ) |
12 | 6, 7, 8, 9, 10, 11 | ablfac1b 18677 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
13 | 6 | fvexi 6345 |
. . . . . . 7
⊢ 𝐵 ∈ V |
14 | 13 | rabex 4947 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V |
15 | 14, 8 | dmmpti 6162 |
. . . . 5
⊢ dom 𝑆 = 𝐴 |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → dom 𝑆 = 𝐴) |
17 | 12, 16 | dprdf2 18614 |
. . 3
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
18 | 17 | ffnd 6185 |
. 2
⊢ (𝜑 → 𝑆 Fn 𝐴) |
19 | 10 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin) |
20 | 17 | ffvelrnda 6504 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
21 | 6 | subgss 17803 |
. . . . 5
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵) |
23 | 19, 22 | ssfid 8343 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin) |
24 | 4 | ffvelrnda 6504 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
25 | 6 | subgss 17803 |
. . . . . 6
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (𝑇‘𝑞) ⊆ 𝐵) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ 𝐵) |
27 | 24 | adantr 466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
28 | 19, 26 | ssfid 8343 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ Fin) |
29 | 28 | adantr 466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ Fin) |
30 | | simpr 471 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ (𝑇‘𝑞)) |
31 | 7 | odsubdvds 18193 |
. . . . . . 7
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇‘𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) |
32 | 27, 29, 30, 31 | syl3anc 1476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) |
33 | | ablfac1eu.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
34 | 11 | sselda 3752 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ) |
35 | | prmz 15596 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℤ) |
37 | | ablfac1eu.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈
ℕ0) |
38 | 37 | nn0zd 11687 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℤ) |
39 | | ablgrp 18405 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
40 | 9, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Grp) |
41 | 6 | grpbn0 17659 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ≠ ∅) |
43 | | hashnncl 13359 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ Fin →
((♯‘𝐵) ∈
ℕ ↔ 𝐵 ≠
∅)) |
44 | 10, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
45 | 42, 44 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ) |
46 | 45 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ) |
47 | 34, 46 | pccld 15762 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
ℕ0) |
48 | 47 | nn0zd 11687 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) |
49 | 6 | lagsubg 17864 |
. . . . . . . . . . . . 13
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) |
50 | 24, 19, 49 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) |
51 | 33, 50 | eqbrtrrd 4811 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (♯‘𝐵)) |
52 | 46 | nnzd 11688 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℤ) |
53 | | pcdvdsb 15780 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℤ ∧ 𝐶 ∈
ℕ0) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) |
54 | 34, 52, 37, 53 | syl3anc 1476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) |
55 | 51, 54 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ≤ (𝑞 pCnt (♯‘𝐵))) |
56 | | eluz2 11899 |
. . . . . . . . . 10
⊢ ((𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (♯‘𝐵)))) |
57 | 38, 48, 55, 56 | syl3anbrc 1428 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶)) |
58 | | dvdsexp 15258 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0
∧ (𝑞 pCnt
(♯‘𝐵)) ∈
(ℤ≥‘𝐶)) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
59 | 36, 37, 57, 58 | syl3anc 1476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
60 | 33, 59 | eqbrtrd 4809 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
61 | 60 | adantr 466 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
62 | 26 | sselda 3752 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ 𝐵) |
63 | 6, 7 | odcl 18162 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈
ℕ0) |
64 | 62, 63 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈
ℕ0) |
65 | 64 | nn0zd 11687 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℤ) |
66 | | hashcl 13349 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑞) ∈ Fin → (♯‘(𝑇‘𝑞)) ∈
ℕ0) |
67 | 28, 66 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈
ℕ0) |
68 | 67 | nn0zd 11687 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℤ) |
69 | 68 | adantr 466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∈ ℤ) |
70 | | prmnn 15595 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
71 | 34, 70 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℕ) |
72 | 71, 47 | nnexpcld 13237 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ) |
73 | 72 | nnzd 11688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) |
74 | 73 | adantr 466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) |
75 | | dvdstr 15227 |
. . . . . . 7
⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (♯‘(𝑇‘𝑞)) ∈ ℤ ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)) ∧ (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) |
76 | 65, 69, 74, 75 | syl3anc 1476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (((𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)) ∧ (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) |
77 | 32, 61, 76 | mp2and 679 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
78 | 26, 77 | ssrabdv 3830 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
79 | | id 22 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → 𝑝 = 𝑞) |
80 | | oveq1 6803 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → (𝑝 pCnt (♯‘𝐵)) = (𝑞 pCnt (♯‘𝐵))) |
81 | 79, 80 | oveq12d 6814 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
82 | 81 | breq2d 4799 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) |
83 | 82 | rabbidv 3339 |
. . . . . 6
⊢ (𝑝 = 𝑞 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
84 | 83, 8, 14 | fvmpt3i 6431 |
. . . . 5
⊢ (𝑞 ∈ 𝐴 → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
85 | 84 | adantl 467 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
86 | 78, 85 | sseqtr4d 3791 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ (𝑆‘𝑞)) |
87 | 72 | nnnn0d 11558 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈
ℕ0) |
88 | | pcdvds 15775 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℕ) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
89 | 34, 46, 88 | syl2anc 573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
90 | 2 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑇) |
91 | 3 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑇 = 𝐴) |
92 | | ablfac1.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
93 | 92 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 ⊆ 𝐴) |
94 | 90, 91, 93 | dprdres 18635 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
95 | 94 | simpld 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
96 | 4 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
97 | 96, 93 | fssresd 6212 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
98 | 97 | fdmd 6193 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom (𝑇 ↾ 𝐷) = 𝐷) |
99 | | difssd 3889 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷) |
100 | 95, 98, 99 | dprdres 18635 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
101 | 100 | simpld 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
102 | | dprdsubg 18631 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
104 | 6 | lagsubg 17864 |
. . . . . . . . . 10
⊢ (((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) |
105 | 103, 19, 104 | syl2anc 573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) |
106 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
107 | 106 | subg0cl 17810 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
108 | 103, 107 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
109 | 108 | ne0d 4070 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅) |
110 | 6 | dprdssv 18623 |
. . . . . . . . . . . . . 14
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵 |
111 | | ssfi 8340 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
112 | 19, 110, 111 | sylancl 574 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
113 | | hashnncl 13359 |
. . . . . . . . . . . . 13
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
115 | 109, 114 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ) |
116 | 115 | nnzd 11688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) |
117 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → 𝑥 = 𝑞) |
118 | | sneq 4327 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑞 → {𝑥} = {𝑞}) |
119 | 118 | difeq2d 3879 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞})) |
120 | 119 | reseq2d 5533 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
121 | 120 | oveq2d 6812 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
122 | 121 | fveq2d 6337 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) = (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
123 | 117, 122 | breq12d 4800 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
124 | 123 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → (¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
125 | | eqid 2771 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) |
126 | 9 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐺 ∈ Abel) |
127 | 10 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐵 ∈ Fin) |
128 | | ablfac1c.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} |
129 | | ssrab2 3836 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆
ℙ |
130 | 128, 129 | eqsstri 3784 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆
ℙ |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ) |
132 | | ssid 3773 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆ 𝐷 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ 𝐷) |
134 | 2, 3, 92 | dprdres 18635 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
135 | 134 | simpld 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
136 | | dprdsubg 18631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ 𝐷) → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
138 | | difssd 3889 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ 𝐴) |
139 | 2, 3, 138 | dprdres 18635 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd 𝑇))) |
140 | 139 | simpld 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) |
141 | | dprdsubg 18631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
143 | | difss 3888 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∖ 𝐷) ⊆ 𝐴 |
144 | | fssres 6211 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴 ∖ 𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
145 | 4, 143, 144 | sylancl 574 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
146 | 145 | fdmd 6193 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷)) |
147 | | fvres 6350 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
148 | 147 | adantl 467 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
149 | | eldif 3733 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) ↔ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) |
150 | 28 | adantrr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ∈ Fin) |
151 | 106 | subg0cl 17810 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
152 | 24, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
153 | 152 | snssd 4476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
154 | 153 | adantrr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
155 | 33 | adantrr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
156 | 34 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ) |
157 | | iddvdsexp 15214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
158 | 36, 157 | sylan 569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
159 | 51 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞↑𝐶) ∥ (♯‘𝐵)) |
160 | 33, 68 | eqeltrrd 2851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∈ ℤ) |
161 | | dvdstr 15227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑞 ∈ ℤ ∧ (𝑞↑𝐶) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
162 | 36, 160, 52, 161 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
163 | 162 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
164 | 158, 159,
163 | mp2and 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (♯‘𝐵)) |
165 | | breq1 4790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤 = 𝑞 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑞 ∥ (♯‘𝐵))) |
166 | 165, 128 | elrab2 3518 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (♯‘𝐵))) |
167 | 156, 164,
166 | sylanbrc 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ 𝐷) |
168 | 167 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ∈ ℕ → 𝑞 ∈ 𝐷)) |
169 | 168 | con3d 149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ)) |
170 | 169 | impr 442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝐶 ∈ ℕ) |
171 | 37 | adantrr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 ∈
ℕ0) |
172 | | elnn0 11501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐶 ∈ ℕ0
↔ (𝐶 ∈ ℕ
∨ 𝐶 =
0)) |
173 | 171, 172 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0)) |
174 | 173 | ord 853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0)) |
175 | 170, 174 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 = 0) |
176 | 175 | oveq2d 6812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑𝐶) = (𝑞↑0)) |
177 | 71 | adantrr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℕ) |
178 | 177 | nncnd 11242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℂ) |
179 | 178 | exp0d 13209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑0) = 1) |
180 | 155, 176,
179 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = 1) |
181 | | fvex 6344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(0g‘𝐺) ∈ V |
182 | | hashsng 13361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0g‘𝐺) ∈ V →
(♯‘{(0g‘𝐺)}) = 1) |
183 | 181, 182 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(♯‘{(0g‘𝐺)}) = 1 |
184 | 180, 183 | syl6reqr 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
(♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞))) |
185 | | snfi 8198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
{(0g‘𝐺)} ∈ Fin |
186 | | hashen 13339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(({(0g‘𝐺)} ∈ Fin ∧ (𝑇‘𝑞) ∈ Fin) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
187 | 185, 150,
186 | sylancr 575 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
188 | 184, 187 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ≈ (𝑇‘𝑞)) |
189 | | fisseneq 8331 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑇‘𝑞) ∈ Fin ∧
{(0g‘𝐺)}
⊆ (𝑇‘𝑞) ∧
{(0g‘𝐺)}
≈ (𝑇‘𝑞)) →
{(0g‘𝐺)} =
(𝑇‘𝑞)) |
190 | 150, 154,
188, 189 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} = (𝑇‘𝑞)) |
191 | 106 | subg0cl 17810 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
192 | 137, 191 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
193 | 192 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
194 | 193 | snssd 4476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
195 | 190, 194 | eqsstr3d 3789 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
196 | 149, 195 | sylan2b 581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
197 | 148, 196 | eqsstrd 3788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
198 | 140, 146,
137, 197 | dprdlub 18633 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
199 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
200 | 199 | lsmss2 18288 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
201 | 137, 142,
198, 200 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
202 | | disjdif 4183 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅ |
203 | 202 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅) |
204 | | undif2 4187 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∪ (𝐴 ∖ 𝐷)) = (𝐷 ∪ 𝐴) |
205 | | ssequn1 3934 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∪ 𝐴) = 𝐴) |
206 | 92, 205 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐷 ∪ 𝐴) = 𝐴) |
207 | 204, 206 | syl5req 2818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 = (𝐷 ∪ (𝐴 ∖ 𝐷))) |
208 | 4, 203, 207, 199, 2 | dprdsplit 18655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))))) |
209 | 1 | simprd 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝐵) |
210 | 208, 209 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = 𝐵) |
211 | 201, 210 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
212 | 135, 211 | jca 501 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
213 | 212 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
214 | 4, 92 | fssresd 6212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
215 | 214 | fdmd 6193 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑇 ↾ 𝐷) = 𝐷) |
216 | 215 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → dom (𝑇 ↾ 𝐷) = 𝐷) |
217 | 92 | sselda 3752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐴) |
218 | 217, 37 | syldan 579 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
219 | 218 | adantlr 694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
220 | | fvres 6350 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ 𝐷 → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
221 | 220 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
222 | 221 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (♯‘(𝑇‘𝑞))) |
223 | 217, 33 | syldan 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
224 | 222, 223 | eqtrd 2805 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
225 | 224 | adantlr 694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
226 | | simpr 471 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝑥 ∈ ℙ) |
227 | | fzfid 12980 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...(♯‘𝐵)) ∈ Fin) |
228 | | prmnn 15595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℕ) |
229 | 228 | 3ad2ant2 1128 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ) |
230 | | prmz 15596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℤ) |
231 | | dvdsle 15241 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ ℤ ∧
(♯‘𝐵) ∈
ℕ) → (𝑤 ∥
(♯‘𝐵) →
𝑤 ≤ (♯‘𝐵))) |
232 | 230, 45, 231 | syl2anr 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵))) |
233 | 232 | 3impia 1109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵)) |
234 | 45 | nnzd 11688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) |
235 | 234 | 3ad2ant1 1127 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) |
236 | | fznn 12615 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝐵)
∈ ℤ → (𝑤
∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) |
238 | 229, 233,
237 | mpbir2and 692 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵))) |
239 | 238 | rabssdv 3831 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))) |
240 | 128, 239 | syl5eqss 3798 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 ⊆ (1...(♯‘𝐵))) |
241 | 227, 240 | ssfid 8343 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ Fin) |
242 | 241 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ∈ Fin) |
243 | 6, 7, 125, 126, 127, 131, 128, 133, 213, 216, 219, 225, 226, 242 | ablfac1eulem 18679 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
244 | 243 | ralrimiva 3115 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
245 | 244 | adantr 466 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
246 | 124, 245,
34 | rspcdva 3466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
247 | | coprm 15630 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
248 | 34, 116, 247 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
249 | 246, 248 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
250 | | rpexp1i 15640 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
→ ((𝑞 gcd
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
251 | 36, 116, 47, 250 | syl3anc 1476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
252 | 249, 251 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
253 | | coprmdvds2 15575 |
. . . . . . . . . 10
⊢ ((((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘𝐵) ∈
ℤ) ∧ ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) |
254 | 73, 116, 52, 252, 253 | syl31anc 1479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) |
255 | 89, 105, 254 | mp2and 679 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)) |
256 | | eqid 2771 |
. . . . . . . . . 10
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
257 | | inss1 3981 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∩ {𝑞}) ⊆ 𝐷 |
258 | 257 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷) |
259 | 95, 98, 258 | dprdres 18635 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
260 | 259 | simpld 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) |
261 | | dprdsubg 18631 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
262 | 260, 261 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
263 | | inass 3972 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) |
264 | | disjdif 4183 |
. . . . . . . . . . . . . 14
⊢ ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅ |
265 | 264 | ineq2i 3962 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅) |
266 | | in0 4113 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ∅) =
∅ |
267 | 263, 265,
266 | 3eqtri 2797 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅ |
268 | 267 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅) |
269 | 95, 98, 258, 99, 268, 106 | dprddisj2 18646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0g‘𝐺)}) |
270 | 95, 98, 258, 99, 268, 256 | dprdcntz2 18645 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
271 | 6 | dprdssv 18623 |
. . . . . . . . . . 11
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵 |
272 | | ssfi 8340 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
273 | 19, 271, 272 | sylancl 574 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
274 | 199, 106,
256, 262, 103, 269, 270, 273, 112 | lsmhash 18325 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
275 | | inundif 4189 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷 |
276 | 275 | eqcomi 2780 |
. . . . . . . . . . . . 13
⊢ 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) |
277 | 276 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))) |
278 | 97, 268, 277, 199, 95 | dprdsplit 18655 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
279 | 211 | adantr 466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
280 | 278, 279 | eqtr3d 2807 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵) |
281 | 280 | fveq2d 6337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (♯‘𝐵)) |
282 | | snssi 4475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ 𝐷 → {𝑞} ⊆ 𝐷) |
283 | 282 | adantl 467 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → {𝑞} ⊆ 𝐷) |
284 | | sseqin2 3968 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞}) |
285 | 283, 284 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐷 ∩ {𝑞}) = {𝑞}) |
286 | 285 | reseq2d 5533 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ {𝑞})) |
287 | 286 | oveq2d 6812 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞}))) |
288 | 95 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
289 | 215 | ad2antrr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → dom (𝑇 ↾ 𝐷) = 𝐷) |
290 | | simpr 471 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐷) |
291 | 288, 289,
290 | dpjlem 18658 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})) = ((𝑇 ↾ 𝐷)‘𝑞)) |
292 | 220 | adantl 467 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
293 | 287, 291,
292 | 3eqtrd 2809 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
294 | | simprr 756 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝑞 ∈ 𝐷) |
295 | | disjsn 4384 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞 ∈ 𝐷) |
296 | 294, 295 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐷 ∩ {𝑞}) = ∅) |
297 | 296 | reseq2d 5533 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ ∅)) |
298 | | res0 5537 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ↾ 𝐷) ↾ ∅) =
∅ |
299 | 297, 298 | syl6eq 2821 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅) |
300 | 299 | oveq2d 6812 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅)) |
301 | 106 | dprd0 18638 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
302 | 40, 301 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
303 | 302 | simprd 483 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
304 | 303 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
305 | 300, 304,
190 | 3eqtrd 2809 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
306 | 305 | anassrs 453 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ ¬ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
307 | 293, 306 | pm2.61dan 814 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
308 | 307 | fveq2d 6337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) = (♯‘(𝑇‘𝑞))) |
309 | 308 | oveq1d 6811 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
310 | 274, 281,
309 | 3eqtr3d 2813 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
311 | 255, 310 | breqtrd 4813 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
312 | 115 | nnne0d 11271 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0) |
313 | | dvdsmulcr 15220 |
. . . . . . . 8
⊢ (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝑇‘𝑞)) ∈ ℤ ∧
((♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) |
314 | 73, 68, 116, 312, 313 | syl112anc 1480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) |
315 | 311, 314 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))) |
316 | | dvdseq 15245 |
. . . . . 6
⊢
((((♯‘(𝑇‘𝑞)) ∈ ℕ0 ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0) ∧
((♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
317 | 67, 87, 60, 315, 316 | syl22anc 1477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
318 | 6, 7, 8, 9, 10, 11 | ablfac1a 18676 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
319 | 317, 318 | eqtr4d 2808 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞))) |
320 | | hashen 13339 |
. . . . 5
⊢ (((𝑇‘𝑞) ∈ Fin ∧ (𝑆‘𝑞) ∈ Fin) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
321 | 28, 23, 320 | syl2anc 573 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
322 | 319, 321 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ≈ (𝑆‘𝑞)) |
323 | | fisseneq 8331 |
. . 3
⊢ (((𝑆‘𝑞) ∈ Fin ∧ (𝑇‘𝑞) ⊆ (𝑆‘𝑞) ∧ (𝑇‘𝑞) ≈ (𝑆‘𝑞)) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
324 | 23, 86, 322, 323 | syl3anc 1476 |
. 2
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
325 | 5, 18, 324 | eqfnfvd 6459 |
1
⊢ (𝜑 → 𝑇 = 𝑆) |