Proof of Theorem clwlkclwwlklem2a4
Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝐼 = ((#‘𝑃) − 2) → (𝐹‘𝐼) = (𝐹‘((#‘𝑃) − 2))) |
2 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
3 | | clwlkclwwlklem2.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) |
4 | 3 | clwlkisclwwlklem2fv2 26311 |
. . . . . . . . . . 11
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (𝐹‘((#‘𝑃) − 2)) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
5 | 2, 4 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝐹‘((#‘𝑃) − 2)) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
6 | 1, 5 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐼 = ((#‘𝑃) − 2)) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
7 | 6 | ex 449 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝐼 = ((#‘𝑃) − 2) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}))) |
8 | 7 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝐼 = ((#‘𝑃) − 2) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}))) |
9 | 8 | ad2antrr 758 |
. . . . . 6
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) → (𝐼 = ((#‘𝑃) − 2) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}))) |
10 | 9 | impcom 445 |
. . . . 5
⊢ ((𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
11 | 10 | fveq2d 6107 |
. . . 4
⊢ ((𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐸‘(𝐹‘𝐼)) = (𝐸‘(◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}))) |
12 | | f1f1orn 6061 |
. . . . . . 7
⊢ (𝐸:dom 𝐸–1-1→𝑅 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
13 | 12 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
14 | 13 | ad2antrr 758 |
. . . . 5
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
15 | | lsw 13204 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
16 | 15 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → (( lastS ‘𝑃) = (𝑃‘0) ↔ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘0))) |
17 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℂ) |
18 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) ∈
ℂ → (#‘𝑃)
∈ ℂ) |
19 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) ∈
ℂ → 2 ∈ ℂ) |
20 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) ∈
ℂ → 1 ∈ ℂ) |
21 | 18, 19, 20 | subsubd 10299 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) ∈
ℂ → ((#‘𝑃)
− (2 − 1)) = (((#‘𝑃) − 2) + 1)) |
22 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2
− 1) = 1 |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) ∈
ℂ → (2 − 1) = 1) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) ∈
ℂ → ((#‘𝑃)
− (2 − 1)) = ((#‘𝑃) − 1)) |
25 | 21, 24 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) ∈
ℂ → (((#‘𝑃) − 2) + 1) = ((#‘𝑃) − 1)) |
26 | 2, 17, 25 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Word 𝑉 → (((#‘𝑃) − 2) + 1) = ((#‘𝑃) − 1)) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘0)) → (((#‘𝑃) − 2) + 1) =
((#‘𝑃) −
1)) |
28 | 27 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘0)) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘((#‘𝑃) − 1))) |
29 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘((#‘𝑃) − 1)) → ((𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0) ↔ (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘((#‘𝑃) − 1)))) |
30 | 29 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘((#‘𝑃) − 1)) = (𝑃‘0) → ((𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0) ↔ (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘((#‘𝑃) − 1)))) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘0)) → ((𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0) ↔ (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘((#‘𝑃) − 1)))) |
32 | 28, 31 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘0)) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0)) |
33 | 32 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → ((𝑃‘((#‘𝑃) − 1)) = (𝑃‘0) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0))) |
34 | 16, 33 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → (( lastS ‘𝑃) = (𝑃‘0) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0))) |
35 | 34 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (( lastS ‘𝑃) = (𝑃‘0) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0))) |
36 | 35 | com12 32 |
. . . . . . . . . . . . . 14
⊢ (( lastS
‘𝑃) = (𝑃‘0) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0))) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((( lastS
‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0))) |
38 | 37 | impcom 445 |
. . . . . . . . . . . 12
⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0)) |
39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ 𝐼 = ((#‘𝑃) − 2)) → (𝑃‘(((#‘𝑃) − 2) + 1)) = (𝑃‘0)) |
40 | 39 | preq2d 4219 |
. . . . . . . . . 10
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ 𝐼 = ((#‘𝑃) − 2)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) |
41 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝐼 = ((#‘𝑃) − 2) → (𝑃‘𝐼) = (𝑃‘((#‘𝑃) − 2))) |
42 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝐼 = ((#‘𝑃) − 2) → (𝐼 + 1) = (((#‘𝑃) − 2) + 1)) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝐼 = ((#‘𝑃) − 2) → (𝑃‘(𝐼 + 1)) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
44 | 41, 43 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))}) |
45 | 44 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝐼 = ((#‘𝑃) − 2) → ({(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ↔ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
46 | 45 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ 𝐼 = ((#‘𝑃) − 2)) → ({(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ↔ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
47 | 40, 46 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ 𝐼 = ((#‘𝑃) − 2)) → {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) |
48 | 47 | eleq1d 2672 |
. . . . . . . 8
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ 𝐼 = ((#‘𝑃) − 2)) → ({(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) |
49 | 48 | biimpd 218 |
. . . . . . 7
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ 𝐼 = ((#‘𝑃) − 2)) → ({(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸 → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) |
50 | 49 | impancom 455 |
. . . . . 6
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) → (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) |
51 | 50 | impcom 445 |
. . . . 5
⊢ ((𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) |
52 | | f1ocnvfv2 6433 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) |
53 | 14, 51, 52 | syl2an2 871 |
. . . 4
⊢ ((𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐸‘(◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) |
54 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘((#‘𝑃) − 1)) = (𝑃‘0) ↔ (𝑃‘0) = (𝑃‘((#‘𝑃) − 1))) |
55 | 54 | biimpi 205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃‘((#‘𝑃) − 1)) = (𝑃‘0) → (𝑃‘0) = (𝑃‘((#‘𝑃) − 1))) |
56 | | 1e2m1 11013 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 = (2
− 1) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Word 𝑉 → 1 = (2 − 1)) |
58 | 57 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = ((#‘𝑃) − (2 − 1))) |
59 | 2, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℂ) |
60 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Word 𝑉 → 2 ∈ ℂ) |
61 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ) |
62 | 59, 60, 61 | subsubd 10299 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − (2 − 1)) = (((#‘𝑃) − 2) +
1)) |
63 | 58, 62 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = (((#‘𝑃) − 2) + 1)) |
64 | 63 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → (𝑃‘((#‘𝑃) − 1)) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
65 | 55, 64 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Word 𝑉 ∧ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘0)) → (𝑃‘0) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
66 | 65 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → ((𝑃‘((#‘𝑃) − 1)) = (𝑃‘0) → (𝑃‘0) = (𝑃‘(((#‘𝑃) − 2) + 1)))) |
67 | 16, 66 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word 𝑉 → (( lastS ‘𝑃) = (𝑃‘0) → (𝑃‘0) = (𝑃‘(((#‘𝑃) − 2) + 1)))) |
68 | 67 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ Word 𝑉 ∧ ( lastS ‘𝑃) = (𝑃‘0)) → (𝑃‘0) = (𝑃‘(((#‘𝑃) − 2) + 1))) |
69 | 68 | preq2d 4219 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ ( lastS ‘𝑃) = (𝑃‘0)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))}) |
70 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ ( lastS ‘𝑃) = (𝑃‘0)) ∧ 𝐼 = ((#‘𝑃) − 2)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))}) |
71 | 44 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ ( lastS ‘𝑃) = (𝑃‘0)) ∧ 𝐼 = ((#‘𝑃) − 2)) → {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘(((#‘𝑃) − 2) + 1))}) |
72 | 70, 71 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (((𝑃 ∈ Word 𝑉 ∧ ( lastS ‘𝑃) = (𝑃‘0)) ∧ 𝐼 = ((#‘𝑃) − 2)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
73 | 72 | exp31 628 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → (( lastS ‘𝑃) = (𝑃‘0) → (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) |
74 | 73 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (( lastS ‘𝑃) = (𝑃‘0) → (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) |
75 | 74 | com12 32 |
. . . . . . . 8
⊢ (( lastS
‘𝑃) = (𝑃‘0) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) |
76 | 75 | adantr 480 |
. . . . . . 7
⊢ ((( lastS
‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) |
77 | 76 | impcom 445 |
. . . . . 6
⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) → (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |
78 | 77 | adantr 480 |
. . . . 5
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) → (𝐼 = ((#‘𝑃) − 2) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |
79 | 78 | impcom 445 |
. . . 4
⊢ ((𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
80 | 11, 53, 79 | 3eqtrd 2648 |
. . 3
⊢ ((𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐸‘(𝐹‘𝐼)) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
81 | | simpll 786 |
. . . . . . . . . . . . . . . . 17
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2))) → (#‘𝑃) ∈
ℕ0) |
82 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑃) = 2
→ ((#‘𝑃) −
1) = (2 − 1)) |
83 | 82, 22 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) = 2
→ ((#‘𝑃) −
1) = 1) |
84 | 83 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) = 2
→ (0..^((#‘𝑃)
− 1)) = (0..^1)) |
85 | 84 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) = 2
→ (𝐼 ∈
(0..^((#‘𝑃) −
1)) ↔ 𝐼 ∈
(0..^1))) |
86 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑃) = 2
→ ((#‘𝑃) −
2) = (2 − 2)) |
87 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℂ |
88 | 87 | subidi 10231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2
− 2) = 0 |
89 | 86, 88 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) = 2
→ ((#‘𝑃) −
2) = 0) |
90 | 89 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) = 2
→ (𝐼 = ((#‘𝑃) − 2) ↔ 𝐼 = 0)) |
91 | 90 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) = 2
→ (¬ 𝐼 =
((#‘𝑃) − 2)
↔ ¬ 𝐼 =
0)) |
92 | 85, 91 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑃) = 2
→ ((𝐼 ∈
(0..^((#‘𝑃) −
1)) ∧ ¬ 𝐼 =
((#‘𝑃) − 2))
↔ (𝐼 ∈ (0..^1)
∧ ¬ 𝐼 =
0))) |
93 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐼 ∈ {0} → 𝐼 = 0) |
94 | 93 | pm2.24d 146 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐼 ∈ {0} → (¬ 𝐼 = 0 → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))) |
95 | | fzo01 12417 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0..^1) =
{0} |
96 | 94, 95 | eleq2s 2706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ (0..^1) → (¬
𝐼 = 0 → (𝐼 ∈ ℕ0
∧ ((#‘𝑃) −
2) ∈ ℕ ∧ 𝐼
< ((#‘𝑃) −
2)))) |
97 | 96 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ (0..^1) ∧ ¬
𝐼 = 0) → (𝐼 ∈ ℕ0
∧ ((#‘𝑃) −
2) ∈ ℕ ∧ 𝐼
< ((#‘𝑃) −
2))) |
98 | 92, 97 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑃) = 2
→ ((𝐼 ∈
(0..^((#‘𝑃) −
1)) ∧ ¬ 𝐼 =
((#‘𝑃) − 2))
→ (𝐼 ∈
ℕ0 ∧ ((#‘𝑃) − 2) ∈ ℕ ∧ 𝐼 < ((#‘𝑃) − 2)))) |
99 | 98 | adantld 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) = 2
→ ((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2))) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))) |
100 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) ≠ 2
↔ ¬ (#‘𝑃) =
2) |
101 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 ∈
ℝ |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → 2 ∈ ℝ) |
103 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℝ) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (#‘𝑃) ∈ ℝ) |
105 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → 2 ≤ (#‘𝑃)) |
106 | 102, 104,
105 | leltned 10069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (2 < (#‘𝑃) ↔ (#‘𝑃) ≠ 2)) |
107 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ↔ (𝐼 ∈ ℕ0
∧ ((#‘𝑃) −
1) ∈ ℕ ∧ 𝐼
< ((#‘𝑃) −
1))) |
108 | | simp-4l 802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝐼 ∈
ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧ ¬
𝐼 = ((#‘𝑃) − 2)) ∧ 2 <
(#‘𝑃)) ∧ 𝐼 < ((#‘𝑃) − 1)) → 𝐼 ∈
ℕ0) |
109 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℤ) |
110 | | 2z 11286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 2 ∈
ℤ |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℤ) |
112 | 109, 111 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 2) ∈
ℤ) |
113 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 < (#‘𝑃)) → ((#‘𝑃) − 2) ∈
ℤ) |
114 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℝ) |
115 | 114, 103 | posdifd 10493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝑃) ∈
ℕ0 → (2 < (#‘𝑃) ↔ 0 < ((#‘𝑃) − 2))) |
116 | 115 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 < (#‘𝑃)) → 0 < ((#‘𝑃) − 2)) |
117 | | elnnz 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝑃)
− 2) ∈ ℕ ↔ (((#‘𝑃) − 2) ∈ ℤ ∧ 0 <
((#‘𝑃) −
2))) |
118 | 113, 116,
117 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 < (#‘𝑃)) → ((#‘𝑃) − 2) ∈
ℕ) |
119 | 118 | ad5ant24 1297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝐼 ∈
ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧ ¬
𝐼 = ((#‘𝑃) − 2)) ∧ 2 <
(#‘𝑃)) ∧ 𝐼 < ((#‘𝑃) − 1)) →
((#‘𝑃) − 2)
∈ ℕ) |
120 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℤ) |
121 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((#‘𝑃) ∈
ℤ → ((#‘𝑃)
− 1) ∈ ℤ) |
122 | 109, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) ∈
ℤ) |
123 | | zltlem1 11307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐼 ∈ ℤ ∧
((#‘𝑃) − 1)
∈ ℤ) → (𝐼
< ((#‘𝑃) −
1) ↔ 𝐼 ≤
(((#‘𝑃) − 1)
− 1))) |
124 | 120, 122,
123 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝐼 < ((#‘𝑃) − 1) ↔ 𝐼 ≤ (((#‘𝑃) − 1) − 1))) |
125 | 17 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (#‘𝑃) ∈ ℂ) |
126 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → 1 ∈ ℂ) |
127 | 125, 126,
126 | subsub4d 10302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (((#‘𝑃) − 1) − 1) = ((#‘𝑃) − (1 +
1))) |
128 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (1 + 1) =
2 |
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (1 + 1) = 2) |
130 | 129 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → ((#‘𝑃) − (1 + 1)) = ((#‘𝑃) − 2)) |
131 | 127, 130 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (((#‘𝑃) − 1) − 1) = ((#‘𝑃) − 2)) |
132 | 131 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝐼 ≤ (((#‘𝑃) − 1) − 1) ↔ 𝐼 ≤ ((#‘𝑃) − 2))) |
133 | 124, 132 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝐼 < ((#‘𝑃) − 1) ↔ 𝐼 ≤ ((#‘𝑃) − 2))) |
134 | | necom 2835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((#‘𝑃)
− 2) ≠ 𝐼 ↔
𝐼 ≠ ((#‘𝑃) − 2)) |
135 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝐼 ≠ ((#‘𝑃) − 2) ↔ ¬ 𝐼 = ((#‘𝑃) − 2)) |
136 | 134, 135 | bitr2i 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (¬
𝐼 = ((#‘𝑃) − 2) ↔
((#‘𝑃) − 2)
≠ 𝐼) |
137 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℝ) |
138 | 137 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ 𝐼 ≤ ((#‘𝑃) − 2)) → 𝐼 ∈ ℝ) |
139 | 103, 114 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 2) ∈
ℝ) |
140 | 139 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ 𝐼 ≤ ((#‘𝑃) − 2)) → ((#‘𝑃) − 2) ∈
ℝ) |
141 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ 𝐼 ≤ ((#‘𝑃) − 2)) → 𝐼 ≤ ((#‘𝑃) − 2)) |
142 | | leltne 10006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝐼 ∈ ℝ ∧
((#‘𝑃) − 2)
∈ ℝ ∧ 𝐼 ≤
((#‘𝑃) − 2))
→ (𝐼 <
((#‘𝑃) − 2)
↔ ((#‘𝑃) −
2) ≠ 𝐼)) |
143 | 142 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝐼 ∈ ℝ ∧
((#‘𝑃) − 2)
∈ ℝ ∧ 𝐼 ≤
((#‘𝑃) − 2))
→ (((#‘𝑃)
− 2) ≠ 𝐼 ↔
𝐼 < ((#‘𝑃) − 2))) |
144 | 138, 140,
141, 143 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ 𝐼 ≤ ((#‘𝑃) − 2)) → (((#‘𝑃) − 2) ≠ 𝐼 ↔ 𝐼 < ((#‘𝑃) − 2))) |
145 | 144 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ 𝐼 ≤ ((#‘𝑃) − 2)) → (((#‘𝑃) − 2) ≠ 𝐼 → 𝐼 < ((#‘𝑃) − 2))) |
146 | 136, 145 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ 𝐼 ≤ ((#‘𝑃) − 2)) → (¬ 𝐼 = ((#‘𝑃) − 2) → 𝐼 < ((#‘𝑃) − 2))) |
147 | 146 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝐼 ≤ ((#‘𝑃) − 2) → (¬ 𝐼 = ((#‘𝑃) − 2) → 𝐼 < ((#‘𝑃) − 2)))) |
148 | 133, 147 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (𝐼 < ((#‘𝑃) − 1) → (¬ 𝐼 = ((#‘𝑃) − 2) → 𝐼 < ((#‘𝑃) − 2)))) |
149 | 148 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) → (¬ 𝐼 = ((#‘𝑃) − 2) → (𝐼 < ((#‘𝑃) − 1) → 𝐼 < ((#‘𝑃) − 2)))) |
150 | 149 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → (𝐼 < ((#‘𝑃) − 1) → 𝐼 < ((#‘𝑃) − 2))) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) ∧ 2 < (#‘𝑃)) → (𝐼 < ((#‘𝑃) − 1) → 𝐼 < ((#‘𝑃) − 2))) |
152 | 151 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝐼 ∈
ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧ ¬
𝐼 = ((#‘𝑃) − 2)) ∧ 2 <
(#‘𝑃)) ∧ 𝐼 < ((#‘𝑃) − 1)) → 𝐼 < ((#‘𝑃) − 2)) |
153 | 108, 119,
152 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝐼 ∈
ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧ ¬
𝐼 = ((#‘𝑃) − 2)) ∧ 2 <
(#‘𝑃)) ∧ 𝐼 < ((#‘𝑃) − 1)) → (𝐼 ∈ ℕ0
∧ ((#‘𝑃) −
2) ∈ ℕ ∧ 𝐼
< ((#‘𝑃) −
2))) |
154 | 153 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝐼 ∈ ℕ0
∧ (#‘𝑃) ∈
ℕ0) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) ∧ 2 < (#‘𝑃)) → (𝐼 < ((#‘𝑃) − 1) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))) |
155 | 154 | exp41 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐼 ∈ ℕ0
→ ((#‘𝑃) ∈
ℕ0 → (¬ 𝐼 = ((#‘𝑃) − 2) → (2 < (#‘𝑃) → (𝐼 < ((#‘𝑃) − 1) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))))))) |
156 | 155 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐼 ∈ ℕ0
→ (𝐼 <
((#‘𝑃) − 1)
→ (¬ 𝐼 =
((#‘𝑃) − 2)
→ (2 < (#‘𝑃)
→ ((#‘𝑃) ∈
ℕ0 → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))))))) |
157 | 156 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐼 ∈ ℕ0
∧ 𝐼 <
((#‘𝑃) − 1))
→ (¬ 𝐼 =
((#‘𝑃) − 2)
→ (2 < (#‘𝑃)
→ ((#‘𝑃) ∈
ℕ0 → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))))) |
158 | 157 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐼 ∈ ℕ0
∧ ((#‘𝑃) −
1) ∈ ℕ ∧ 𝐼
< ((#‘𝑃) −
1)) → (¬ 𝐼 =
((#‘𝑃) − 2)
→ (2 < (#‘𝑃)
→ ((#‘𝑃) ∈
ℕ0 → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))))) |
159 | 107, 158 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐼 ∈ (0..^((#‘𝑃) − 1)) → (¬
𝐼 = ((#‘𝑃) − 2) → (2 <
(#‘𝑃) →
((#‘𝑃) ∈
ℕ0 → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))))) |
160 | 159 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → (2 < (#‘𝑃) → ((#‘𝑃) ∈ ℕ0
→ (𝐼 ∈
ℕ0 ∧ ((#‘𝑃) − 2) ∈ ℕ ∧ 𝐼 < ((#‘𝑃) −
2))))) |
161 | 160 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑃) ∈
ℕ0 → (2 < (#‘𝑃) → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))))) |
162 | 161 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (2 < (#‘𝑃) → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))))) |
163 | 106, 162 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) ≠ 2 → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))))) |
164 | 100, 163 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (¬ (#‘𝑃) = 2 → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))))) |
165 | 164 | com23 84 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → (¬ (#‘𝑃) = 2 → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))))) |
166 | 165 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2))) → (¬ (#‘𝑃) = 2 → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))) |
167 | 166 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(#‘𝑃) = 2 →
((((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2))) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2)))) |
168 | 99, 167 | pm2.61i 175 |
. . . . . . . . . . . . . . . . . 18
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2))) → (𝐼 ∈ ℕ0 ∧
((#‘𝑃) − 2)
∈ ℕ ∧ 𝐼 <
((#‘𝑃) −
2))) |
169 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (0..^((#‘𝑃) − 2)) ↔ (𝐼 ∈ ℕ0
∧ ((#‘𝑃) −
2) ∈ ℕ ∧ 𝐼
< ((#‘𝑃) −
2))) |
170 | 168, 169 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2))) → 𝐼 ∈ (0..^((#‘𝑃) − 2))) |
171 | 81, 170 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ (𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2))) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2)))) |
172 | 171 | exp31 628 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑃) ∈
ℕ0 → (2 ≤ (#‘𝑃) → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2)))))) |
173 | 2, 172 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (#‘𝑃) → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2)))))) |
174 | 173 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2))))) |
175 | 174 | 3adant1 1072 |
. . . . . . . . . . . 12
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝐼 ∈ (0..^((#‘𝑃) − 1)) ∧ ¬ 𝐼 = ((#‘𝑃) − 2)) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2))))) |
176 | 175 | expd 451 |
. . . . . . . . . . 11
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝐼 ∈ (0..^((#‘𝑃) − 1)) → (¬ 𝐼 = ((#‘𝑃) − 2) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2)))))) |
177 | 176 | com12 32 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (0..^((#‘𝑃) − 1)) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (¬ 𝐼 = ((#‘𝑃) − 2) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2)))))) |
178 | 177 | adantl 481 |
. . . . . . . . 9
⊢ ((( lastS
‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (¬ 𝐼 = ((#‘𝑃) − 2) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2)))))) |
179 | 178 | impcom 445 |
. . . . . . . 8
⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) → (¬ 𝐼 = ((#‘𝑃) − 2) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2))))) |
180 | 179 | adantr 480 |
. . . . . . 7
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) → (¬ 𝐼 = ((#‘𝑃) − 2) → ((#‘𝑃) ∈ ℕ0
∧ 𝐼 ∈
(0..^((#‘𝑃) −
2))))) |
181 | 180 | impcom 445 |
. . . . . 6
⊢ ((¬
𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → ((#‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((#‘𝑃) − 2)))) |
182 | 3 | clwlkisclwwlklem2fv1 26310 |
. . . . . 6
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝐼
∈ (0..^((#‘𝑃)
− 2))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |
183 | 181, 182 | syl 17 |
. . . . 5
⊢ ((¬
𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |
184 | 183 | fveq2d 6107 |
. . . 4
⊢ ((¬
𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐸‘(𝐹‘𝐼)) = (𝐸‘(◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) |
185 | | simprr 792 |
. . . . 5
⊢ ((¬
𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) |
186 | | f1ocnvfv2 6433 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
187 | 14, 185, 186 | syl2an2 871 |
. . . 4
⊢ ((¬
𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐸‘(◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
188 | 184, 187 | eqtrd 2644 |
. . 3
⊢ ((¬
𝐼 = ((#‘𝑃) − 2) ∧ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸)) → (𝐸‘(𝐹‘𝐼)) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
189 | 80, 188 | pm2.61ian 827 |
. 2
⊢ ((((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1)))) ∧ {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝐼)) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
190 | 189 | exp31 628 |
1
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝐼)) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) |