Step | Hyp | Ref
| Expression |
1 | | clwlkisclwwlklem0 26316 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) |
2 | | lencl 13179 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
3 | | ige2m1fz 12299 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈ (0...(#‘𝑃))) |
4 | 2, 3 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈ (0...(#‘𝑃))) |
5 | | swrd0len 13274 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ (0...(#‘𝑃))) → (#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) =
((#‘𝑃) −
1)) |
6 | 4, 5 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) = ((#‘𝑃) − 1)) |
7 | 2 | nn0cnd 11230 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℂ) |
8 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ) |
9 | 7, 8 | subcld 10271 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) ∈
ℂ) |
10 | 9 | subid1d 10260 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (((#‘𝑃) − 1) − 0) = ((#‘𝑃) − 1)) |
11 | 10 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = (((#‘𝑃) − 1) − 0)) |
12 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) = (((#‘𝑃) − 1) − 0)) |
13 | 6, 12 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) = (((#‘𝑃) − 1) −
0)) |
14 | 13 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1) =
((((#‘𝑃) − 1)
− 0) − 1)) |
15 | 14 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) =
(0..^((((#‘𝑃) −
1) − 0) − 1))) |
16 | 6 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1) =
(((#‘𝑃) − 1)
− 1)) |
17 | 16 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) =
(0..^(((#‘𝑃) −
1) − 1))) |
18 | 17 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) ↔
𝑖 ∈
(0..^(((#‘𝑃) −
1) − 1)))) |
19 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑃 ∈ Word 𝑉) |
20 | | wrdlenge2n0 13196 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → 𝑃 ≠ ∅) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑃 ≠ ∅) |
22 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℤ) |
23 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) ∈
ℤ → ((#‘𝑃)
− 1) ∈ ℤ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) ∈
ℤ) |
25 | 2, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) ∈
ℤ) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈
ℤ) |
27 | | elfzom1elfzo 12403 |
. . . . . . . . . . . . . . . 16
⊢
((((#‘𝑃)
− 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((#‘𝑃) − 1))) |
28 | 26, 27 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((#‘𝑃) − 1))) |
29 | | swrdtrcfv 13293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖) = (𝑃‘𝑖)) |
30 | 19, 21, 28, 29 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖) = (𝑃‘𝑖)) |
31 | 2 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘𝑃) ∈
ℕ0) |
32 | | elfzom1elp1fzo 12402 |
. . . . . . . . . . . . . . . . 17
⊢
((((#‘𝑃)
− 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈
(0..^((#‘𝑃) −
1))) |
33 | 24, 32 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝑖
∈ (0..^(((#‘𝑃)
− 1) − 1))) → (𝑖 + 1) ∈ (0..^((#‘𝑃) − 1))) |
34 | 31, 33 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈
(0..^((#‘𝑃) −
1))) |
35 | | swrdtrcfv 13293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ (𝑖 + 1) ∈ (0..^((#‘𝑃) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
36 | 19, 21, 34, 35 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
37 | 30, 36 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → {((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
38 | 37 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → ({((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
39 | 38 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1)) → ({((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
40 | 18, 39 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) →
({((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
41 | 40 | imp 444 |
. . . . . . . . 9
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1))) →
({((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
42 | 15, 41 | raleqbidva 3131 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
43 | | swrdtrcfvl 13302 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) = (𝑃‘((#‘𝑃) − 2))) |
44 | | swrdtrcfv0 13294 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0) = (𝑃‘0)) |
45 | 43, 44 | preq12d 4220 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) |
46 | 45 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ({( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) |
47 | 42, 46 | anbi12d 743 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸) ↔
(∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) |
48 | 47 | bicomd 212 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸))) |
49 | 48 | 3adant1 1072 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸))) |
50 | | swrdcl 13271 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉) |
51 | 50 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉) |
52 | 51 | 3biant1d 1433 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸) ↔
((𝑃 substr 〈0,
((#‘𝑃) −
1)〉) ∈ Word 𝑉
∧ ∀𝑖 ∈
(0..^((#‘(𝑃 substr
〈0, ((#‘𝑃)
− 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸))) |
53 | 49, 52 | bitrd 267 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸))) |
54 | 53 | anbi2d 736 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸)))) |
55 | 1, 54 | bitrd 267 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸)))) |
56 | | usgrav 25867 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
57 | | isclwlk 26284 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))))) |
58 | | 3an4anass 1283 |
. . . . . . 7
⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
59 | 57, 58 | syl6bbr 277 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
60 | 56, 59 | syl 17 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
61 | 60 | adantr 480 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉) → (𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
62 | 61 | exbidv 1837 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
63 | 62 | 3adant3 1074 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
64 | | isclwwlk 26296 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈
(𝑉 ClWWalks 𝐸) ↔ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸))) |
65 | 56, 64 | syl 17 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸))) |
66 | 65 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸))) |
67 | 66 | anbi2d 736 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ (𝑉 ClWWalks 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸)))) |
68 | 55, 63, 67 | 3bitr4d 299 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ (𝑉 ClWWalks 𝐸)))) |