Step | Hyp | Ref
| Expression |
1 | | ablfac1eu.1 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) |
2 | 1 | simpld 487 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
3 | | ablfac1eu.2 |
. . . 4
⊢ (𝜑 → dom 𝑇 = 𝐴) |
4 | 2, 3 | dprdf2 18882 |
. . 3
⊢ (𝜑 → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
5 | 4 | ffnd 6347 |
. 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 18945 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
13 | 6 | fvexi 6515 |
. . . . . . 7
⊢ 𝐵 ∈ V |
14 | 13 | rabex 5092 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V |
15 | 14, 8 | dmmpti 6324 |
. . . . 5
⊢ dom 𝑆 = 𝐴 |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → dom 𝑆 = 𝐴) |
17 | 12, 16 | dprdf2 18882 |
. . 3
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
18 | 17 | ffnd 6347 |
. 2
⊢ (𝜑 → 𝑆 Fn 𝐴) |
19 | 10 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin) |
20 | 17 | ffvelrnda 6678 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
21 | 6 | subgss 18067 |
. . . . 5
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵) |
23 | 19, 22 | ssfid 8538 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin) |
24 | 4 | ffvelrnda 6678 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
25 | 6 | subgss 18067 |
. . . . . 6
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (𝑇‘𝑞) ⊆ 𝐵) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ 𝐵) |
27 | 24 | adantr 473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
28 | 19, 26 | ssfid 8538 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ Fin) |
29 | 28 | adantr 473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ Fin) |
30 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ (𝑇‘𝑞)) |
31 | 7 | odsubdvds 18460 |
. . . . . . 7
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇‘𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) |
32 | 27, 29, 30, 31 | syl3anc 1351 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) |
33 | | ablfac1eu.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
34 | 11 | sselda 3860 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ) |
35 | | prmz 15878 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℤ) |
37 | | ablfac1eu.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈
ℕ0) |
38 | 37 | nn0zd 11901 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℤ) |
39 | | ablgrp 18674 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
40 | 9, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ Grp) |
41 | 6 | grpbn0 17923 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ≠ ∅) |
43 | | hashnncl 13545 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ Fin →
((♯‘𝐵) ∈
ℕ ↔ 𝐵 ≠
∅)) |
44 | 10, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
45 | 42, 44 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ) |
46 | 45 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ) |
47 | 34, 46 | pccld 16046 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
ℕ0) |
48 | 47 | nn0zd 11901 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) |
49 | 6 | lagsubg 18128 |
. . . . . . . . . . . . 13
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) |
50 | 24, 19, 49 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) |
51 | 33, 50 | eqbrtrrd 4954 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (♯‘𝐵)) |
52 | 46 | nnzd 11902 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℤ) |
53 | | pcdvdsb 16064 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℤ ∧ 𝐶 ∈
ℕ0) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) |
54 | 34, 52, 37, 53 | syl3anc 1351 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) |
55 | 51, 54 | mpbird 249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ≤ (𝑞 pCnt (♯‘𝐵))) |
56 | | eluz2 12067 |
. . . . . . . . . 10
⊢ ((𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (♯‘𝐵)))) |
57 | 38, 48, 55, 56 | syl3anbrc 1323 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶)) |
58 | | dvdsexp 15540 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0
∧ (𝑞 pCnt
(♯‘𝐵)) ∈
(ℤ≥‘𝐶)) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
59 | 36, 37, 57, 58 | syl3anc 1351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
60 | 33, 59 | eqbrtrd 4952 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
61 | 60 | adantr 473 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
62 | 26 | sselda 3860 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ 𝐵) |
63 | 6, 7 | odcl 18429 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈
ℕ0) |
64 | 62, 63 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈
ℕ0) |
65 | 64 | nn0zd 11901 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℤ) |
66 | | hashcl 13535 |
. . . . . . . . . 10
⊢ ((𝑇‘𝑞) ∈ Fin → (♯‘(𝑇‘𝑞)) ∈
ℕ0) |
67 | 28, 66 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈
ℕ0) |
68 | 67 | nn0zd 11901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℤ) |
69 | 68 | adantr 473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∈ ℤ) |
70 | | prmnn 15877 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
71 | 34, 70 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℕ) |
72 | 71, 47 | nnexpcld 13424 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ) |
73 | 72 | nnzd 11902 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) |
74 | 73 | adantr 473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) |
75 | | dvdstr 15509 |
. . . . . . 7
⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (♯‘(𝑇‘𝑞)) ∈ ℤ ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)) ∧ (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) |
76 | 65, 69, 74, 75 | syl3anc 1351 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (((𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞)) ∧ (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) |
77 | 32, 61, 76 | mp2and 686 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
78 | 26, 77 | ssrabdv 3942 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
79 | | id 22 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → 𝑝 = 𝑞) |
80 | | oveq1 6985 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → (𝑝 pCnt (♯‘𝐵)) = (𝑞 pCnt (♯‘𝐵))) |
81 | 79, 80 | oveq12d 6996 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
82 | 81 | breq2d 4942 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) |
83 | 82 | rabbidv 3403 |
. . . . . 6
⊢ (𝑝 = 𝑞 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
84 | 83, 8, 14 | fvmpt3i 6602 |
. . . . 5
⊢ (𝑞 ∈ 𝐴 → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
85 | 84 | adantl 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
86 | 78, 85 | sseqtr4d 3900 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ (𝑆‘𝑞)) |
87 | 72 | nnnn0d 11770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈
ℕ0) |
88 | | pcdvds 16059 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℕ) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
89 | 34, 46, 88 | syl2anc 576 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
90 | 2 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑇) |
91 | 3 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑇 = 𝐴) |
92 | | ablfac1.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
93 | 92 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 ⊆ 𝐴) |
94 | 90, 91, 93 | dprdres 18903 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
95 | 94 | simpld 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
96 | 4 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
97 | 96, 93 | fssresd 6376 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
98 | 97 | fdmd 6355 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom (𝑇 ↾ 𝐷) = 𝐷) |
99 | | difssd 4001 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷) |
100 | 95, 98, 99 | dprdres 18903 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
101 | 100 | simpld 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
102 | | dprdsubg 18899 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
104 | 6 | lagsubg 18128 |
. . . . . . . . . 10
⊢ (((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) |
105 | 103, 19, 104 | syl2anc 576 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) |
106 | | eqid 2778 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
107 | 106 | subg0cl 18074 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
108 | 103, 107 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
109 | 108 | ne0d 4189 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅) |
110 | 6 | dprdssv 18891 |
. . . . . . . . . . . . . 14
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵 |
111 | | ssfi 8535 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
112 | 19, 110, 111 | sylancl 577 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
113 | | hashnncl 13545 |
. . . . . . . . . . . . 13
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
115 | 109, 114 | mpbird 249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ) |
116 | 115 | nnzd 11902 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) |
117 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → 𝑥 = 𝑞) |
118 | | sneq 4452 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑞 → {𝑥} = {𝑞}) |
119 | 118 | difeq2d 3991 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞})) |
120 | 119 | reseq2d 5696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
121 | 120 | oveq2d 6994 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
122 | 121 | fveq2d 6505 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) = (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
123 | 117, 122 | breq12d 4943 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
124 | 123 | notbid 310 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → (¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
125 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) |
126 | 9 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐺 ∈ Abel) |
127 | 10 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐵 ∈ Fin) |
128 | | ablfac1c.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} |
129 | 128 | ssrab3 3949 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆
ℙ |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ) |
131 | | ssidd 3882 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ 𝐷) |
132 | 2, 3, 92 | dprdres 18903 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
133 | 132 | simpld 487 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
134 | | dprdsubg 18899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ 𝐷) → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
136 | | difssd 4001 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ 𝐴) |
137 | 2, 3, 136 | dprdres 18903 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd 𝑇))) |
138 | 137 | simpld 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) |
139 | | dprdsubg 18899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
141 | | difss 4000 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∖ 𝐷) ⊆ 𝐴 |
142 | | fssres 6375 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴 ∖ 𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
143 | 4, 141, 142 | sylancl 577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
144 | 143 | fdmd 6355 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷)) |
145 | | fvres 6520 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
146 | 145 | adantl 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
147 | | eldif 3841 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) ↔ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) |
148 | 28 | adantrr 704 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ∈ Fin) |
149 | 106 | subg0cl 18074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
150 | 24, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
151 | 150 | snssd 4617 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
152 | 151 | adantrr 704 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
153 | 33 | adantrr 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
154 | 34 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ) |
155 | | iddvdsexp 15496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
156 | 36, 155 | sylan 572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
157 | 51 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞↑𝐶) ∥ (♯‘𝐵)) |
158 | 33, 68 | eqeltrrd 2867 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∈ ℤ) |
159 | | dvdstr 15509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑞 ∈ ℤ ∧ (𝑞↑𝐶) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
160 | 36, 158, 52, 159 | syl3anc 1351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
161 | 160 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
162 | 156, 157,
161 | mp2and 686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (♯‘𝐵)) |
163 | | breq1 4933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤 = 𝑞 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑞 ∥ (♯‘𝐵))) |
164 | 163, 128 | elrab2 3599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (♯‘𝐵))) |
165 | 154, 162,
164 | sylanbrc 575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ 𝐷) |
166 | 165 | ex 405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ∈ ℕ → 𝑞 ∈ 𝐷)) |
167 | 166 | con3d 150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ)) |
168 | 167 | impr 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝐶 ∈ ℕ) |
169 | 37 | adantrr 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 ∈
ℕ0) |
170 | | elnn0 11712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐶 ∈ ℕ0
↔ (𝐶 ∈ ℕ
∨ 𝐶 =
0)) |
171 | 169, 170 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0)) |
172 | 171 | ord 850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0)) |
173 | 168, 172 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 = 0) |
174 | 173 | oveq2d 6994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑𝐶) = (𝑞↑0)) |
175 | 71 | adantrr 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℕ) |
176 | 175 | nncnd 11459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℂ) |
177 | 176 | exp0d 13322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑0) = 1) |
178 | 153, 174,
177 | 3eqtrd 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = 1) |
179 | | fvex 6514 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(0g‘𝐺) ∈ V |
180 | | hashsng 13547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0g‘𝐺) ∈ V →
(♯‘{(0g‘𝐺)}) = 1) |
181 | 179, 180 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(♯‘{(0g‘𝐺)}) = 1 |
182 | 178, 181 | syl6reqr 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
(♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞))) |
183 | | snfi 8393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
{(0g‘𝐺)} ∈ Fin |
184 | | hashen 13525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(({(0g‘𝐺)} ∈ Fin ∧ (𝑇‘𝑞) ∈ Fin) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
185 | 183, 148,
184 | sylancr 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
186 | 182, 185 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ≈ (𝑇‘𝑞)) |
187 | | fisseneq 8526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑇‘𝑞) ∈ Fin ∧
{(0g‘𝐺)}
⊆ (𝑇‘𝑞) ∧
{(0g‘𝐺)}
≈ (𝑇‘𝑞)) →
{(0g‘𝐺)} =
(𝑇‘𝑞)) |
188 | 148, 152,
186, 187 | syl3anc 1351 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} = (𝑇‘𝑞)) |
189 | 106 | subg0cl 18074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
190 | 135, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
191 | 190 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
192 | 191 | snssd 4617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
193 | 188, 192 | eqsstr3d 3898 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
194 | 147, 193 | sylan2b 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
195 | 146, 194 | eqsstrd 3897 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
196 | 138, 144,
135, 195 | dprdlub 18901 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
197 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
198 | 197 | lsmss2 18555 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
199 | 135, 140,
196, 198 | syl3anc 1351 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
200 | | disjdif 4305 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅ |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅) |
202 | | undif2 4309 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∪ (𝐴 ∖ 𝐷)) = (𝐷 ∪ 𝐴) |
203 | | ssequn1 4046 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∪ 𝐴) = 𝐴) |
204 | 92, 203 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐷 ∪ 𝐴) = 𝐴) |
205 | 202, 204 | syl5req 2827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 = (𝐷 ∪ (𝐴 ∖ 𝐷))) |
206 | 4, 201, 205, 197, 2 | dprdsplit 18923 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))))) |
207 | 1 | simprd 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝐵) |
208 | 206, 207 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = 𝐵) |
209 | 199, 208 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
210 | 133, 209 | jca 504 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
211 | 210 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
212 | 4, 92 | fssresd 6376 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
213 | 212 | fdmd 6355 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑇 ↾ 𝐷) = 𝐷) |
214 | 213 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → dom (𝑇 ↾ 𝐷) = 𝐷) |
215 | 92 | sselda 3860 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐴) |
216 | 215, 37 | syldan 582 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
217 | 216 | adantlr 702 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
218 | | fvres 6520 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ 𝐷 → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
219 | 218 | adantl 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
220 | 219 | fveq2d 6505 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (♯‘(𝑇‘𝑞))) |
221 | 215, 33 | syldan 582 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
222 | 220, 221 | eqtrd 2814 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
223 | 222 | adantlr 702 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
224 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝑥 ∈ ℙ) |
225 | | fzfid 13159 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...(♯‘𝐵)) ∈ Fin) |
226 | | prmnn 15877 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℕ) |
227 | 226 | 3ad2ant2 1114 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ) |
228 | | prmz 15878 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℤ) |
229 | | dvdsle 15523 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ ℤ ∧
(♯‘𝐵) ∈
ℕ) → (𝑤 ∥
(♯‘𝐵) →
𝑤 ≤ (♯‘𝐵))) |
230 | 228, 45, 229 | syl2anr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵))) |
231 | 230 | 3impia 1097 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵)) |
232 | 45 | nnzd 11902 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) |
233 | 232 | 3ad2ant1 1113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) |
234 | | fznn 12794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝐵)
∈ ℤ → (𝑤
∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) |
235 | 233, 234 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) |
236 | 227, 231,
235 | mpbir2and 700 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵))) |
237 | 236 | rabssdv 3943 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))) |
238 | 128, 237 | syl5eqss 3907 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 ⊆ (1...(♯‘𝐵))) |
239 | 225, 238 | ssfid 8538 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ Fin) |
240 | 239 | adantr 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ∈ Fin) |
241 | 6, 7, 125, 126, 127, 130, 128, 131, 211, 214, 217, 223, 224, 240 | ablfac1eulem 18947 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
242 | 241 | ralrimiva 3132 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
243 | 242 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
244 | 124, 243,
34 | rspcdva 3541 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
245 | | coprm 15914 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
246 | 34, 116, 245 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
247 | 244, 246 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
248 | | rpexp1i 15924 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
→ ((𝑞 gcd
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
249 | 36, 116, 47, 248 | syl3anc 1351 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
250 | 247, 249 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
251 | | coprmdvds2 15857 |
. . . . . . . . . 10
⊢ ((((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘𝐵) ∈
ℤ) ∧ ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) |
252 | 73, 116, 52, 250, 251 | syl31anc 1353 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) |
253 | 89, 105, 252 | mp2and 686 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)) |
254 | | eqid 2778 |
. . . . . . . . . 10
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
255 | | inss1 4094 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∩ {𝑞}) ⊆ 𝐷 |
256 | 255 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷) |
257 | 95, 98, 256 | dprdres 18903 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
258 | 257 | simpld 487 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) |
259 | | dprdsubg 18899 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
260 | 258, 259 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
261 | | inass 4085 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) |
262 | | disjdif 4305 |
. . . . . . . . . . . . . 14
⊢ ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅ |
263 | 262 | ineq2i 4075 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅) |
264 | | in0 4233 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ∅) =
∅ |
265 | 261, 263,
264 | 3eqtri 2806 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅ |
266 | 265 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅) |
267 | 95, 98, 256, 99, 266, 106 | dprddisj2 18914 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0g‘𝐺)}) |
268 | 95, 98, 256, 99, 266, 254 | dprdcntz2 18913 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
269 | 6 | dprdssv 18891 |
. . . . . . . . . . 11
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵 |
270 | | ssfi 8535 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
271 | 19, 269, 270 | sylancl 577 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
272 | 197, 106,
254, 260, 103, 267, 268, 271, 112 | lsmhash 18592 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
273 | | inundif 4311 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷 |
274 | 273 | eqcomi 2787 |
. . . . . . . . . . . . 13
⊢ 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) |
275 | 274 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))) |
276 | 97, 266, 275, 197, 95 | dprdsplit 18923 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
277 | 209 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
278 | 276, 277 | eqtr3d 2816 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵) |
279 | 278 | fveq2d 6505 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (♯‘𝐵)) |
280 | | snssi 4616 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ 𝐷 → {𝑞} ⊆ 𝐷) |
281 | 280 | adantl 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → {𝑞} ⊆ 𝐷) |
282 | | sseqin2 4081 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞}) |
283 | 281, 282 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐷 ∩ {𝑞}) = {𝑞}) |
284 | 283 | reseq2d 5696 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ {𝑞})) |
285 | 284 | oveq2d 6994 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞}))) |
286 | 95 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
287 | 213 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → dom (𝑇 ↾ 𝐷) = 𝐷) |
288 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐷) |
289 | 286, 287,
288 | dpjlem 18926 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})) = ((𝑇 ↾ 𝐷)‘𝑞)) |
290 | 218 | adantl 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
291 | 285, 289,
290 | 3eqtrd 2818 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
292 | | simprr 760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝑞 ∈ 𝐷) |
293 | | disjsn 4522 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞 ∈ 𝐷) |
294 | 292, 293 | sylibr 226 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐷 ∩ {𝑞}) = ∅) |
295 | 294 | reseq2d 5696 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ ∅)) |
296 | | res0 5700 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ↾ 𝐷) ↾ ∅) =
∅ |
297 | 295, 296 | syl6eq 2830 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅) |
298 | 297 | oveq2d 6994 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅)) |
299 | 106 | dprd0 18906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
300 | 40, 299 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
301 | 300 | simprd 488 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
302 | 301 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
303 | 298, 302,
188 | 3eqtrd 2818 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
304 | 303 | anassrs 460 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ ¬ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
305 | 291, 304 | pm2.61dan 800 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
306 | 305 | fveq2d 6505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) = (♯‘(𝑇‘𝑞))) |
307 | 306 | oveq1d 6993 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
308 | 272, 279,
307 | 3eqtr3d 2822 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
309 | 253, 308 | breqtrd 4956 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
310 | 115 | nnne0d 11493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0) |
311 | | dvdsmulcr 15502 |
. . . . . . . 8
⊢ (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝑇‘𝑞)) ∈ ℤ ∧
((♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) |
312 | 73, 68, 116, 310, 311 | syl112anc 1354 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) |
313 | 309, 312 | mpbid 224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))) |
314 | | dvdseq 15527 |
. . . . . 6
⊢
((((♯‘(𝑇‘𝑞)) ∈ ℕ0 ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0) ∧
((♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
315 | 67, 87, 60, 313, 314 | syl22anc 826 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
316 | 6, 7, 8, 9, 10, 11 | ablfac1a 18944 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
317 | 315, 316 | eqtr4d 2817 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞))) |
318 | | hashen 13525 |
. . . . 5
⊢ (((𝑇‘𝑞) ∈ Fin ∧ (𝑆‘𝑞) ∈ Fin) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
319 | 28, 23, 318 | syl2anc 576 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
320 | 317, 319 | mpbid 224 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ≈ (𝑆‘𝑞)) |
321 | | fisseneq 8526 |
. . 3
⊢ (((𝑆‘𝑞) ∈ Fin ∧ (𝑇‘𝑞) ⊆ (𝑆‘𝑞) ∧ (𝑇‘𝑞) ≈ (𝑆‘𝑞)) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
322 | 23, 86, 320, 321 | syl3anc 1351 |
. 2
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
323 | 5, 18, 322 | eqfnfvd 6632 |
1
⊢ (𝜑 → 𝑇 = 𝑆) |