Step | Hyp | Ref
| Expression |
1 | | ablfac1eu.1 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) |
2 | 1 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
3 | | ablfac1eu.2 |
. . . 4
⊢ (𝜑 → dom 𝑇 = 𝐴) |
4 | 2, 3 | dprdf2 18406 |
. . 3
⊢ (𝜑 → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
5 | 4 | ffnd 6046 |
. 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 18469 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
13 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐺)
∈ V |
14 | 6, 13 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐵 ∈ V |
15 | 14 | rabex 4813 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ V |
16 | 15, 8 | dmmpti 6023 |
. . . . 5
⊢ dom 𝑆 = 𝐴 |
17 | 16 | a1i 11 |
. . . 4
⊢ (𝜑 → dom 𝑆 = 𝐴) |
18 | 12, 17 | dprdf2 18406 |
. . 3
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
19 | 18 | ffnd 6046 |
. 2
⊢ (𝜑 → 𝑆 Fn 𝐴) |
20 | 10 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin) |
21 | 18 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
22 | 6 | subgss 17595 |
. . . . 5
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵) |
24 | 20, 23 | ssfid 8183 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin) |
25 | 4 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
26 | 6 | subgss 17595 |
. . . . . 6
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (𝑇‘𝑞) ⊆ 𝐵) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ 𝐵) |
28 | 25 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
29 | 20, 27 | ssfid 8183 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ Fin) |
30 | 29 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ Fin) |
31 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ (𝑇‘𝑞)) |
32 | 7 | odsubdvds 17986 |
. . . . . . 7
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇‘𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (#‘(𝑇‘𝑞))) |
33 | 28, 30, 31, 32 | syl3anc 1326 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (#‘(𝑇‘𝑞))) |
34 | | ablfac1eu.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
35 | 11 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ) |
36 | | prmz 15389 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℤ) |
38 | | ablfac1eu.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈
ℕ0) |
39 | 38 | nn0zd 11480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℤ) |
40 | | ablgrp 18198 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
41 | 9, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Grp) |
42 | 6 | grpbn0 17451 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ≠ ∅) |
44 | | hashnncl 13157 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ Fin →
((#‘𝐵) ∈ ℕ
↔ 𝐵 ≠
∅)) |
45 | 10, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((#‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
46 | 43, 45 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘𝐵) ∈ ℕ) |
47 | 46 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘𝐵) ∈ ℕ) |
48 | 35, 47 | pccld 15555 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ∈
ℕ0) |
49 | 48 | nn0zd 11480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ∈ ℤ) |
50 | 6 | lagsubg 17656 |
. . . . . . . . . . . . 13
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (#‘(𝑇‘𝑞)) ∥ (#‘𝐵)) |
51 | 25, 20, 50 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑇‘𝑞)) ∥ (#‘𝐵)) |
52 | 34, 51 | eqbrtrrd 4677 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (#‘𝐵)) |
53 | 47 | nnzd 11481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘𝐵) ∈ ℤ) |
54 | | pcdvdsb 15573 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℙ ∧
(#‘𝐵) ∈ ℤ
∧ 𝐶 ∈
ℕ0) → (𝐶 ≤ (𝑞 pCnt (#‘𝐵)) ↔ (𝑞↑𝐶) ∥ (#‘𝐵))) |
55 | 35, 53, 38, 54 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ≤ (𝑞 pCnt (#‘𝐵)) ↔ (𝑞↑𝐶) ∥ (#‘𝐵))) |
56 | 52, 55 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ≤ (𝑞 pCnt (#‘𝐵))) |
57 | | eluz2 11693 |
. . . . . . . . . 10
⊢ ((𝑞 pCnt (#‘𝐵)) ∈
(ℤ≥‘𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (#‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (#‘𝐵)))) |
58 | 39, 49, 56, 57 | syl3anbrc 1246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (#‘𝐵)) ∈
(ℤ≥‘𝐶)) |
59 | | dvdsexp 15049 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0
∧ (𝑞 pCnt
(#‘𝐵)) ∈
(ℤ≥‘𝐶)) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
60 | 37, 38, 58, 59 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
61 | 34, 60 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
62 | 61 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (#‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
63 | 27 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ 𝐵) |
64 | 6, 7 | odcl 17955 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈
ℕ0) |
65 | 63, 64 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈
ℕ0) |
66 | 65 | nn0zd 11480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℤ) |
67 | | hashcl 13147 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑞) ∈ Fin → (#‘(𝑇‘𝑞)) ∈
ℕ0) |
68 | 29, 67 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑇‘𝑞)) ∈
ℕ0) |
69 | 68 | nn0zd 11480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑇‘𝑞)) ∈ ℤ) |
70 | 69 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (#‘(𝑇‘𝑞)) ∈ ℤ) |
71 | | prmnn 15388 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
72 | 35, 71 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℕ) |
73 | 72, 48 | nnexpcld 13030 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (#‘𝐵))) ∈ ℕ) |
74 | 73 | nnzd 11481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (#‘𝐵))) ∈ ℤ) |
75 | 74 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑞↑(𝑞 pCnt (#‘𝐵))) ∈ ℤ) |
76 | | dvdstr 15018 |
. . . . . . 7
⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (#‘(𝑇‘𝑞)) ∈ ℤ ∧ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (#‘(𝑇‘𝑞)) ∧ (#‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵))))) |
77 | 66, 70, 75, 76 | syl3anc 1326 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (((𝑂‘𝑥) ∥ (#‘(𝑇‘𝑞)) ∧ (#‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵))))) |
78 | 33, 62, 77 | mp2and 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
79 | 27, 78 | ssrabdv 3681 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))}) |
80 | | id 22 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → 𝑝 = 𝑞) |
81 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → (𝑝 pCnt (#‘𝐵)) = (𝑞 pCnt (#‘𝐵))) |
82 | 80, 81 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (#‘𝐵))) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
83 | 82 | breq2d 4665 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵))))) |
84 | 83 | rabbidv 3189 |
. . . . . 6
⊢ (𝑝 = 𝑞 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))}) |
85 | 84, 8, 15 | fvmpt3i 6287 |
. . . . 5
⊢ (𝑞 ∈ 𝐴 → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))}) |
86 | 85 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵)))}) |
87 | 79, 86 | sseqtr4d 3642 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ (𝑆‘𝑞)) |
88 | 73 | nnnn0d 11351 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (#‘𝐵))) ∈
ℕ0) |
89 | | pcdvds 15568 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧
(#‘𝐵) ∈ ℕ)
→ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘𝐵)) |
90 | 35, 47, 89 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘𝐵)) |
91 | 2 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑇) |
92 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑇 = 𝐴) |
93 | | ablfac1.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
94 | 93 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 ⊆ 𝐴) |
95 | 91, 92, 94 | dprdres 18427 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
96 | 95 | simpld 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
97 | 4 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
98 | 97, 94 | fssresd 6071 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
99 | | fdm 6051 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺) → dom (𝑇 ↾ 𝐷) = 𝐷) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom (𝑇 ↾ 𝐷) = 𝐷) |
101 | | difssd 3738 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷) |
102 | 96, 100, 101 | dprdres 18427 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
103 | 102 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
104 | | dprdsubg 18423 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
106 | 6 | lagsubg 17656 |
. . . . . . . . . 10
⊢ (((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (#‘𝐵)) |
107 | 105, 20, 106 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (#‘𝐵)) |
108 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
109 | 108 | subg0cl 17602 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
110 | 105, 109 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
111 | | ne0i 3921 |
. . . . . . . . . . . . 13
⊢
((0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅) |
113 | 6 | dprdssv 18415 |
. . . . . . . . . . . . . 14
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵 |
114 | | ssfi 8180 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
115 | 20, 113, 114 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
116 | | hashnncl 13157 |
. . . . . . . . . . . . 13
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
118 | 112, 117 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ) |
119 | 118 | nnzd 11481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) |
120 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → 𝑥 = 𝑞) |
121 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑞 → {𝑥} = {𝑞}) |
122 | 121 | difeq2d 3728 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞})) |
123 | 122 | reseq2d 5396 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
124 | 123 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
125 | 124 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) = (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
126 | 120, 125 | breq12d 4666 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑥 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
127 | 126 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → (¬ 𝑥 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
128 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) = (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) |
129 | 9 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐺 ∈ Abel) |
130 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐵 ∈ Fin) |
131 | | ablfac1c.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} |
132 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} ⊆
ℙ |
133 | 131, 132 | eqsstri 3635 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆
ℙ |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ) |
135 | | ssid 3624 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆ 𝐷 |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ 𝐷) |
137 | 2, 3, 93 | dprdres 18427 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
138 | 137 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
139 | | dprdsubg 18423 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ 𝐷) → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
141 | | difssd 3738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ 𝐴) |
142 | 2, 3, 141 | dprdres 18427 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd 𝑇))) |
143 | 142 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) |
144 | | dprdsubg 18423 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
146 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∖ 𝐷) ⊆ 𝐴 |
147 | | fssres 6070 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴 ∖ 𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
148 | 4, 146, 147 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
149 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺) → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷)) |
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷)) |
151 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
152 | 151 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
153 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) ↔ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) |
154 | 29 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ∈ Fin) |
155 | 108 | subg0cl 17602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
156 | 25, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
157 | 156 | snssd 4340 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
158 | 157 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
159 | 34 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (#‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
160 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ) |
161 | | iddvdsexp 15005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
162 | 37, 161 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
163 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞↑𝐶) ∥ (#‘𝐵)) |
164 | 34, 69 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∈ ℤ) |
165 | | dvdstr 15018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑞 ∈ ℤ ∧ (𝑞↑𝐶) ∈ ℤ ∧ (#‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (#‘𝐵)) → 𝑞 ∥ (#‘𝐵))) |
166 | 37, 164, 53, 165 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (#‘𝐵)) → 𝑞 ∥ (#‘𝐵))) |
167 | 166 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (#‘𝐵)) → 𝑞 ∥ (#‘𝐵))) |
168 | 162, 163,
167 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (#‘𝐵)) |
169 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤 = 𝑞 → (𝑤 ∥ (#‘𝐵) ↔ 𝑞 ∥ (#‘𝐵))) |
170 | 169, 131 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (#‘𝐵))) |
171 | 160, 168,
170 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ 𝐷) |
172 | 171 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ∈ ℕ → 𝑞 ∈ 𝐷)) |
173 | 172 | con3d 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ)) |
174 | 173 | impr 649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝐶 ∈ ℕ) |
175 | 38 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 ∈
ℕ0) |
176 | | elnn0 11294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐶 ∈ ℕ0
↔ (𝐶 ∈ ℕ
∨ 𝐶 =
0)) |
177 | 175, 176 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0)) |
178 | 177 | ord 392 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0)) |
179 | 174, 178 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 = 0) |
180 | 179 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑𝐶) = (𝑞↑0)) |
181 | 72 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℕ) |
182 | 181 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℂ) |
183 | 182 | exp0d 13002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑0) = 1) |
184 | 159, 180,
183 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (#‘(𝑇‘𝑞)) = 1) |
185 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(0g‘𝐺) ∈ V |
186 | | hashsng 13159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0g‘𝐺) ∈ V →
(#‘{(0g‘𝐺)}) = 1) |
187 | 185, 186 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(#‘{(0g‘𝐺)}) = 1 |
188 | 184, 187 | syl6reqr 2675 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
(#‘{(0g‘𝐺)}) = (#‘(𝑇‘𝑞))) |
189 | | snfi 8038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
{(0g‘𝐺)} ∈ Fin |
190 | | hashen 13135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(({(0g‘𝐺)} ∈ Fin ∧ (𝑇‘𝑞) ∈ Fin) →
((#‘{(0g‘𝐺)}) = (#‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
191 | 189, 154,
190 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
((#‘{(0g‘𝐺)}) = (#‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
192 | 188, 191 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ≈ (𝑇‘𝑞)) |
193 | | fisseneq 8171 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑇‘𝑞) ∈ Fin ∧
{(0g‘𝐺)}
⊆ (𝑇‘𝑞) ∧
{(0g‘𝐺)}
≈ (𝑇‘𝑞)) →
{(0g‘𝐺)} =
(𝑇‘𝑞)) |
194 | 154, 158,
192, 193 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} = (𝑇‘𝑞)) |
195 | 108 | subg0cl 17602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
196 | 140, 195 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
197 | 196 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
198 | 197 | snssd 4340 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
199 | 194, 198 | eqsstr3d 3640 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
200 | 153, 199 | sylan2b 492 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
201 | 152, 200 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
202 | 143, 150,
140, 201 | dprdlub 18425 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
203 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
204 | 203 | lsmss2 18081 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
205 | 140, 145,
202, 204 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
206 | | disjdif 4040 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅ |
207 | 206 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅) |
208 | | undif2 4044 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∪ (𝐴 ∖ 𝐷)) = (𝐷 ∪ 𝐴) |
209 | | ssequn1 3783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∪ 𝐴) = 𝐴) |
210 | 93, 209 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐷 ∪ 𝐴) = 𝐴) |
211 | 208, 210 | syl5req 2669 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 = (𝐷 ∪ (𝐴 ∖ 𝐷))) |
212 | 4, 207, 211, 203, 2 | dprdsplit 18447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))))) |
213 | 1 | simprd 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝐵) |
214 | 212, 213 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = 𝐵) |
215 | 205, 214 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
216 | 138, 215 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
217 | 216 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
218 | 4, 93 | fssresd 6071 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
219 | 218, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑇 ↾ 𝐷) = 𝐷) |
220 | 219 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → dom (𝑇 ↾ 𝐷) = 𝐷) |
221 | 93 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐴) |
222 | 221, 38 | syldan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
223 | 222 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
224 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ 𝐷 → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
225 | 224 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
226 | 225 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (#‘((𝑇 ↾ 𝐷)‘𝑞)) = (#‘(𝑇‘𝑞))) |
227 | 221, 34 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (#‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
228 | 226, 227 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (#‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
229 | 228 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → (#‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
230 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝑥 ∈ ℙ) |
231 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...(#‘𝐵)) ∈ Fin) |
232 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℕ) |
233 | 232 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → 𝑤 ∈ ℕ) |
234 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℤ) |
235 | | dvdsle 15032 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ ℤ ∧
(#‘𝐵) ∈ ℕ)
→ (𝑤 ∥
(#‘𝐵) → 𝑤 ≤ (#‘𝐵))) |
236 | 234, 46, 235 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (#‘𝐵) → 𝑤 ≤ (#‘𝐵))) |
237 | 236 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → 𝑤 ≤ (#‘𝐵)) |
238 | 46 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (#‘𝐵) ∈ ℤ) |
239 | 238 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → (#‘𝐵) ∈ ℤ) |
240 | | fznn 12408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐵) ∈
ℤ → (𝑤 ∈
(1...(#‘𝐵)) ↔
(𝑤 ∈ ℕ ∧
𝑤 ≤ (#‘𝐵)))) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → (𝑤 ∈ (1...(#‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (#‘𝐵)))) |
242 | 233, 237,
241 | mpbir2and 957 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (#‘𝐵)) → 𝑤 ∈ (1...(#‘𝐵))) |
243 | 242 | rabssdv 3682 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} ⊆ (1...(#‘𝐵))) |
244 | 131, 243 | syl5eqss 3649 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 ⊆ (1...(#‘𝐵))) |
245 | 231, 244 | ssfid 8183 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ Fin) |
246 | 245 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ∈ Fin) |
247 | 6, 7, 128, 129, 130, 134, 131, 136, 217, 220, 223, 229, 230, 246 | ablfac1eulem 18471 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
248 | 247 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
249 | 248 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
250 | 127, 249,
35 | rspcdva 3316 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
251 | | coprm 15423 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧
(#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
252 | 35, 119, 251 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∥ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
253 | 250, 252 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
254 | | rpexp1i 15433 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℤ ∧
(#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (#‘𝐵)) ∈ ℕ0) →
((𝑞 gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (#‘𝐵))) gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
255 | 37, 119, 48, 254 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (#‘𝐵))) gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
256 | 253, 255 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (#‘𝐵))) gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
257 | | coprmdvds2 15368 |
. . . . . . . . . 10
⊢ ((((𝑞↑(𝑞 pCnt (#‘𝐵))) ∈ ℤ ∧ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (#‘𝐵) ∈ ℤ) ∧ ((𝑞↑(𝑞 pCnt (#‘𝐵))) gcd (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘𝐵) ∧ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (#‘𝐵)) → ((𝑞↑(𝑞 pCnt (#‘𝐵))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (#‘𝐵))) |
258 | 74, 119, 53, 256, 257 | syl31anc 1329 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘𝐵) ∧ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (#‘𝐵)) → ((𝑞↑(𝑞 pCnt (#‘𝐵))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (#‘𝐵))) |
259 | 90, 107, 258 | mp2and 715 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (#‘𝐵))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (#‘𝐵)) |
260 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
261 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∩ {𝑞}) ⊆ 𝐷 |
262 | 261 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷) |
263 | 96, 100, 262 | dprdres 18427 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
264 | 263 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) |
265 | | dprdsubg 18423 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
266 | 264, 265 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
267 | | inass 3823 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) |
268 | | disjdif 4040 |
. . . . . . . . . . . . . 14
⊢ ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅ |
269 | 268 | ineq2i 3811 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅) |
270 | | in0 3968 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ∅) =
∅ |
271 | 267, 269,
270 | 3eqtri 2648 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅ |
272 | 271 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅) |
273 | 96, 100, 262, 101, 272, 108 | dprddisj2 18438 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0g‘𝐺)}) |
274 | 96, 100, 262, 101, 272, 260 | dprdcntz2 18437 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
275 | 6 | dprdssv 18415 |
. . . . . . . . . . 11
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵 |
276 | | ssfi 8180 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
277 | 20, 275, 276 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
278 | 203, 108,
260, 266, 105, 273, 274, 277, 115 | lsmhash 18118 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
279 | | inundif 4046 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷 |
280 | 279 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢ 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) |
281 | 280 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))) |
282 | 98, 272, 281, 203, 96 | dprdsplit 18447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
283 | 215 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
284 | 282, 283 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵) |
285 | 284 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (#‘𝐵)) |
286 | | snssi 4339 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ 𝐷 → {𝑞} ⊆ 𝐷) |
287 | 286 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → {𝑞} ⊆ 𝐷) |
288 | | sseqin2 3817 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞}) |
289 | 287, 288 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐷 ∩ {𝑞}) = {𝑞}) |
290 | 289 | reseq2d 5396 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ {𝑞})) |
291 | 290 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞}))) |
292 | 96 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
293 | 219 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → dom (𝑇 ↾ 𝐷) = 𝐷) |
294 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐷) |
295 | 292, 293,
294 | dpjlem 18450 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})) = ((𝑇 ↾ 𝐷)‘𝑞)) |
296 | 224 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
297 | 291, 295,
296 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
298 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝑞 ∈ 𝐷) |
299 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞 ∈ 𝐷) |
300 | 298, 299 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐷 ∩ {𝑞}) = ∅) |
301 | 300 | reseq2d 5396 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ ∅)) |
302 | | res0 5400 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ↾ 𝐷) ↾ ∅) =
∅ |
303 | 301, 302 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅) |
304 | 303 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅)) |
305 | 108 | dprd0 18430 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
306 | 41, 305 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
307 | 306 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
308 | 307 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
309 | 304, 308,
194 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
310 | 309 | anassrs 680 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ ¬ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
311 | 297, 310 | pm2.61dan 832 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
312 | 311 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) = (#‘(𝑇‘𝑞))) |
313 | 312 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((#‘(𝑇‘𝑞)) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
314 | 278, 285,
313 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘𝐵) = ((#‘(𝑇‘𝑞)) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
315 | 259, 314 | breqtrd 4679 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (#‘𝐵))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((#‘(𝑇‘𝑞)) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
316 | 118 | nnne0d 11065 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0) |
317 | | dvdsmulcr 15011 |
. . . . . . . 8
⊢ (((𝑞↑(𝑞 pCnt (#‘𝐵))) ∈ ℤ ∧ (#‘(𝑇‘𝑞)) ∈ ℤ ∧ ((#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (#‘𝐵))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((#‘(𝑇‘𝑞)) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘(𝑇‘𝑞)))) |
318 | 74, 69, 119, 316, 317 | syl112anc 1330 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (#‘𝐵))) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((#‘(𝑇‘𝑞)) · (#‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘(𝑇‘𝑞)))) |
319 | 315, 318 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘(𝑇‘𝑞))) |
320 | | dvdseq 15036 |
. . . . . 6
⊢
((((#‘(𝑇‘𝑞)) ∈ ℕ0 ∧ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∈ ℕ0) ∧
((#‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (#‘𝐵))) ∥ (#‘(𝑇‘𝑞)))) → (#‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
321 | 68, 88, 61, 319, 320 | syl22anc 1327 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
322 | 6, 7, 8, 9, 10, 11 | ablfac1a 18468 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (#‘𝐵)))) |
323 | 321, 322 | eqtr4d 2659 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (#‘(𝑇‘𝑞)) = (#‘(𝑆‘𝑞))) |
324 | | hashen 13135 |
. . . . 5
⊢ (((𝑇‘𝑞) ∈ Fin ∧ (𝑆‘𝑞) ∈ Fin) → ((#‘(𝑇‘𝑞)) = (#‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
325 | 29, 24, 324 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((#‘(𝑇‘𝑞)) = (#‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
326 | 323, 325 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ≈ (𝑆‘𝑞)) |
327 | | fisseneq 8171 |
. . 3
⊢ (((𝑆‘𝑞) ∈ Fin ∧ (𝑇‘𝑞) ⊆ (𝑆‘𝑞) ∧ (𝑇‘𝑞) ≈ (𝑆‘𝑞)) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
328 | 24, 87, 326, 327 | syl3anc 1326 |
. 2
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
329 | 5, 19, 328 | eqfnfvd 6314 |
1
⊢ (𝜑 → 𝑇 = 𝑆) |