Step | Hyp | Ref
| Expression |
1 | | clwlkclwwlk.e |
. . . . . 6
⊢ 𝐸 = (iEdg‘𝐺) |
2 | 1 | uspgrf1oedg 40403 |
. . . . 5
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) |
3 | | f1of1 6049 |
. . . . 5
⊢ (𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺) → 𝐸:dom 𝐸–1-1→(Edg‘𝐺)) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1→(Edg‘𝐺)) |
5 | | clwlkclwwlklem3 41210 |
. . . 4
⊢ ((𝐸:dom 𝐸–1-1→(Edg‘𝐺) ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) |
6 | 4, 5 | syl3an1 1351 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) |
7 | | lencl 13179 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
8 | | ige2m1fz 12299 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈ (0...(#‘𝑃))) |
9 | 7, 8 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈ (0...(#‘𝑃))) |
10 | | swrd0len 13274 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ (0...(#‘𝑃))) → (#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) =
((#‘𝑃) −
1)) |
11 | 9, 10 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) = ((#‘𝑃) − 1)) |
12 | 7 | nn0cnd 11230 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈ ℂ) |
13 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ) |
14 | 12, 13 | subcld 10271 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) ∈
ℂ) |
15 | 14 | subid1d 10260 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word 𝑉 → (((#‘𝑃) − 1) − 0) = ((#‘𝑃) − 1)) |
16 | 15 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) = (((#‘𝑃) − 1) − 0)) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) = (((#‘𝑃) − 1) − 0)) |
18 | 11, 17 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) = (((#‘𝑃) − 1) −
0)) |
19 | 18 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1) =
((((#‘𝑃) − 1)
− 0) − 1)) |
20 | 19 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) =
(0..^((((#‘𝑃) −
1) − 0) − 1))) |
21 | 11 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1) =
(((#‘𝑃) − 1)
− 1)) |
22 | 21 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) =
(0..^(((#‘𝑃) −
1) − 1))) |
23 | 22 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) ↔
𝑖 ∈
(0..^(((#‘𝑃) −
1) − 1)))) |
24 | | simpll 786 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑃 ∈ Word 𝑉) |
25 | | wrdlenge2n0 13196 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → 𝑃 ≠ ∅) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑃 ≠ ∅) |
27 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℤ) |
28 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) ∈
ℤ → ((#‘𝑃)
− 1) ∈ ℤ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) ∈
ℤ) |
30 | 7, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) − 1) ∈
ℤ) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈
ℤ) |
32 | | elfzom1elfzo 12403 |
. . . . . . . . . . . . . . . 16
⊢
((((#‘𝑃)
− 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((#‘𝑃) − 1))) |
33 | 31, 32 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((#‘𝑃) − 1))) |
34 | | swrdtrcfv 13293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖) = (𝑃‘𝑖)) |
35 | 24, 26, 33, 34 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖) = (𝑃‘𝑖)) |
36 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘𝑃) ∈
ℕ0) |
37 | | elfzom1elp1fzo 12402 |
. . . . . . . . . . . . . . . . 17
⊢
((((#‘𝑃)
− 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈
(0..^((#‘𝑃) −
1))) |
38 | 29, 37 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝑖
∈ (0..^(((#‘𝑃)
− 1) − 1))) → (𝑖 + 1) ∈ (0..^((#‘𝑃) − 1))) |
39 | 36, 38 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈
(0..^((#‘𝑃) −
1))) |
40 | | swrdtrcfv 13293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ 𝑃 ≠ ∅ ∧ (𝑖 + 1) ∈ (0..^((#‘𝑃) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
41 | 24, 26, 39, 40 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
42 | 35, 41 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → {((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
43 | 42 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1))) → ({((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
44 | 43 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑖 ∈ (0..^(((#‘𝑃) − 1) − 1)) → ({((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
45 | 23, 44 | sylbid 229 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)) →
({((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))) |
46 | 45 | imp 444 |
. . . . . . . . 9
⊢ (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1))) →
({((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
47 | 20, 46 | raleqbidva 3131 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
48 | | swrdtrcfvl 13302 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) = (𝑃‘((#‘𝑃) − 2))) |
49 | | swrdtrcfv0 13294 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0) = (𝑃‘0)) |
50 | 48, 49 | preq12d 4220 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) |
51 | 50 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ({( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) |
52 | 47, 51 | 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 𝐸))) |
53 | 52 | 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 𝐸))) |
54 | 53 | 3adant1 1072 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 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 𝐸))) |
55 | | swrdcl 13271 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉) |
56 | 55 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉) |
57 | 56 | 3biant1d 1433 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 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 𝐸))) |
58 | 54, 57 | bitrd 267 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 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 𝐸))) |
59 | 58 | anbi2d 736 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 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 𝐸)))) |
60 | 6, 59 | bitrd 267 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 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 𝐸)))) |
61 | | uspgrupgr 40406 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph
) |
62 | 61 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → 𝐺 ∈ UPGraph ) |
63 | | vex 3176 |
. . . . . 6
⊢ 𝑓 ∈ V |
64 | 63 | a1i 11 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → 𝑓 ∈ V) |
65 | | simpr 476 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → 𝑃 ∈ Word 𝑉) |
66 | | clwlkclwwlk.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
67 | 66, 1 | isclWlkupgr 40985 |
. . . . . 6
⊢ ((𝐺 ∈ UPGraph ∧ 𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑓(ClWalkS‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))))) |
68 | | 3an4anass 1283 |
. . . . . 6
⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
69 | 67, 68 | syl6bbr 277 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ 𝑓 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑓(ClWalkS‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
70 | 62, 64, 65, 69 | syl3anc 1318 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (𝑓(ClWalkS‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
71 | 70 | exbidv 1837 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (∃𝑓 𝑓(ClWalkS‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
72 | 71 | 3adant3 1074 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓 𝑓(ClWalkS‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
73 | | eqid 2610 |
. . . . . 6
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
74 | 66, 73 | isclwwlks 41188 |
. . . . 5
⊢ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈
(ClWWalkS‘𝐺) ↔
(((𝑃 substr 〈0,
((#‘𝑃) −
1)〉) ∈ Word 𝑉
∧ (𝑃 substr 〈0,
((#‘𝑃) −
1)〉) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ (Edg‘𝐺))) |
75 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → 𝑃 ∈ Word 𝑉) |
76 | | nn0ge2m1nn 11237 |
. . . . . . . . . . . 12
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈
ℕ) |
77 | 7, 76 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈
ℕ) |
78 | | nn0re 11178 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℝ) |
79 | 78 | lem1d 10836 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) ≤ (#‘𝑃)) |
80 | 79 | a1d 25 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℕ0 → (2 ≤ (#‘𝑃) → ((#‘𝑃) − 1) ≤ (#‘𝑃))) |
81 | 7, 80 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Word 𝑉 → (2 ≤ (#‘𝑃) → ((#‘𝑃) − 1) ≤ (#‘𝑃))) |
82 | 81 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ≤ (#‘𝑃)) |
83 | 75, 77, 82 | 3jca 1235 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧
((#‘𝑃) − 1)
≤ (#‘𝑃))) |
84 | 83 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧
((#‘𝑃) − 1)
≤ (#‘𝑃))) |
85 | | swrdn0 13282 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Word 𝑉 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧
((#‘𝑃) − 1)
≤ (#‘𝑃)) →
(𝑃 substr 〈0,
((#‘𝑃) −
1)〉) ≠ ∅) |
86 | 84, 85 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ≠
∅) |
87 | 86 | biantrud 527 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ↔ ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ≠
∅))) |
88 | 87 | bicomd 212 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ≠ ∅) ↔
(𝑃 substr 〈0,
((#‘𝑃) −
1)〉) ∈ Word 𝑉)) |
89 | 88 | 3anbi1d 1395 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ≠ ∅) ∧
∀𝑖 ∈
(0..^((#‘(𝑃 substr
〈0, ((#‘𝑃)
− 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ (Edg‘𝐺))
↔ ((𝑃 substr 〈0,
((#‘𝑃) −
1)〉) ∈ Word 𝑉
∧ ∀𝑖 ∈
(0..^((#‘(𝑃 substr
〈0, ((#‘𝑃)
− 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ (Edg‘𝐺)))) |
90 | 74, 89 | syl5bb 271 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈
(ClWWalkS‘𝐺) ↔
((𝑃 substr 〈0,
((#‘𝑃) −
1)〉) ∈ Word 𝑉
∧ ∀𝑖 ∈
(0..^((#‘(𝑃 substr
〈0, ((#‘𝑃)
− 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ (Edg‘𝐺)))) |
91 | | edgaval 25794 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
92 | 1 | eqcomi 2619 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
𝐸 |
93 | 92 | rneqi 5273 |
. . . . . . . . 9
⊢ ran
(iEdg‘𝐺) = ran 𝐸 |
94 | 91, 93 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran 𝐸) |
95 | 94 | eleq2d 2673 |
. . . . . . 7
⊢ (𝐺 ∈ USPGraph →
({((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
96 | 95 | ralbidv 2969 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(∀𝑖 ∈
(0..^((#‘(𝑃 substr
〈0, ((#‘𝑃)
− 1)〉)) − 1)){((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
97 | 94 | eleq2d 2673 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph → ({(
lastS ‘(𝑃 substr
〈0, ((#‘𝑃)
− 1)〉)), ((𝑃
substr 〈0, ((#‘𝑃) − 1)〉)‘0)} ∈
(Edg‘𝐺) ↔ {(
lastS ‘(𝑃 substr
〈0, ((#‘𝑃)
− 1)〉)), ((𝑃
substr 〈0, ((#‘𝑃) − 1)〉)‘0)} ∈ ran
𝐸)) |
98 | 96, 97 | 3anbi23d 1394 |
. . . . 5
⊢ (𝐺 ∈ USPGraph → (((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ (Edg‘𝐺))
↔ ((𝑃 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 𝐸))) |
99 | 98 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (((𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)) −
1)){((𝑃 substr 〈0,
((#‘𝑃) −
1)〉)‘𝑖), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝑃 substr 〈0, ((#‘𝑃) − 1)〉)), ((𝑃 substr 〈0, ((#‘𝑃) − 1)〉)‘0)}
∈ (Edg‘𝐺))
↔ ((𝑃 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 𝐸))) |
100 | 90, 99 | bitrd 267 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 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 𝐸))) |
101 | 100 | anbi2d 736 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 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 𝐸)))) |
102 | 60, 72, 101 | 3bitr4d 299 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓 𝑓(ClWalkS‘𝐺)𝑃 ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈
(ClWWalkS‘𝐺)))) |