Step | Hyp | Ref
| Expression |
1 | | psgnunilem4.w1 |
. 2
⊢ (𝜑 → 𝑊 ∈ Word 𝑇) |
2 | | psgnunilem4.w2 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) |
3 | | wrdfin 13509 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑇 → 𝑊 ∈ Fin) |
4 | | hashcl 13339 |
. . . . 5
⊢ (𝑊 ∈ Fin →
(♯‘𝑊) ∈
ℕ0) |
5 | 1, 3, 4 | 3syl 18 |
. . . 4
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
6 | | nn0uz 11915 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
7 | 5, 6 | syl6eleq 2849 |
. . 3
⊢ (𝜑 → (♯‘𝑊) ∈
(ℤ≥‘0)) |
8 | | fveq2 6352 |
. . . . . . . . 9
⊢ (𝑤 = ∅ →
(♯‘𝑤) =
(♯‘∅)) |
9 | | hash0 13350 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
10 | 8, 9 | syl6eq 2810 |
. . . . . . . 8
⊢ (𝑤 = ∅ →
(♯‘𝑤) =
0) |
11 | 10 | oveq2d 6829 |
. . . . . . 7
⊢ (𝑤 = ∅ →
(-1↑(♯‘𝑤))
= (-1↑0)) |
12 | | neg1cn 11316 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
13 | | exp0 13058 |
. . . . . . . 8
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
14 | 12, 13 | ax-mp 5 |
. . . . . . 7
⊢
(-1↑0) = 1 |
15 | 11, 14 | syl6eq 2810 |
. . . . . 6
⊢ (𝑤 = ∅ →
(-1↑(♯‘𝑤))
= 1) |
16 | 15 | 2a1d 26 |
. . . . 5
⊢ (𝑤 = ∅ → ((𝜑 ∧ ∀𝑥((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1))) |
17 | | psgnunilem4.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (SymGrp‘𝐷) |
18 | | psgnunilem4.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = ran (pmTrsp‘𝐷) |
19 | | simpl1 1228 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝜑) |
20 | | psgnunilem4.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝐷 ∈ 𝑉) |
22 | | simpl3l 1287 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ∈ Word 𝑇) |
23 | | eqidd 2761 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (♯‘𝑤) = (♯‘𝑤)) |
24 | | wrdfin 13509 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Word 𝑇 → 𝑤 ∈ Fin) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ∈ Fin) |
26 | | simpl2 1230 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ≠ ∅) |
27 | | hashnncl 13349 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Fin →
((♯‘𝑤) ∈
ℕ ↔ 𝑤 ≠
∅)) |
28 | 27 | biimpar 503 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Fin ∧ 𝑤 ≠ ∅) →
(♯‘𝑤) ∈
ℕ) |
29 | 25, 26, 28 | syl2anc 696 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (♯‘𝑤) ∈
ℕ) |
30 | | simpl3r 1289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) |
31 | | fveq2 6352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
32 | 31 | eqeq1d 2762 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) = ((♯‘𝑤) − 2) ↔ (♯‘𝑦) = ((♯‘𝑤) − 2))) |
33 | | oveq2 6821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐺 Σg 𝑥) = (𝐺 Σg 𝑦)) |
34 | 33 | eqeq1d 2762 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
35 | 32, 34 | anbi12d 749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑦) = ( I ↾ 𝐷)))) |
36 | 35 | cbvrexv 3311 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥 ∈
Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) ↔ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
37 | 36 | notbii 309 |
. . . . . . . . . . . . . . 15
⊢ (¬
∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) ↔ ¬ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
38 | 37 | biimpi 206 |
. . . . . . . . . . . . . 14
⊢ (¬
∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) → ¬ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
39 | 38 | adantl 473 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → ¬ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
40 | 17, 18, 21, 22, 23, 29, 30, 39 | psgnunilem3 18116 |
. . . . . . . . . . . 12
⊢ ¬
((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
41 | | iman 439 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) ↔ ¬ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
42 | 40, 41 | mpbir 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
43 | | df-rex 3056 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) ↔ ∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
44 | 42, 43 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
45 | | simprl 811 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → 𝑥 ∈ Word 𝑇) |
46 | | simprrr 824 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) |
47 | 45, 46 | jca 555 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
48 | | wrdfin 13509 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Word 𝑇 → 𝑥 ∈ Fin) |
49 | | hashcl 13339 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) |
50 | 45, 48, 49 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) ∈
ℕ0) |
51 | | simp3l 1244 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ∈ Word 𝑇) |
52 | 51, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ∈ Fin) |
53 | | simp2 1132 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ≠ ∅) |
54 | 52, 53, 28 | syl2anc 696 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (♯‘𝑤) ∈
ℕ) |
55 | 54 | adantr 472 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑤) ∈
ℕ) |
56 | | simprrl 823 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) = ((♯‘𝑤) − 2)) |
57 | 55 | nnred 11227 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑤) ∈
ℝ) |
58 | | 2rp 12030 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
59 | | ltsubrp 12059 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑤)
∈ ℝ ∧ 2 ∈ ℝ+) → ((♯‘𝑤) − 2) <
(♯‘𝑤)) |
60 | 57, 58, 59 | sylancl 697 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((♯‘𝑤) −
2) < (♯‘𝑤)) |
61 | 56, 60 | eqbrtrd 4826 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) < (♯‘𝑤)) |
62 | | elfzo0 12703 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑥)
∈ (0..^(♯‘𝑤)) ↔ ((♯‘𝑥) ∈ ℕ0 ∧
(♯‘𝑤) ∈
ℕ ∧ (♯‘𝑥) < (♯‘𝑤))) |
63 | 50, 55, 61, 62 | syl3anbrc 1429 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) ∈
(0..^(♯‘𝑤))) |
64 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑥)
∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) |
65 | 64 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) → ((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ (((♯‘𝑥)
∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑥)) = 1))) |
66 | 47, 63, 65 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑥)) = 1)) |
67 | 56 | oveq2d 6829 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(♯‘𝑥))
= (-1↑((♯‘𝑤) − 2))) |
68 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → -1 ∈
ℂ) |
69 | | neg1ne0 11318 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ≠
0 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → -1 ≠
0) |
71 | | 2z 11601 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → 2 ∈
ℤ) |
73 | 55 | nnzd 11673 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑤) ∈
ℤ) |
74 | 68, 70, 72, 73 | expsubd 13213 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑((♯‘𝑤)
− 2)) = ((-1↑(♯‘𝑤)) / (-1↑2))) |
75 | | neg1sqe1 13153 |
. . . . . . . . . . . . . . . . . . 19
⊢
(-1↑2) = 1 |
76 | 75 | oveq2i 6824 |
. . . . . . . . . . . . . . . . . 18
⊢
((-1↑(♯‘𝑤)) / (-1↑2)) =
((-1↑(♯‘𝑤)) / 1) |
77 | | m1expcl 13077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑤)
∈ ℤ → (-1↑(♯‘𝑤)) ∈ ℤ) |
78 | 77 | zcnd 11675 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑤)
∈ ℤ → (-1↑(♯‘𝑤)) ∈ ℂ) |
79 | 73, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(♯‘𝑤))
∈ ℂ) |
80 | 79 | div1d 10985 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(♯‘𝑤)) / 1) = (-1↑(♯‘𝑤))) |
81 | 76, 80 | syl5eq 2806 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(♯‘𝑤)) / (-1↑2)) =
(-1↑(♯‘𝑤))) |
82 | 67, 74, 81 | 3eqtrd 2798 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(♯‘𝑥))
= (-1↑(♯‘𝑤))) |
83 | 82 | eqeq1d 2762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(♯‘𝑥)) = 1 ↔ (-1↑(♯‘𝑤)) = 1)) |
84 | 66, 83 | sylibd 229 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1)) |
85 | 84 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ((𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1))) |
86 | 85 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((𝑥 ∈
Word 𝑇 ∧
((♯‘𝑥) =
((♯‘𝑤) −
2) ∧ (𝐺
Σg 𝑥) = ( I ↾ 𝐷))) → (-1↑(♯‘𝑤)) = 1))) |
87 | 86 | alimdv 1994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ∀𝑥((𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1))) |
88 | | 19.23v 2020 |
. . . . . . . . . . 11
⊢
(∀𝑥((𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1) ↔ (∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1)) |
89 | 87, 88 | syl6ib 241 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1))) |
90 | 44, 89 | mpid 44 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1)) |
91 | 90 | 3exp 1113 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ≠ ∅ → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1)))) |
92 | 91 | com34 91 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ≠ ∅ → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)))) |
93 | 92 | com12 32 |
. . . . . 6
⊢ (𝑤 ≠ ∅ → (𝜑 → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)))) |
94 | 93 | impd 446 |
. . . . 5
⊢ (𝑤 ≠ ∅ → ((𝜑 ∧ ∀𝑥((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1))) |
95 | 16, 94 | pm2.61ine 3015 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)) |
96 | 95 | 3adant2 1126 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑤) ∈
(0...(♯‘𝑊))
∧ ∀𝑥((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)) |
97 | | eleq1 2827 |
. . . . 5
⊢ (𝑤 = 𝑥 → (𝑤 ∈ Word 𝑇 ↔ 𝑥 ∈ Word 𝑇)) |
98 | | oveq2 6821 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑥)) |
99 | 98 | eqeq1d 2762 |
. . . . 5
⊢ (𝑤 = 𝑥 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
100 | 97, 99 | anbi12d 749 |
. . . 4
⊢ (𝑤 = 𝑥 → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) ↔ (𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
101 | | fveq2 6352 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (♯‘𝑤) = (♯‘𝑥)) |
102 | 101 | oveq2d 6829 |
. . . . 5
⊢ (𝑤 = 𝑥 → (-1↑(♯‘𝑤)) =
(-1↑(♯‘𝑥))) |
103 | 102 | eqeq1d 2762 |
. . . 4
⊢ (𝑤 = 𝑥 → ((-1↑(♯‘𝑤)) = 1 ↔
(-1↑(♯‘𝑥))
= 1)) |
104 | 100, 103 | imbi12d 333 |
. . 3
⊢ (𝑤 = 𝑥 → (((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1) ↔ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) |
105 | | eleq1 2827 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑤 ∈ Word 𝑇 ↔ 𝑊 ∈ Word 𝑇)) |
106 | | oveq2 6821 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑊)) |
107 | 106 | eqeq1d 2762 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑊) = ( I ↾ 𝐷))) |
108 | 105, 107 | anbi12d 749 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) ↔ (𝑊 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)))) |
109 | | fveq2 6352 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊)) |
110 | 109 | oveq2d 6829 |
. . . . 5
⊢ (𝑤 = 𝑊 → (-1↑(♯‘𝑤)) =
(-1↑(♯‘𝑊))) |
111 | 110 | eqeq1d 2762 |
. . . 4
⊢ (𝑤 = 𝑊 → ((-1↑(♯‘𝑤)) = 1 ↔
(-1↑(♯‘𝑊))
= 1)) |
112 | 108, 111 | imbi12d 333 |
. . 3
⊢ (𝑤 = 𝑊 → (((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1) ↔ ((𝑊 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑊))
= 1))) |
113 | 1, 7, 96, 104, 112, 101, 109 | uzindi 12975 |
. 2
⊢ (𝜑 → ((𝑊 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑊))
= 1)) |
114 | 1, 2, 113 | mp2and 717 |
1
⊢ (𝜑 →
(-1↑(♯‘𝑊))
= 1) |