Step | Hyp | Ref
| Expression |
1 | | psgnunilem4.w1 |
. 2
⊢ (𝜑 → 𝑊 ∈ Word 𝑇) |
2 | | psgnunilem4.w2 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) |
3 | | wrdfin 13178 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑇 → 𝑊 ∈ Fin) |
4 | | hashcl 13009 |
. . . . 5
⊢ (𝑊 ∈ Fin →
(#‘𝑊) ∈
ℕ0) |
5 | 1, 3, 4 | 3syl 18 |
. . . 4
⊢ (𝜑 → (#‘𝑊) ∈
ℕ0) |
6 | | nn0uz 11598 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
7 | 5, 6 | syl6eleq 2698 |
. . 3
⊢ (𝜑 → (#‘𝑊) ∈
(ℤ≥‘0)) |
8 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (#‘𝑤) =
(#‘∅)) |
9 | | hash0 13019 |
. . . . . . . . 9
⊢
(#‘∅) = 0 |
10 | 8, 9 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (#‘𝑤) = 0) |
11 | 10 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑤 = ∅ →
(-1↑(#‘𝑤)) =
(-1↑0)) |
12 | | neg1cn 11001 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
13 | | exp0 12726 |
. . . . . . . 8
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
14 | 12, 13 | ax-mp 5 |
. . . . . . 7
⊢
(-1↑0) = 1 |
15 | 11, 14 | syl6eq 2660 |
. . . . . 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 1057 |
. . . . . . . . . . . . . 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 1109 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ∈ Word 𝑇) |
23 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (#‘𝑤) = (#‘𝑤)) |
24 | | wrdfin 13178 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Word 𝑇 → 𝑤 ∈ Fin) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ∈ Fin) |
26 | | simpl2 1058 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → 𝑤 ≠ ∅) |
27 | | hashnncl 13018 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ Fin →
((#‘𝑤) ∈ ℕ
↔ 𝑤 ≠
∅)) |
28 | 27 | biimpar 501 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ Fin ∧ 𝑤 ≠ ∅) →
(#‘𝑤) ∈
ℕ) |
29 | 25, 26, 28 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (#‘𝑤) ∈
ℕ) |
30 | | simpl3r 1110 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((#‘𝑥) = ((#‘𝑤) − 2) ↔ (#‘𝑦) = ((#‘𝑤) − 2))) |
33 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐺 Σg 𝑥) = (𝐺 Σg 𝑦)) |
34 | 33 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
35 | 32, 34 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((#‘𝑦) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷)))) |
36 | 35 | cbvrexv 3148 |
. . . . . . . . . . . . . . . 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 205 |
. . . . . . . . . . . . . 14
⊢ (¬
∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) → ¬ ∃𝑦 ∈ Word 𝑇((#‘𝑦) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) → ¬ ∃𝑦 ∈ Word 𝑇((#‘𝑦) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))) |
40 | 17, 18, 21, 22, 23, 29, 30, 39 | psgnunilem3 17739 |
. . . . . . . . . . . 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 220 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥 ∈ Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
43 | | df-rex 2902 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
Word 𝑇((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
44 | 42, 43 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → ∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
45 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → 𝑥 ∈ Word 𝑇) |
46 | | simprrr 801 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) |
47 | 45, 46 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
48 | | wrdfin 13178 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Word 𝑇 → 𝑥 ∈ Fin) |
49 | | hashcl 13009 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ Fin →
(#‘𝑥) ∈
ℕ0) |
50 | 45, 48, 49 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (#‘𝑥) ∈
ℕ0) |
51 | | simp3l 1082 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ∈ Word 𝑇) |
52 | 51, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ∈ Fin) |
53 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → 𝑤 ≠ ∅) |
54 | 52, 53, 28 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (#‘𝑤) ∈
ℕ) |
55 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (#‘𝑤) ∈
ℕ) |
56 | | simprrl 800 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (#‘𝑥) = ((#‘𝑤) − 2)) |
57 | 55 | nnred 10912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (#‘𝑤) ∈
ℝ) |
58 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
59 | | ltsubrp 11742 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑤) ∈
ℝ ∧ 2 ∈ ℝ+) → ((#‘𝑤) − 2) < (#‘𝑤)) |
60 | 57, 58, 59 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → ((#‘𝑤) − 2) < (#‘𝑤)) |
61 | 56, 60 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (#‘𝑥) < (#‘𝑤)) |
62 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑥) ∈
(0..^(#‘𝑤)) ↔
((#‘𝑥) ∈
ℕ0 ∧ (#‘𝑤) ∈ ℕ ∧ (#‘𝑥) < (#‘𝑤))) |
63 | 50, 55, 61, 62 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . 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 86 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) → ((#‘𝑥) ∈ (0..^(#‘𝑤)) → (((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) = 1))
→ (-1↑(#‘𝑥)) = 1))) |
66 | 47, 63, 65 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) = 1))
→ (-1↑(#‘𝑥)) = 1)) |
67 | 56 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 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 11003 |
. . . . . . . . . . . . . . . . . . 19
⊢ -1 ≠
0 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → -1 ≠
0) |
71 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → 2 ∈
ℤ) |
73 | 55 | nnzd 11357 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) → (#‘𝑤) ∈
ℤ) |
74 | 68, 70, 72, 73 | expsubd 12881 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑((#‘𝑤)
− 2)) = ((-1↑(#‘𝑤)) / (-1↑2))) |
75 | | neg1sqe1 12821 |
. . . . . . . . . . . . . . . . . . 19
⊢
(-1↑2) = 1 |
76 | 75 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . 18
⊢
((-1↑(#‘𝑤)) / (-1↑2)) = ((-1↑(#‘𝑤)) / 1) |
77 | | m1expcl 12745 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑤) ∈
ℤ → (-1↑(#‘𝑤)) ∈ ℤ) |
78 | 77 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑤) ∈
ℤ → (-1↑(#‘𝑤)) ∈ ℂ) |
79 | 73, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(#‘𝑤))
∈ ℂ) |
80 | 79 | div1d 10672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(#‘𝑤)) / 1)
= (-1↑(#‘𝑤))) |
81 | 76, 80 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(#‘𝑤)) /
(-1↑2)) = (-1↑(#‘𝑤))) |
82 | 67, 74, 81 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
(-1↑(#‘𝑥)) =
(-1↑(#‘𝑤))) |
83 | 82 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) ∧ (𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) →
((-1↑(#‘𝑥)) = 1
↔ (-1↑(#‘𝑤)) = 1)) |
84 | 66, 83 | sylibd 228 |
. . . . . . . . . . . . . 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 84 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) = 1))
→ ((𝑥 ∈ Word
𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(#‘𝑤)) =
1))) |
87 | 86 | alimdv 1832 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) = 1))
→ ∀𝑥((𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(#‘𝑤)) =
1))) |
88 | | 19.23v 1889 |
. . . . . . . . . . 11
⊢
(∀𝑥((𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(#‘𝑤)) = 1)
↔ (∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(#‘𝑤)) =
1)) |
89 | 87, 88 | syl6ib 240 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) = 1))
→ (∃𝑥(𝑥 ∈ Word 𝑇 ∧ ((#‘𝑥) = ((#‘𝑤) − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) →
(-1↑(#‘𝑤)) =
1))) |
90 | 44, 89 | mpid 43 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷))) → (∀𝑥((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) = 1))
→ (-1↑(#‘𝑤)) = 1)) |
91 | 90 | 3exp 1256 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ≠ ∅ → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) → (∀𝑥((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) = 1))
→ (-1↑(#‘𝑤)) = 1)))) |
92 | 91 | com34 89 |
. . . . . . 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 2865 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) =
1))) → ((𝑤 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑤)) =
1)) |
96 | 95 | 3adant2 1073 |
. . 3
⊢ ((𝜑 ∧ (#‘𝑤) ∈ (0...(#‘𝑊)) ∧ ∀𝑥((#‘𝑥) ∈ (0..^(#‘𝑤)) → ((𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) =
1))) → ((𝑤 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑤)) =
1)) |
97 | | eleq1 2676 |
. . . . 5
⊢ (𝑤 = 𝑥 → (𝑤 ∈ Word 𝑇 ↔ 𝑥 ∈ Word 𝑇)) |
98 | | oveq2 6557 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑥)) |
99 | 98 | eqeq1d 2612 |
. . . . 5
⊢ (𝑤 = 𝑥 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) |
100 | 97, 99 | anbi12d 743 |
. . . 4
⊢ (𝑤 = 𝑥 → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) ↔ (𝑥 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))) |
101 | | fveq2 6103 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (#‘𝑤) = (#‘𝑥)) |
102 | 101 | oveq2d 6565 |
. . . . 5
⊢ (𝑤 = 𝑥 → (-1↑(#‘𝑤)) = (-1↑(#‘𝑥))) |
103 | 102 | eqeq1d 2612 |
. . . 4
⊢ (𝑤 = 𝑥 → ((-1↑(#‘𝑤)) = 1 ↔ (-1↑(#‘𝑥)) = 1)) |
104 | 100, 103 | imbi12d 333 |
. . 3
⊢ (𝑤 = 𝑥 → (((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑤)) = 1)
↔ ((𝑥 ∈ Word
𝑇 ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑥)) =
1))) |
105 | | eleq1 2676 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑤 ∈ Word 𝑇 ↔ 𝑊 ∈ Word 𝑇)) |
106 | | oveq2 6557 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑊)) |
107 | 106 | eqeq1d 2612 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑊) = ( I ↾ 𝐷))) |
108 | 105, 107 | anbi12d 743 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝑤 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑤) = ( I ↾ 𝐷)) ↔ (𝑊 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)))) |
109 | | fveq2 6103 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (#‘𝑤) = (#‘𝑊)) |
110 | 109 | oveq2d 6565 |
. . . . 5
⊢ (𝑤 = 𝑊 → (-1↑(#‘𝑤)) = (-1↑(#‘𝑊))) |
111 | 110 | eqeq1d 2612 |
. . . 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 12643 |
. 2
⊢ (𝜑 → ((𝑊 ∈ Word 𝑇 ∧ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) →
(-1↑(#‘𝑊)) =
1)) |
114 | 1, 2, 113 | mp2and 711 |
1
⊢ (𝜑 → (-1↑(#‘𝑊)) = 1) |