Proof of Theorem clwlkisclwwlklem1
Step | Hyp | Ref
| Expression |
1 | | usgraf1 25889 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸) |
2 | | f1f 6014 |
. . . 4
⊢ (𝐸:dom 𝐸–1-1→ran 𝐸 → 𝐸:dom 𝐸⟶ran 𝐸) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸⟶ran 𝐸) |
4 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈
ℕ0) |
5 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 Fn (0...(#‘𝐹))) |
6 | | fnfz0hash 13087 |
. . . . . . . . . . 11
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑃
Fn (0...(#‘𝐹)))
→ (#‘𝑃) =
((#‘𝐹) +
1)) |
7 | 4, 5, 6 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (#‘𝑃) = ((#‘𝐹) + 1)) |
8 | | ffz0iswrd 13187 |
. . . . . . . . . . . . . 14
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 ∈ Word 𝑉) |
9 | | lsw 13204 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
10 | 9 | ad6antr 768 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
11 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑃) =
((#‘𝐹) + 1) →
((#‘𝑃) − 1) =
(((#‘𝐹) + 1) −
1)) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) =
((#‘𝐹) + 1) →
(𝑃‘((#‘𝑃) − 1)) = (𝑃‘(((#‘𝐹) + 1) −
1))) |
13 | 12 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (𝑃‘((#‘𝑃) − 1)) = (𝑃‘(((#‘𝐹) + 1) − 1))) |
14 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘(#‘𝐹)) = (𝑃‘0)) |
15 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℂ) |
16 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) ∈
ℕ0 → 1 ∈ ℂ) |
17 | 15, 16 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝐹) ∈
ℕ0 → (((#‘𝐹) + 1) − 1) = (#‘𝐹)) |
18 | 17 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) = (((#‘𝐹) + 1) − 1)) |
19 | 18 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (#‘𝐹) = (((#‘𝐹) + 1) − 1)) |
20 | 19 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (𝑃‘(#‘𝐹)) = (𝑃‘(((#‘𝐹) + 1) − 1))) |
21 | 20 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) ↔ (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0))) |
22 | 21 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘(#‘𝐹)) = (𝑃‘0) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0))) |
23 | 14, 22 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0))) |
24 | 23 | adantld 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0))) |
25 | 24 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (𝑃‘(((#‘𝐹) + 1) − 1)) = (𝑃‘0)) |
26 | 10, 13, 25 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ( lastS ‘𝑃) = (𝑃‘0)) |
27 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℤ) |
28 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
ℤ → ((#‘𝐹)
− 1) ∈ ℤ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) − 1) ∈
ℤ) |
30 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℝ) |
31 | 30 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) − 1) ≤ (#‘𝐹)) |
32 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1)) ↔ (((#‘𝐹) − 1) ∈ ℤ
∧ (#‘𝐹) ∈
ℤ ∧ ((#‘𝐹)
− 1) ≤ (#‘𝐹))) |
33 | 29, 27, 31, 32 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1))) |
34 | 33 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1))) |
35 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1)) → (0..^((#‘𝐹) − 1)) ⊆
(0..^(#‘𝐹))) |
36 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((0..^((#‘𝐹)
− 1)) ⊆ (0..^(#‘𝐹)) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
38 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → 𝐸:dom 𝐸⟶ran 𝐸) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → 𝐸:dom 𝐸⟶ran 𝐸) |
40 | | wrdf 13165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
41 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
42 | | fzossrbm1 12366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐹) ∈
ℤ → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
43 | 27, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐹) ∈
ℕ0 → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹))) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) →
(0..^((#‘𝐹) −
1)) ⊆ (0..^(#‘𝐹))) |
45 | 44 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → 𝑖 ∈ (0..^(#‘𝐹))) |
46 | 41, 45 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ (#‘𝐹) ∈ ℕ0) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → (𝐹‘𝑖) ∈ dom 𝐸) |
47 | 46 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → ((#‘𝐹) ∈ ℕ0 → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
48 | 40, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) ∈ ℕ0
→ (𝑖 ∈
(0..^((#‘𝐹) −
1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) → ((#‘𝐹) ∈ ℕ0 → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸))) |
50 | 49 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)) |
51 | 50 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (𝑖 ∈ (0..^((#‘𝐹) − 1)) → (𝐹‘𝑖) ∈ dom 𝐸)) |
52 | 51 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → (𝐹‘𝑖) ∈ dom 𝐸) |
53 | 39, 52 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸) |
54 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = (𝐸‘(𝐹‘𝑖))) |
55 | 54 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = (𝐸‘(𝐹‘𝑖))) |
56 | 55 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘𝑖)) ∈ ran 𝐸)) |
57 | 53, 56 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 ∈ (0..^((#‘𝐹) − 1))) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
58 | 57 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^((#‘𝐹) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
59 | 37, 58 | syld 46 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
60 | 59 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
62 | 61 | impcom 445 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) |
63 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝑃) =
((#‘𝐹) + 1) → (2
≤ (#‘𝑃) ↔ 2
≤ ((#‘𝐹) +
1))) |
64 | 63 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) →
(2 ≤ (#‘𝑃) ↔
2 ≤ ((#‘𝐹) +
1))) |
65 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 2 ∈
ℝ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐹) ∈
ℕ0 → 2 ∈ ℝ) |
67 | | 1red 9934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐹) ∈
ℕ0 → 1 ∈ ℝ) |
68 | 66, 67, 30 | lesubaddd 10503 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐹) ∈
ℕ0 → ((2 − 1) ≤ (#‘𝐹) ↔ 2 ≤ ((#‘𝐹) + 1))) |
69 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (2
− 1) = 1 |
70 | 69 | breq1i 4590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((2
− 1) ≤ (#‘𝐹)
↔ 1 ≤ (#‘𝐹)) |
71 | | elnnnn0c 11215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐹) ∈
ℕ ↔ ((#‘𝐹)
∈ ℕ0 ∧ 1 ≤ (#‘𝐹))) |
72 | 71 | simplbi2 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐹) ∈
ℕ0 → (1 ≤ (#‘𝐹) → (#‘𝐹) ∈ ℕ)) |
73 | 70, 72 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐹) ∈
ℕ0 → ((2 − 1) ≤ (#‘𝐹) → (#‘𝐹) ∈ ℕ)) |
74 | 68, 73 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐹) ∈
ℕ0 → (2 ≤ ((#‘𝐹) + 1) → (#‘𝐹) ∈ ℕ)) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) → (2 ≤
((#‘𝐹) + 1) →
(#‘𝐹) ∈
ℕ)) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) →
(2 ≤ ((#‘𝐹) + 1)
→ (#‘𝐹) ∈
ℕ)) |
77 | 64, 76 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) →
(2 ≤ (#‘𝑃) →
(#‘𝐹) ∈
ℕ)) |
78 | 77 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) →
(#‘𝐹) ∈
ℕ) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (#‘𝐹) ∈ ℕ) |
80 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ∈
(0..^(#‘𝐹)) ↔
(#‘𝐹) ∈
ℕ) |
81 | 79, 80 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → 0 ∈ (0..^(#‘𝐹))) |
82 | | fzoend 12425 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 ∈
(0..^(#‘𝐹)) →
((#‘𝐹) − 1)
∈ (0..^(#‘𝐹))) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) |
84 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = ((#‘𝐹) − 1) → (𝐹‘𝑖) = (𝐹‘((#‘𝐹) − 1))) |
85 | 84 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = ((#‘𝐹) − 1) → (𝐸‘(𝐹‘𝑖)) = (𝐸‘(𝐹‘((#‘𝐹) − 1)))) |
86 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = ((#‘𝐹) − 1) → (𝑃‘𝑖) = (𝑃‘((#‘𝐹) − 1))) |
87 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = ((#‘𝐹) − 1) → (𝑖 + 1) = (((#‘𝐹) − 1) + 1)) |
88 | 87 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 = ((#‘𝐹) − 1) → (𝑃‘(𝑖 + 1)) = (𝑃‘(((#‘𝐹) − 1) + 1))) |
89 | 86, 88 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 = ((#‘𝐹) − 1) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))}) |
90 | 85, 89 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 = ((#‘𝐹) − 1) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))})) |
91 | 90 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ 𝑖 = ((#‘𝐹) − 1)) → ((𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))})) |
92 | 83, 91 | rspcdv 3285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))})) |
93 | 15, 16 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) ∈
ℕ0 → (((#‘𝐹) − 1) + 1) = (#‘𝐹)) |
94 | 93 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (((#‘𝐹) − 1) + 1) = (#‘𝐹)) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (𝑃‘(((#‘𝐹) − 1) + 1)) = (𝑃‘(#‘𝐹))) |
96 | 95 | preq2d 4219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))}) |
97 | 96 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))})) |
98 | 40 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) →
𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
99 | 74 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (2 ≤
((#‘𝐹) + 1) →
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℕ)) |
100 | 63, 99 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑃) =
((#‘𝐹) + 1) → (2
≤ (#‘𝑃) →
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℕ))) |
101 | 100 | com3r 85 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (#‘𝐹) ∈
ℕ))) |
102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) →
((#‘𝑃) =
((#‘𝐹) + 1) → (2
≤ (#‘𝑃) →
(#‘𝐹) ∈
ℕ))) |
103 | 102 | imp31 447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) →
(#‘𝐹) ∈
ℕ) |
104 | 103, 80 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) → 0
∈ (0..^(#‘𝐹))) |
105 | 104, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) →
((#‘𝐹) − 1)
∈ (0..^(#‘𝐹))) |
106 | 98, 105 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) →
(𝐹‘((#‘𝐹) − 1)) ∈ dom 𝐸) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (𝐹‘((#‘𝐹) − 1)) ∈ dom 𝐸) |
108 | 38, 107 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (𝐸‘(𝐹‘((#‘𝐹) − 1))) ∈ ran 𝐸) |
109 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} = (𝐸‘(𝐹‘((#‘𝐹) − 1)))) |
110 | 109 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} = (𝐸‘(𝐹‘((#‘𝐹) − 1)))) |
111 | 110 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸 ↔ (𝐸‘(𝐹‘((#‘𝐹) − 1))) ∈ ran 𝐸)) |
112 | 108, 111 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
113 | 97, 112 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → ((𝐸‘(𝐹‘((#‘𝐹) − 1))) = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
114 | 92, 113 | syld 46 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
115 | 114 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
116 | 115 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
117 | 116 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸) |
118 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))}) |
119 | 118 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) = (𝑃‘(#‘𝐹)) → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
120 | 119 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
121 | 120 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(#‘𝐹))} ∈ ran 𝐸)) |
122 | 117, 121 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸) |
123 | 26, 62, 122 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑃 ∈ Word
𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) ∧ 2
≤ (#‘𝑃)) ∧
𝐸:dom 𝐸⟶ran 𝐸) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |
124 | 123 | exp41 636 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑃 ∈ Word 𝑉 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (#‘𝐹) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝐹) + 1)) →
(2 ≤ (#‘𝑃) →
(𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
125 | 124 | exp41 636 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) ∈ ℕ0 →
((#‘𝑃) =
((#‘𝐹) + 1) → (2
≤ (#‘𝑃) →
(𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))))) |
126 | 8, 125 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝐹 ∈ Word dom 𝐸 → ((#‘𝐹) ∈ ℕ0 →
((#‘𝑃) =
((#‘𝐹) + 1) → (2
≤ (#‘𝑃) →
(𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))))) |
127 | 126 | com13 86 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ0 → (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))))) |
128 | 4, 127 | mpcom 37 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))))) |
129 | 128 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝑃) = ((#‘𝐹) + 1) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
130 | 7, 129 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
131 | 130 | expcom 450 |
. . . . . . . 8
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (𝐹 ∈ Word dom 𝐸 → (2 ≤ (#‘𝑃) → (𝐸:dom 𝐸⟶ran 𝐸 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
132 | 131 | com14 94 |
. . . . . . 7
⊢ (𝐸:dom 𝐸⟶ran 𝐸 → (𝐹 ∈ Word dom 𝐸 → (2 ≤ (#‘𝑃) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
133 | 132 | imp 444 |
. . . . . 6
⊢ ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → (2 ≤ (#‘𝑃) → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
134 | 133 | com13 86 |
. . . . 5
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → (2 ≤ (#‘𝑃) → ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
135 | 134 | imp 444 |
. . . 4
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
136 | 135 | com12 32 |
. . 3
⊢ ((𝐸:dom 𝐸⟶ran 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
137 | 3, 136 | sylan 487 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
138 | 137 | 3imp 1249 |
1
⊢ (((𝑉 USGrph 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |