Proof of Theorem clwlkisclwwlklem0
Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → 𝑉 USGrph 𝐸) |
2 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → 𝑓 ∈ Word dom 𝐸) |
3 | 2 | adantr 480 |
. . . . . . 7
⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → 𝑓 ∈ Word dom 𝐸) |
4 | 1, 3 | anim12i 588 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) → (𝑉 USGrph 𝐸 ∧ 𝑓 ∈ Word dom 𝐸)) |
5 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → 2 ≤ (#‘𝑃)) |
6 | | simpl2 1058 |
. . . . . . 7
⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → 𝑃:(0...(#‘𝑓))⟶𝑉) |
7 | 5, 6 | anim12ci 589 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) → (𝑃:(0...(#‘𝑓))⟶𝑉 ∧ 2 ≤ (#‘𝑃))) |
8 | | simp3 1056 |
. . . . . . . 8
⊢ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
9 | 8 | anim1i 590 |
. . . . . . 7
⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) |
10 | 9 | adantl 481 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) → (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) |
11 | | clwlkisclwwlklem1 26315 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑓 ∈ Word dom 𝐸) ∧ (𝑃:(0...(#‘𝑓))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |
12 | 4, 7, 10, 11 | syl3anc 1318 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |
13 | | lencl 13179 |
. . . . . . . 8
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
14 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ Word dom 𝐸 → (#‘𝑓) ∈
ℕ0) |
15 | | ffz0hash 13088 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑓) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉) → (#‘𝑃) = ((#‘𝑓) + 1)) |
16 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑃) =
((#‘𝑓) + 1) →
((#‘𝑃) − 1) =
(((#‘𝑓) + 1) −
1)) |
17 | 16 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) =
((#‘𝑓) + 1) →
(((#‘𝑃) − 1)
− 0) = ((((#‘𝑓)
+ 1) − 1) − 0)) |
18 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑓) ∈
ℕ0 → (#‘𝑓) ∈ ℂ) |
19 | | peano2cn 10087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝑓) ∈
ℂ → ((#‘𝑓)
+ 1) ∈ ℂ) |
20 | | peano2cnm 10226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑓) + 1)
∈ ℂ → (((#‘𝑓) + 1) − 1) ∈
ℂ) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑓) ∈
ℕ0 → (((#‘𝑓) + 1) − 1) ∈
ℂ) |
22 | 21 | subid1d 10260 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑓) ∈
ℕ0 → ((((#‘𝑓) + 1) − 1) − 0) =
(((#‘𝑓) + 1) −
1)) |
23 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑓) ∈
ℕ0 → 1 ∈ ℂ) |
24 | 18, 23 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑓) ∈
ℕ0 → (((#‘𝑓) + 1) − 1) = (#‘𝑓)) |
25 | 22, 24 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑓) ∈
ℕ0 → ((((#‘𝑓) + 1) − 1) − 0) = (#‘𝑓)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑓) ∈
ℕ0 ∧ (#‘𝑃) ∈ ℕ0) →
((((#‘𝑓) + 1) −
1) − 0) = (#‘𝑓)) |
27 | 17, 26 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
(((#‘𝑃) − 1)
− 0) = (#‘𝑓)) |
28 | 27 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
((((#‘𝑃) − 1)
− 0) − 1) = ((#‘𝑓) − 1)) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
(0..^((((#‘𝑃) −
1) − 0) − 1)) = (0..^((#‘𝑓) − 1))) |
30 | 29 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
(∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) |
31 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) =
((#‘𝑓) + 1) →
((#‘𝑃) − 2) =
(((#‘𝑓) + 1) −
2)) |
32 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑓) ∈
ℕ0 → 2 ∈ ℂ) |
33 | 18, 32, 23 | subsub3d 10301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑓) ∈
ℕ0 → ((#‘𝑓) − (2 − 1)) = (((#‘𝑓) + 1) −
2)) |
34 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (2
− 1) = 1 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝑓) ∈
ℕ0 → (2 − 1) = 1) |
36 | 35 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑓) ∈
ℕ0 → ((#‘𝑓) − (2 − 1)) = ((#‘𝑓) − 1)) |
37 | 33, 36 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑓) ∈
ℕ0 → (((#‘𝑓) + 1) − 2) = ((#‘𝑓) − 1)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑓) ∈
ℕ0 ∧ (#‘𝑃) ∈ ℕ0) →
(((#‘𝑓) + 1) −
2) = ((#‘𝑓) −
1)) |
39 | 31, 38 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
((#‘𝑃) − 2) =
((#‘𝑓) −
1)) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
(𝑃‘((#‘𝑃) − 2)) = (𝑃‘((#‘𝑓) − 1))) |
41 | 40 | preq1d 4218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} = {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)}) |
42 | 41 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
({(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |
43 | 30, 42 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
((∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸))) |
44 | 43 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
((( lastS ‘𝑃) =
(𝑃‘0) ∧
(∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
45 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( lastS
‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸))) |
46 | 44, 45 | syl6bbr 277 |
. . . . . . . . . . . . . . . . 17
⊢
((((#‘𝑓)
∈ ℕ0 ∧ (#‘𝑃) ∈ ℕ0) ∧
(#‘𝑃) =
((#‘𝑓) + 1)) →
((( lastS ‘𝑃) =
(𝑃‘0) ∧
(∀𝑖 ∈
(0..^((((#‘𝑃) −
1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸))) |
47 | 46 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑃) =
((#‘𝑓) + 1) →
(((#‘𝑓) ∈
ℕ0 ∧ (#‘𝑃) ∈ ℕ0) → (((
lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
48 | 47 | expd 451 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑃) =
((#‘𝑓) + 1) →
((#‘𝑓) ∈
ℕ0 → ((#‘𝑃) ∈ ℕ0 → (((
lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
49 | 15, 48 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑓) ∈
ℕ0 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉) → ((#‘𝑓) ∈ ℕ0 →
((#‘𝑃) ∈
ℕ0 → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
50 | 49 | ex 449 |
. . . . . . . . . . . . 13
⊢
((#‘𝑓) ∈
ℕ0 → (𝑃:(0...(#‘𝑓))⟶𝑉 → ((#‘𝑓) ∈ ℕ0 →
((#‘𝑃) ∈
ℕ0 → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
51 | 50 | com23 84 |
. . . . . . . . . . . 12
⊢
((#‘𝑓) ∈
ℕ0 → ((#‘𝑓) ∈ ℕ0 → (𝑃:(0...(#‘𝑓))⟶𝑉 → ((#‘𝑃) ∈ ℕ0 → (((
lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))))) |
52 | 14, 14, 51 | sylc 63 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ Word dom 𝐸 → (𝑃:(0...(#‘𝑓))⟶𝑉 → ((#‘𝑃) ∈ ℕ0 → (((
lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸))))) |
53 | 52 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉) → ((#‘𝑃) ∈ ℕ0 → (((
lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
54 | 53 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((#‘𝑃) ∈ ℕ0 → (((
lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
55 | 54 | adantr 480 |
. . . . . . . 8
⊢ (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → ((#‘𝑃) ∈ ℕ0 → (((
lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
56 | 13, 55 | syl5com 31 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
57 | 56 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸)))) |
58 | 57 | imp 444 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝑓) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑓) − 1)), (𝑃‘0)} ∈ ran 𝐸))) |
59 | 12, 58 | mpbird 246 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ ((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))) |
60 | 59 | ex 449 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) |
61 | 60 | exlimdv 1848 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) |
62 | | clwlkisclwwlklem2 26314 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) |
63 | 61, 62 | impbid 201 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) |