Step | Hyp | Ref
| Expression |
1 | | psgnunilem4.w1 |
. 2
⊢ (𝜑 → 𝑊 ∈ Word 𝑇) |
2 | | psgnunilem4.w2 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) |
3 | | wrdfin 14087 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑇 → 𝑊 ∈ Fin) |
4 | | hashcl 13923 |
. . . . 5
⊢ (𝑊 ∈ Fin →
(♯‘𝑊) ∈
ℕ0) |
5 | 1, 3, 4 | 3syl 18 |
. . . 4
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
6 | | nn0uz 12476 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
7 | 5, 6 | eleqtrdi 2848 |
. . 3
⊢ (𝜑 → (♯‘𝑊) ∈
(ℤ≥‘0)) |
8 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑤 = ∅ →
(♯‘𝑤) =
(♯‘∅)) |
9 | | hash0 13934 |
. . . . . . . . 9
⊢
(♯‘∅) = 0 |
10 | 8, 9 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑤 = ∅ →
(♯‘𝑤) =
0) |
11 | 10 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑤 = ∅ →
(-1↑(♯‘𝑤))
= (-1↑0)) |
12 | | neg1cn 11944 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
13 | | exp0 13639 |
. . . . . . . 8
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
14 | 12, 13 | ax-mp 5 |
. . . . . . 7
⊢
(-1↑0) = 1 |
15 | 11, 14 | eqtrdi 2794 |
. . . . . 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 1193 |
. . . . . . . . . . . . . 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 1230 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ∈ Word 𝑇) |
23 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (♯‘𝑤) = (♯‘𝑤)) |
24 | | wrdfin 14087 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Word 𝑇 → 𝑤 ∈ Fin) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ∈ Fin) |
26 | | simpl2 1194 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ≠ ∅) |
27 | | hashnncl 13933 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Fin →
((♯‘𝑤) ∈
ℕ ↔ 𝑤 ≠
∅)) |
28 | 27 | biimpar 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Fin ∧ 𝑤 ≠ ∅) →
(♯‘𝑤) ∈
ℕ) |
29 | 25, 26, 28 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (♯‘𝑤) ∈
ℕ) |
30 | | simpl3r 1231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) |
31 | | fveqeq2 6726 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) = ((♯‘𝑤) − 2) ↔ (♯‘𝑦) = ((♯‘𝑤) − 2))) |
32 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐺 Σg 𝑥) = (𝐺 Σg 𝑦)) |
33 | 32 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
34 | 31, 33 | anbi12d 634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑦) = ( I ↾ 𝐷)))) |
35 | 34 | cbvrexvw 3359 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑥 ∈
Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) ↔ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
36 | 35 | notbii 323 |
. . . . . . . . . . . . . . 15
⊢ (¬
∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) ↔ ¬ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
37 | 36 | biimpi 219 |
. . . . . . . . . . . . . 14
⊢ (¬
∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) → ¬ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
38 | 37 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → ¬ ∃𝑦 ∈ Word 𝑇((♯‘𝑦) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
39 | 17, 18, 21, 22, 23, 29, 30, 38 | psgnunilem3 18888 |
. . . . . . . . . . . 12
⊢ ¬
((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
40 | | iman 405 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) ↔ ¬ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
41 | 39, 40 | mpbir 234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
42 | | df-rex 3067 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
Word 𝑇((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg
𝑥) = ( I ↾ 𝐷)) ↔ ∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
43 | 41, 42 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
44 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → 𝑥 ∈ Word 𝑇) |
45 | | simprrr 782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) |
46 | 44, 45 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
47 | | wrdfin 14087 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Word 𝑇 → 𝑥 ∈ Fin) |
48 | | hashcl 13923 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Fin →
(♯‘𝑥) ∈
ℕ0) |
49 | 44, 47, 48 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) ∈
ℕ0) |
50 | | simp3l 1203 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ∈ Word 𝑇) |
51 | 50, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ∈ Fin) |
52 | | simp2 1139 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ≠ ∅) |
53 | 51, 52, 28 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (♯‘𝑤) ∈
ℕ) |
54 | 53 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑤) ∈
ℕ) |
55 | | simprrl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) = ((♯‘𝑤) − 2)) |
56 | 54 | nnred 11845 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑤) ∈
ℝ) |
57 | | 2rp 12591 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
58 | | ltsubrp 12622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑤)
∈ ℝ ∧ 2 ∈ ℝ+) → ((♯‘𝑤) − 2) <
(♯‘𝑤)) |
59 | 56, 57, 58 | sylancl 589 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((♯‘𝑤) −
2) < (♯‘𝑤)) |
60 | 55, 59 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) < (♯‘𝑤)) |
61 | | elfzo0 13283 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑥)
∈ (0..^(♯‘𝑤)) ↔ ((♯‘𝑥) ∈ ℕ0 ∧
(♯‘𝑤) ∈
ℕ ∧ (♯‘𝑥) < (♯‘𝑤))) |
62 | 49, 54, 60, 61 | syl3anbrc 1345 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑥) ∈
(0..^(♯‘𝑤))) |
63 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑥)
∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) |
64 | 63 | com13 88 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) → ((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ (((♯‘𝑥)
∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑥)) = 1))) |
65 | 46, 62, 64 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑥)) = 1)) |
66 | 55 | oveq2d 7229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(♯‘𝑥))
= (-1↑((♯‘𝑤) − 2))) |
67 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → -1 ∈
ℂ) |
68 | | neg1ne0 11946 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ≠
0 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → -1 ≠
0) |
70 | | 2z 12209 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → 2 ∈
ℤ) |
72 | 54 | nnzd 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (♯‘𝑤) ∈
ℤ) |
73 | 67, 69, 71, 72 | expsubd 13727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑((♯‘𝑤)
− 2)) = ((-1↑(♯‘𝑤)) / (-1↑2))) |
74 | | neg1sqe1 13765 |
. . . . . . . . . . . . . . . . . . 19
⊢
(-1↑2) = 1 |
75 | 74 | oveq2i 7224 |
. . . . . . . . . . . . . . . . . 18
⊢
((-1↑(♯‘𝑤)) / (-1↑2)) =
((-1↑(♯‘𝑤)) / 1) |
76 | | m1expcl 13658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑤)
∈ ℤ → (-1↑(♯‘𝑤)) ∈ ℤ) |
77 | 76 | zcnd 12283 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑤)
∈ ℤ → (-1↑(♯‘𝑤)) ∈ ℂ) |
78 | 72, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(♯‘𝑤))
∈ ℂ) |
79 | 78 | div1d 11600 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(♯‘𝑤)) / 1) = (-1↑(♯‘𝑤))) |
80 | 75, 79 | syl5eq 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(♯‘𝑤)) / (-1↑2)) =
(-1↑(♯‘𝑤))) |
81 | 66, 73, 80 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(♯‘𝑥))
= (-1↑(♯‘𝑤))) |
82 | 81 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(♯‘𝑥)) = 1 ↔ (-1↑(♯‘𝑤)) = 1)) |
83 | 65, 82 | sylibd 242 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1)) |
84 | 83 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ((𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1))) |
85 | 84 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) →
(((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((𝑥 ∈
Word 𝑇 ∧
((♯‘𝑥) =
((♯‘𝑤) −
2) ∧ (𝐺
Σg 𝑥) = ( I ↾ 𝐷))) → (-1↑(♯‘𝑤)) = 1))) |
86 | 85 | alimdv 1924 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ∀𝑥((𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1))) |
87 | | 19.23v 1950 |
. . . . . . . . . . 11
⊢
(∀𝑥((𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1) ↔ (∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1)) |
88 | 86, 87 | syl6ib 254 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((♯‘𝑥) = ((♯‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(♯‘𝑤))
= 1))) |
89 | 43, 88 | mpid 44 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1)) |
90 | 89 | 3exp 1121 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ≠ ∅ → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → (-1↑(♯‘𝑤)) = 1)))) |
91 | 90 | com34 91 |
. . . . . . 7
⊢ (𝜑 → (𝑤 ≠ ∅ → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)))) |
92 | 91 | com12 32 |
. . . . . 6
⊢ (𝑤 ≠ ∅ → (𝜑 → (∀𝑥((♯‘𝑥) ∈
(0..^(♯‘𝑤))
→ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1)) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)))) |
93 | 92 | impd 414 |
. . . . 5
⊢ (𝑤 ≠ ∅ → ((𝜑 ∧ ∀𝑥((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1))) |
94 | 16, 93 | pm2.61ine 3025 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)) |
95 | 94 | 3adant2 1133 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑤) ∈
(0...(♯‘𝑊))
∧ ∀𝑥((♯‘𝑥) ∈ (0..^(♯‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) → ((𝑤 ∈
Word 𝑇 ∧ (𝐺 Σg
𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1)) |
96 | | eleq1 2825 |
. . . . 5
⊢ (𝑤 = 𝑥 → (𝑤 ∈ Word 𝑇 ↔ 𝑥 ∈ Word 𝑇)) |
97 | | oveq2 7221 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑥)) |
98 | 97 | eqeq1d 2739 |
. . . . 5
⊢ (𝑤 = 𝑥 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
99 | 96, 98 | anbi12d 634 |
. . . 4
⊢ (𝑤 = 𝑥 → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) ↔ (𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
100 | | fveq2 6717 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (♯‘𝑤) = (♯‘𝑥)) |
101 | 100 | oveq2d 7229 |
. . . . 5
⊢ (𝑤 = 𝑥 → (-1↑(♯‘𝑤)) =
(-1↑(♯‘𝑥))) |
102 | 101 | eqeq1d 2739 |
. . . 4
⊢ (𝑤 = 𝑥 → ((-1↑(♯‘𝑤)) = 1 ↔
(-1↑(♯‘𝑥))
= 1)) |
103 | 99, 102 | imbi12d 348 |
. . 3
⊢ (𝑤 = 𝑥 → (((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1) ↔ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑥))
= 1))) |
104 | | eleq1 2825 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑤 ∈ Word 𝑇 ↔ 𝑊 ∈ Word 𝑇)) |
105 | | oveq2 7221 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑊)) |
106 | 105 | eqeq1d 2739 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑊) = ( I ↾ 𝐷))) |
107 | 104, 106 | anbi12d 634 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) ↔ (𝑊 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)))) |
108 | | fveq2 6717 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (♯‘𝑤) = (♯‘𝑊)) |
109 | 108 | oveq2d 7229 |
. . . . 5
⊢ (𝑤 = 𝑊 → (-1↑(♯‘𝑤)) =
(-1↑(♯‘𝑊))) |
110 | 109 | eqeq1d 2739 |
. . . 4
⊢ (𝑤 = 𝑊 → ((-1↑(♯‘𝑤)) = 1 ↔
(-1↑(♯‘𝑊))
= 1)) |
111 | 107, 110 | imbi12d 348 |
. . 3
⊢ (𝑤 = 𝑊 → (((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑤))
= 1) ↔ ((𝑊 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑊))
= 1))) |
112 | 1, 7, 95, 103, 111, 100, 108 | uzindi 13555 |
. 2
⊢ (𝜑 → ((𝑊 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) →
(-1↑(♯‘𝑊))
= 1)) |
113 | 1, 2, 112 | mp2and 699 |
1
⊢ (𝜑 →
(-1↑(♯‘𝑊))
= 1) |