Step | Hyp | Ref
| Expression |
1 | | ablfac1eu.1 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) |
2 | 1 | simpld 495 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑇) |
3 | | ablfac1eu.2 |
. . . 4
⊢ (𝜑 → dom 𝑇 = 𝐴) |
4 | 2, 3 | dprdf2 19619 |
. . 3
⊢ (𝜑 → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
5 | 4 | ffnd 6610 |
. 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 19682 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
13 | 6 | fvexi 6797 |
. . . . . . 7
⊢ 𝐵 ∈ V |
14 | 13 | rabex 5257 |
. . . . . 6
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V |
15 | 14, 8 | dmmpti 6586 |
. . . . 5
⊢ dom 𝑆 = 𝐴 |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → dom 𝑆 = 𝐴) |
17 | 12, 16 | dprdf2 19619 |
. . 3
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
18 | 17 | ffnd 6610 |
. 2
⊢ (𝜑 → 𝑆 Fn 𝐴) |
19 | 10 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐵 ∈ Fin) |
20 | 17 | ffvelrnda 6970 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ (SubGrp‘𝐺)) |
21 | 6 | subgss 18765 |
. . . . 5
⊢ ((𝑆‘𝑞) ∈ (SubGrp‘𝐺) → (𝑆‘𝑞) ⊆ 𝐵) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ⊆ 𝐵) |
23 | 19, 22 | ssfid 9051 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) ∈ Fin) |
24 | 4 | ffvelrnda 6970 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
25 | 6 | subgss 18765 |
. . . . . 6
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (𝑇‘𝑞) ⊆ 𝐵) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ 𝐵) |
27 | 26 | sselda 3922 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ 𝐵) |
28 | 6, 7 | odcl 19153 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈
ℕ0) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈
ℕ0) |
30 | 29 | nn0zd 12433 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∈ ℤ) |
31 | 19, 26 | ssfid 9051 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ∈ Fin) |
32 | | hashcl 14080 |
. . . . . . . . 9
⊢ ((𝑇‘𝑞) ∈ Fin → (♯‘(𝑇‘𝑞)) ∈
ℕ0) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈
ℕ0) |
34 | 33 | nn0zd 12433 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∈ ℤ) |
35 | 34 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∈ ℤ) |
36 | 11 | sselda 3922 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℙ) |
37 | | prmnn 16388 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℕ) |
39 | | ablgrp 19400 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
40 | 9, 39 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ Grp) |
41 | 6 | grpbn0 18617 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ≠ ∅) |
43 | | hashnncl 14090 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ Fin →
((♯‘𝐵) ∈
ℕ ↔ 𝐵 ≠
∅)) |
44 | 10, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
45 | 42, 44 | mpbird 256 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ) |
46 | 45 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ) |
47 | 36, 46 | pccld 16560 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
ℕ0) |
48 | 38, 47 | nnexpcld 13969 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ) |
49 | 48 | nnzd 12434 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) |
50 | 49 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ) |
51 | 24 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ (SubGrp‘𝐺)) |
52 | 31 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑇‘𝑞) ∈ Fin) |
53 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → 𝑥 ∈ (𝑇‘𝑞)) |
54 | 7 | odsubdvds 19185 |
. . . . . . 7
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ (𝑇‘𝑞) ∈ Fin ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) |
55 | 51, 52, 53, 54 | syl3anc 1370 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (♯‘(𝑇‘𝑞))) |
56 | | ablfac1eu.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
57 | | prmz 16389 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
58 | 36, 57 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ ℤ) |
59 | | ablfac1eu.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈
ℕ0) |
60 | 59 | nn0zd 12433 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℤ) |
61 | 47 | nn0zd 12433 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈ ℤ) |
62 | 6 | lagsubg 18827 |
. . . . . . . . . . . . 13
⊢ (((𝑇‘𝑞) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) |
63 | 24, 19, 62 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (♯‘𝐵)) |
64 | 56, 63 | eqbrtrrd 5099 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (♯‘𝐵)) |
65 | 46 | nnzd 12434 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) ∈ ℤ) |
66 | | pcdvdsb 16579 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℤ ∧ 𝐶 ∈
ℕ0) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) |
67 | 36, 65, 59, 66 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ≤ (𝑞 pCnt (♯‘𝐵)) ↔ (𝑞↑𝐶) ∥ (♯‘𝐵))) |
68 | 64, 67 | mpbird 256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ≤ (𝑞 pCnt (♯‘𝐵))) |
69 | | eluz2 12597 |
. . . . . . . . . 10
⊢ ((𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶) ↔ (𝐶 ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℤ ∧ 𝐶 ≤ (𝑞 pCnt (♯‘𝐵)))) |
70 | 60, 61, 68, 69 | syl3anbrc 1342 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 pCnt (♯‘𝐵)) ∈
(ℤ≥‘𝐶)) |
71 | | dvdsexp 16046 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ0
∧ (𝑞 pCnt
(♯‘𝐵)) ∈
(ℤ≥‘𝐶)) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
72 | 58, 59, 70, 71 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
73 | 56, 72 | eqbrtrd 5097 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
74 | 73 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
75 | 30, 35, 50, 55, 74 | dvdstrd 16013 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑥 ∈ (𝑇‘𝑞)) → (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
76 | 26, 75 | ssrabdv 4008 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
77 | | id 22 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → 𝑝 = 𝑞) |
78 | | oveq1 7291 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → (𝑝 pCnt (♯‘𝐵)) = (𝑞 pCnt (♯‘𝐵))) |
79 | 77, 78 | oveq12d 7302 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
80 | 79 | breq2d 5087 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))))) |
81 | 80 | rabbidv 3415 |
. . . . . 6
⊢ (𝑝 = 𝑞 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
82 | 81, 8, 14 | fvmpt3i 6889 |
. . . . 5
⊢ (𝑞 ∈ 𝐴 → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
83 | 82 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑆‘𝑞) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵)))}) |
84 | 76, 83 | sseqtrrd 3963 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ⊆ (𝑆‘𝑞)) |
85 | 48 | nnnn0d 12302 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈
ℕ0) |
86 | | pcdvds 16574 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ ℙ ∧
(♯‘𝐵) ∈
ℕ) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
87 | 36, 46, 86 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) |
88 | 2 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd 𝑇) |
89 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom 𝑇 = 𝐴) |
90 | | ablfac1.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 ⊆ 𝐴) |
92 | 88, 89, 91 | dprdres 19640 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
93 | 92 | simpld 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
94 | 4 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝑇:𝐴⟶(SubGrp‘𝐺)) |
95 | 94, 91 | fssresd 6650 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
96 | 95 | fdmd 6620 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → dom (𝑇 ↾ 𝐷) = 𝐷) |
97 | | difssd 4068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∖ {𝑞}) ⊆ 𝐷) |
98 | 93, 96, 97 | dprdres 19640 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
99 | 98 | simpld 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
100 | | dprdsubg 19636 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
101 | 99, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺)) |
102 | 6 | lagsubg 18827 |
. . . . . . . . . 10
⊢ (((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) ∧ 𝐵 ∈ Fin) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) |
103 | 101, 19, 102 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) |
104 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝐺) = (0g‘𝐺) |
105 | 104 | subg0cl 18772 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
106 | 101, 105 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
107 | 106 | ne0d 4270 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅) |
108 | 6 | dprdssv 19628 |
. . . . . . . . . . . . . 14
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵 |
109 | | ssfi 8965 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
110 | 19, 108, 109 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin) |
111 | | hashnncl 14090 |
. . . . . . . . . . . . 13
⊢ ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ∈ Fin → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ ↔ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) ≠ ∅)) |
113 | 107, 112 | mpbird 256 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℕ) |
114 | 113 | nnzd 12434 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) |
115 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → 𝑥 = 𝑞) |
116 | | sneq 4572 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑞 → {𝑥} = {𝑞}) |
117 | 116 | difeq2d 4058 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑞 → (𝐷 ∖ {𝑥}) = (𝐷 ∖ {𝑞})) |
118 | 117 | reseq2d 5894 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑞 → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})) = ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))) |
119 | 118 | oveq2d 7300 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) |
120 | 119 | fveq2d 6787 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑞 → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) = (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
121 | 115, 120 | breq12d 5088 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
122 | 121 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑞 → (¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥})))) ↔ ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
123 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) = (𝑝 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ (𝑂‘𝑦) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) |
124 | 9 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐺 ∈ Abel) |
125 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐵 ∈ Fin) |
126 | | ablfac1c.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} |
127 | 126 | ssrab3 4016 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐷 ⊆
ℙ |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ ℙ) |
129 | | ssidd 3945 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ⊆ 𝐷) |
130 | 2, 3, 90 | dprdres 19640 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) ⊆ (𝐺 DProd 𝑇))) |
131 | 130 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
132 | | dprdsubg 19636 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ 𝐷) → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) |
134 | | difssd 4068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐴 ∖ 𝐷) ⊆ 𝐴) |
135 | 2, 3, 134 | dprdres 19640 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd 𝑇))) |
136 | 135 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) |
137 | | dprdsubg 19636 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺dom DProd (𝑇 ↾ (𝐴 ∖ 𝐷)) → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺)) |
139 | | difss 4067 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∖ 𝐷) ⊆ 𝐴 |
140 | | fssres 6649 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑇:𝐴⟶(SubGrp‘𝐺) ∧ (𝐴 ∖ 𝐷) ⊆ 𝐴) → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
141 | 4, 139, 140 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑇 ↾ (𝐴 ∖ 𝐷)):(𝐴 ∖ 𝐷)⟶(SubGrp‘𝐺)) |
142 | 141 | fdmd 6620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom (𝑇 ↾ (𝐴 ∖ 𝐷)) = (𝐴 ∖ 𝐷)) |
143 | | fvres 6802 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
144 | 143 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) = (𝑇‘𝑞)) |
145 | | eldif 3898 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (𝐴 ∖ 𝐷) ↔ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) |
146 | 31 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ∈ Fin) |
147 | 104 | subg0cl 18772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇‘𝑞) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
148 | 24, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑇‘𝑞)) |
149 | 148 | snssd 4743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
150 | 149 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝑇‘𝑞)) |
151 | | fvex 6796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(0g‘𝐺) ∈ V |
152 | | hashsng 14093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((0g‘𝐺) ∈ V →
(♯‘{(0g‘𝐺)}) = 1) |
153 | 151, 152 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(♯‘{(0g‘𝐺)}) = 1 |
154 | 56 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
155 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ ℙ) |
156 | | iddvdsexp 15998 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑞 ∈ ℤ ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
157 | 58, 156 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (𝑞↑𝐶)) |
158 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → (𝑞↑𝐶) ∥ (♯‘𝐵)) |
159 | 56, 34 | eqeltrrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑𝐶) ∈ ℤ) |
160 | | dvdstr 16012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑞 ∈ ℤ ∧ (𝑞↑𝐶) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
161 | 58, 159, 65, 160 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
162 | 161 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → ((𝑞 ∥ (𝑞↑𝐶) ∧ (𝑞↑𝐶) ∥ (♯‘𝐵)) → 𝑞 ∥ (♯‘𝐵))) |
163 | 157, 158,
162 | mp2and 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∥ (♯‘𝐵)) |
164 | | breq1 5078 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑤 = 𝑞 → (𝑤 ∥ (♯‘𝐵) ↔ 𝑞 ∥ (♯‘𝐵))) |
165 | 164, 126 | elrab2 3628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑞 ∈ 𝐷 ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ (♯‘𝐵))) |
166 | 155, 163,
165 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝐶 ∈ ℕ) → 𝑞 ∈ 𝐷) |
167 | 166 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐶 ∈ ℕ → 𝑞 ∈ 𝐷)) |
168 | 167 | con3d 152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∈ 𝐷 → ¬ 𝐶 ∈ ℕ)) |
169 | 168 | impr 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝐶 ∈ ℕ) |
170 | 59 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 ∈
ℕ0) |
171 | | elnn0 12244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐶 ∈ ℕ0
↔ (𝐶 ∈ ℕ
∨ 𝐶 =
0)) |
172 | 170, 171 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐶 ∈ ℕ ∨ 𝐶 = 0)) |
173 | 172 | ord 861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (¬ 𝐶 ∈ ℕ → 𝐶 = 0)) |
174 | 169, 173 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝐶 = 0) |
175 | 174 | oveq2d 7300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑𝐶) = (𝑞↑0)) |
176 | 38 | adantrr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℕ) |
177 | 176 | nncnd 11998 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → 𝑞 ∈ ℂ) |
178 | 177 | exp0d 13867 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑞↑0) = 1) |
179 | 154, 175,
178 | 3eqtrd 2783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (♯‘(𝑇‘𝑞)) = 1) |
180 | 153, 179 | eqtr4id 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
(♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞))) |
181 | | snfi 8843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
{(0g‘𝐺)} ∈ Fin |
182 | | hashen 14070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(({(0g‘𝐺)} ∈ Fin ∧ (𝑇‘𝑞) ∈ Fin) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
183 | 181, 146,
182 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) →
((♯‘{(0g‘𝐺)}) = (♯‘(𝑇‘𝑞)) ↔ {(0g‘𝐺)} ≈ (𝑇‘𝑞))) |
184 | 180, 183 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ≈ (𝑇‘𝑞)) |
185 | | fisseneq 9043 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑇‘𝑞) ∈ Fin ∧
{(0g‘𝐺)}
⊆ (𝑇‘𝑞) ∧
{(0g‘𝐺)}
≈ (𝑇‘𝑞)) →
{(0g‘𝐺)} =
(𝑇‘𝑞)) |
186 | 146, 150,
184, 185 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} = (𝑇‘𝑞)) |
187 | 104 | subg0cl 18772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
188 | 133, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
189 | 188 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (0g‘𝐺) ∈ (𝐺 DProd (𝑇 ↾ 𝐷))) |
190 | 189 | snssd 4743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → {(0g‘𝐺)} ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
191 | 186, 190 | eqsstrrd 3961 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
192 | 145, 191 | sylan2b 594 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → (𝑇‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
193 | 144, 192 | eqsstrd 3960 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑞 ∈ (𝐴 ∖ 𝐷)) → ((𝑇 ↾ (𝐴 ∖ 𝐷))‘𝑞) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
194 | 136, 142,
133, 193 | dprdlub 19638 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) |
195 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) |
196 | 195 | lsmss2 19282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 DProd (𝑇 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷))) → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
197 | 133, 138,
194, 196 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = (𝐺 DProd (𝑇 ↾ 𝐷))) |
198 | | disjdif 4406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅ |
199 | 198 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐷 ∩ (𝐴 ∖ 𝐷)) = ∅) |
200 | | undif2 4411 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∪ (𝐴 ∖ 𝐷)) = (𝐷 ∪ 𝐴) |
201 | | ssequn1 4115 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐷 ⊆ 𝐴 ↔ (𝐷 ∪ 𝐴) = 𝐴) |
202 | 90, 201 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐷 ∪ 𝐴) = 𝐴) |
203 | 200, 202 | eqtr2id 2792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 = (𝐷 ∪ (𝐴 ∖ 𝐷))) |
204 | 4, 199, 203, 195, 2 | dprdsplit 19660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷))))) |
205 | 1 | simprd 496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝐵) |
206 | 204, 205 | eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ 𝐷))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ (𝐴 ∖ 𝐷)))) = 𝐵) |
207 | 197, 206 | eqtr3d 2781 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
208 | 131, 207 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
209 | 208 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → (𝐺dom DProd (𝑇 ↾ 𝐷) ∧ (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵)) |
210 | 4, 90 | fssresd 6650 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑇 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) |
211 | 210 | fdmd 6620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑇 ↾ 𝐷) = 𝐷) |
212 | 211 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → dom (𝑇 ↾ 𝐷) = 𝐷) |
213 | 90 | sselda 3922 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐴) |
214 | 213, 59 | syldan 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
215 | 214 | adantlr 712 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → 𝐶 ∈
ℕ0) |
216 | | fvres 6802 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ 𝐷 → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
217 | 216 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
218 | 217 | fveq2d 6787 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (♯‘(𝑇‘𝑞))) |
219 | 213, 56 | syldan 591 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) |
220 | 218, 219 | eqtrd 2779 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
221 | 220 | adantlr 712 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℙ) ∧ 𝑞 ∈ 𝐷) → (♯‘((𝑇 ↾ 𝐷)‘𝑞)) = (𝑞↑𝐶)) |
222 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝑥 ∈ ℙ) |
223 | | fzfid 13702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...(♯‘𝐵)) ∈ Fin) |
224 | | prmnn 16388 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℕ) |
225 | 224 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ ℕ) |
226 | | prmz 16389 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℙ → 𝑤 ∈
ℤ) |
227 | | dvdsle 16028 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 ∈ ℤ ∧
(♯‘𝐵) ∈
ℕ) → (𝑤 ∥
(♯‘𝐵) →
𝑤 ≤ (♯‘𝐵))) |
228 | 226, 45, 227 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ) → (𝑤 ∥ (♯‘𝐵) → 𝑤 ≤ (♯‘𝐵))) |
229 | 228 | 3impia 1116 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ≤ (♯‘𝐵)) |
230 | 45 | nnzd 12434 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) |
231 | 230 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ) |
232 | | fznn 13333 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝐵)
∈ ℤ → (𝑤
∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → (𝑤 ∈ (1...(♯‘𝐵)) ↔ (𝑤 ∈ ℕ ∧ 𝑤 ≤ (♯‘𝐵)))) |
234 | 225, 229,
233 | mpbir2and 710 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ (♯‘𝐵)) → 𝑤 ∈ (1...(♯‘𝐵))) |
235 | 234 | rabssdv 4009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))) |
236 | 126, 235 | eqsstrid 3970 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 ⊆ (1...(♯‘𝐵))) |
237 | 223, 236 | ssfid 9051 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐷 ∈ Fin) |
238 | 237 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → 𝐷 ∈ Fin) |
239 | 6, 7, 123, 124, 125, 128, 126, 129, 209, 212, 215, 221, 222, 238 | ablfac1eulem 19684 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℙ) → ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
240 | 239 | ralrimiva 3104 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
241 | 240 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ∀𝑥 ∈ ℙ ¬ 𝑥 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑥}))))) |
242 | 122, 241,
36 | rspcdva 3563 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
243 | | coprm 16425 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
244 | 36, 114, 243 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (¬ 𝑞 ∥ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ↔ (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
245 | 242, 244 | mpbid 231 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
246 | | rpexp1i 16437 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧ (𝑞 pCnt (♯‘𝐵)) ∈ ℕ0)
→ ((𝑞 gcd
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
247 | 58, 114, 47, 246 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞 gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1 → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1)) |
248 | 245, 247 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) |
249 | | coprmdvds2 16368 |
. . . . . . . . . 10
⊢ ((((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘𝐵) ∈
ℤ) ∧ ((𝑞↑(𝑞 pCnt (♯‘𝐵))) gcd (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = 1) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) |
250 | 49, 114, 65, 248, 249 | syl31anc 1372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∥ (♯‘𝐵)) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵))) |
251 | 87, 103, 250 | mp2and 696 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ (♯‘𝐵)) |
252 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
253 | | inss1 4163 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∩ {𝑞}) ⊆ 𝐷 |
254 | 253 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐷 ∩ {𝑞}) ⊆ 𝐷) |
255 | 93, 96, 254 | dprdres 19640 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ (𝐺 DProd (𝑇 ↾ 𝐷)))) |
256 | 255 | simpld 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) |
257 | | dprdsubg 19636 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
258 | 256, 257 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ (SubGrp‘𝐺)) |
259 | | inass 4154 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) |
260 | | disjdif 4406 |
. . . . . . . . . . . . . 14
⊢ ({𝑞} ∩ (𝐷 ∖ {𝑞})) = ∅ |
261 | 260 | ineq2i 4144 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ({𝑞} ∩ (𝐷 ∖ {𝑞}))) = (𝐷 ∩ ∅) |
262 | | in0 4326 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∩ ∅) =
∅ |
263 | 259, 261,
262 | 3eqtri 2771 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅ |
264 | 263 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐷 ∩ {𝑞}) ∩ (𝐷 ∖ {𝑞})) = ∅) |
265 | 93, 96, 254, 97, 264, 104 | dprddisj2 19651 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∩ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = {(0g‘𝐺)}) |
266 | 93, 96, 254, 97, 264, 252 | dprdcntz2 19650 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
267 | 6 | dprdssv 19628 |
. . . . . . . . . . 11
⊢ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵 |
268 | | ssfi 8965 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ⊆ 𝐵) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
269 | 19, 267, 268 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) ∈ Fin) |
270 | 195, 104,
252, 258, 101, 265, 266, 269, 110 | lsmhash 19320 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
271 | | inundif 4413 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) = 𝐷 |
272 | 271 | eqcomi 2748 |
. . . . . . . . . . . . 13
⊢ 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞})) |
273 | 272 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐷 = ((𝐷 ∩ {𝑞}) ∪ (𝐷 ∖ {𝑞}))) |
274 | 95, 264, 273, 195, 93 | dprdsplit 19660 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) |
275 | 207 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd (𝑇 ↾ 𝐷)) = 𝐵) |
276 | 274, 275 | eqtr3d 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) = 𝐵) |
277 | 276 | fveq2d 6787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘((𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))(LSSum‘𝐺)(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = (♯‘𝐵)) |
278 | | snssi 4742 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ 𝐷 → {𝑞} ⊆ 𝐷) |
279 | 278 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → {𝑞} ⊆ 𝐷) |
280 | | sseqin2 4150 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑞} ⊆ 𝐷 ↔ (𝐷 ∩ {𝑞}) = {𝑞}) |
281 | 279, 280 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐷 ∩ {𝑞}) = {𝑞}) |
282 | 281 | reseq2d 5894 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ {𝑞})) |
283 | 282 | oveq2d 7300 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞}))) |
284 | 93 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝐺dom DProd (𝑇 ↾ 𝐷)) |
285 | 211 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → dom (𝑇 ↾ 𝐷) = 𝐷) |
286 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → 𝑞 ∈ 𝐷) |
287 | 284, 285,
286 | dpjlem 19663 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ {𝑞})) = ((𝑇 ↾ 𝐷)‘𝑞)) |
288 | 216 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → ((𝑇 ↾ 𝐷)‘𝑞) = (𝑇‘𝑞)) |
289 | 283, 287,
288 | 3eqtrd 2783 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
290 | | simprr 770 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ¬ 𝑞 ∈ 𝐷) |
291 | | disjsn 4648 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∩ {𝑞}) = ∅ ↔ ¬ 𝑞 ∈ 𝐷) |
292 | 290, 291 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐷 ∩ {𝑞}) = ∅) |
293 | 292 | reseq2d 5894 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ((𝑇 ↾ 𝐷) ↾ ∅)) |
294 | | res0 5898 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ↾ 𝐷) ↾ ∅) =
∅ |
295 | 293, 294 | eqtrdi 2795 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})) = ∅) |
296 | 295 | oveq2d 7300 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝐺 DProd ∅)) |
297 | 104 | dprd0 19643 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
298 | 40, 297 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) =
{(0g‘𝐺)})) |
299 | 298 | simprd 496 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
300 | 299 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ∅) =
{(0g‘𝐺)}) |
301 | 296, 300,
186 | 3eqtrd 2783 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ∈ 𝐷)) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
302 | 301 | anassrs 468 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑞 ∈ 𝐴) ∧ ¬ 𝑞 ∈ 𝐷) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
303 | 289, 302 | pm2.61dan 810 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞}))) = (𝑇‘𝑞)) |
304 | 303 | fveq2d 6787 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) = (♯‘(𝑇‘𝑞))) |
305 | 304 | oveq1d 7299 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∩ {𝑞})))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
306 | 270, 277,
305 | 3eqtr3d 2787 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘𝐵) = ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
307 | 251, 306 | breqtrd 5101 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))))) |
308 | 113 | nnne0d 12032 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0) |
309 | | dvdsmulcr 16004 |
. . . . . . . 8
⊢ (((𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℤ ∧
(♯‘(𝑇‘𝑞)) ∈ ℤ ∧
((♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ∈ ℤ ∧
(♯‘(𝐺 DProd
((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞})))) ≠ 0)) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) |
310 | 49, 34, 114, 308, 309 | syl112anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (((𝑞↑(𝑞 pCnt (♯‘𝐵))) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ∥ ((♯‘(𝑇‘𝑞)) · (♯‘(𝐺 DProd ((𝑇 ↾ 𝐷) ↾ (𝐷 ∖ {𝑞}))))) ↔ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) |
311 | 307, 310 | mpbid 231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞))) |
312 | | dvdseq 16032 |
. . . . . 6
⊢
((((♯‘(𝑇‘𝑞)) ∈ ℕ0 ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∈ ℕ0) ∧
((♯‘(𝑇‘𝑞)) ∥ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∧ (𝑞↑(𝑞 pCnt (♯‘𝐵))) ∥ (♯‘(𝑇‘𝑞)))) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
313 | 33, 85, 73, 311, 312 | syl22anc 836 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
314 | 6, 7, 8, 9, 10, 11 | ablfac1a 19681 |
. . . . 5
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑆‘𝑞)) = (𝑞↑(𝑞 pCnt (♯‘𝐵)))) |
315 | 313, 314 | eqtr4d 2782 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞))) |
316 | | hashen 14070 |
. . . . 5
⊢ (((𝑇‘𝑞) ∈ Fin ∧ (𝑆‘𝑞) ∈ Fin) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
317 | 31, 23, 316 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → ((♯‘(𝑇‘𝑞)) = (♯‘(𝑆‘𝑞)) ↔ (𝑇‘𝑞) ≈ (𝑆‘𝑞))) |
318 | 315, 317 | mpbid 231 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) ≈ (𝑆‘𝑞)) |
319 | | fisseneq 9043 |
. . 3
⊢ (((𝑆‘𝑞) ∈ Fin ∧ (𝑇‘𝑞) ⊆ (𝑆‘𝑞) ∧ (𝑇‘𝑞) ≈ (𝑆‘𝑞)) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
320 | 23, 84, 318, 319 | syl3anc 1370 |
. 2
⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (𝑇‘𝑞) = (𝑆‘𝑞)) |
321 | 5, 18, 320 | eqfnfvd 6921 |
1
⊢ (𝜑 → 𝑇 = 𝑆) |