Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
2 | 1 | wlkf 27702 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom (iEdg‘𝐺)) |
3 | | revcl 14326 |
. . 3
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(reverse‘𝐹) ∈
Word dom (iEdg‘𝐺)) |
4 | 2, 3 | syl 17 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹) ∈ Word dom (iEdg‘𝐺)) |
5 | | eqid 2737 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
6 | 5 | wlkpwrd 27705 |
. . . 4
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ Word (Vtx‘𝐺)) |
7 | | revcl 14326 |
. . . 4
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (reverse‘𝑃) ∈ Word (Vtx‘𝐺)) |
8 | | wrdf 14074 |
. . . 4
⊢
((reverse‘𝑃)
∈ Word (Vtx‘𝐺)
→ (reverse‘𝑃):(0..^(♯‘(reverse‘𝑃)))⟶(Vtx‘𝐺)) |
9 | 6, 7, 8 | 3syl 18 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝑃):(0..^(♯‘(reverse‘𝑃)))⟶(Vtx‘𝐺)) |
10 | | revlen 14327 |
. . . . . . 7
⊢ (𝐹 ∈ Word dom
(iEdg‘𝐺) →
(♯‘(reverse‘𝐹)) = (♯‘𝐹)) |
11 | 2, 10 | syl 17 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘(reverse‘𝐹)) = (♯‘𝐹)) |
12 | 11 | oveq2d 7229 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 →
(0...(♯‘(reverse‘𝐹))) = (0...(♯‘𝐹))) |
13 | | wlklenvp1 27706 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝑃) = ((♯‘𝐹) + 1)) |
14 | 13 | oveq2d 7229 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → (0..^(♯‘𝑃)) = (0..^((♯‘𝐹) + 1))) |
15 | | revlen 14327 |
. . . . . . . 8
⊢ (𝑃 ∈ Word (Vtx‘𝐺) →
(♯‘(reverse‘𝑃)) = (♯‘𝑃)) |
16 | 6, 15 | syl 17 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘(reverse‘𝑃)) = (♯‘𝑃)) |
17 | 16 | oveq2d 7229 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 →
(0..^(♯‘(reverse‘𝑃))) = (0..^(♯‘𝑃))) |
18 | | wlkcl 27703 |
. . . . . . . 8
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
19 | 18 | nn0zd 12280 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℤ) |
20 | | fzval3 13311 |
. . . . . . 7
⊢
((♯‘𝐹)
∈ ℤ → (0...(♯‘𝐹)) = (0..^((♯‘𝐹) + 1))) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → (0...(♯‘𝐹)) = (0..^((♯‘𝐹) + 1))) |
22 | 14, 17, 21 | 3eqtr4rd 2788 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 → (0...(♯‘𝐹)) =
(0..^(♯‘(reverse‘𝑃)))) |
23 | 12, 22 | eqtrd 2777 |
. . . 4
⊢ (𝐹(Walks‘𝐺)𝑃 →
(0...(♯‘(reverse‘𝐹))) =
(0..^(♯‘(reverse‘𝑃)))) |
24 | 23 | feq2d 6531 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → ((reverse‘𝑃):(0...(♯‘(reverse‘𝐹)))⟶(Vtx‘𝐺) ↔ (reverse‘𝑃):(0..^(♯‘(reverse‘𝑃)))⟶(Vtx‘𝐺))) |
25 | 9, 24 | mpbird 260 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝑃):(0...(♯‘(reverse‘𝐹)))⟶(Vtx‘𝐺)) |
26 | 11 | oveq2d 7229 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 →
(0..^(♯‘(reverse‘𝐹))) = (0..^(♯‘𝐹))) |
27 | 26 | eleq2d 2823 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝑘 ∈
(0..^(♯‘(reverse‘𝐹))) ↔ 𝑘 ∈ (0..^(♯‘𝐹)))) |
28 | 27 | biimpa 480 |
. . . 4
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈
(0..^(♯‘(reverse‘𝐹)))) → 𝑘 ∈ (0..^(♯‘𝐹))) |
29 | | revfv 14328 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word dom
(iEdg‘𝐺) ∧ 𝑘 ∈
(0..^(♯‘𝐹)))
→ ((reverse‘𝐹)‘𝑘) = (𝐹‘(((♯‘𝐹) − 1) − 𝑘))) |
30 | 2, 29 | sylan 583 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((reverse‘𝐹)‘𝑘) = (𝐹‘(((♯‘𝐹) − 1) − 𝑘))) |
31 | | wlklenvm1 27709 |
. . . . . . . . . . . . 13
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) = ((♯‘𝑃) − 1)) |
32 | 31 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (𝐹(Walks‘𝐺)𝑃 → ((♯‘𝐹) − 1) = (((♯‘𝑃) − 1) −
1)) |
33 | | lencl 14088 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (♯‘𝑃) ∈
ℕ0) |
34 | 33 | nn0cnd 12152 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ Word (Vtx‘𝐺) → (♯‘𝑃) ∈
ℂ) |
35 | | sub1m1 12082 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑃)
∈ ℂ → (((♯‘𝑃) − 1) − 1) =
((♯‘𝑃) −
2)) |
36 | 6, 34, 35 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝐹(Walks‘𝐺)𝑃 → (((♯‘𝑃) − 1) − 1) =
((♯‘𝑃) −
2)) |
37 | 32, 36 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝐹(Walks‘𝐺)𝑃 → ((♯‘𝐹) − 1) = ((♯‘𝑃) − 2)) |
38 | 37 | fvoveq1d 7235 |
. . . . . . . . . 10
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹‘(((♯‘𝐹) − 1) − 𝑘)) = (𝐹‘(((♯‘𝑃) − 2) − 𝑘))) |
39 | 38 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (𝐹‘(((♯‘𝐹) − 1) − 𝑘)) = (𝐹‘(((♯‘𝑃) − 2) − 𝑘))) |
40 | 30, 39 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((reverse‘𝐹)‘𝑘) = (𝐹‘(((♯‘𝑃) − 2) − 𝑘))) |
41 | 40 | fveq2d 6721 |
. . . . . . 7
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))) |
42 | 41 | adantr 484 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))) |
43 | | fzonn0p1p1 13321 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(0..^(♯‘𝐹))
→ (𝑘 + 1) ∈
(0..^((♯‘𝐹) +
1))) |
44 | 43 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (𝑘 + 1) ∈ (0..^((♯‘𝐹) + 1))) |
45 | 14 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (0..^(♯‘𝑃)) = (0..^((♯‘𝐹) + 1))) |
46 | 44, 45 | eleqtrrd 2841 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (𝑘 + 1) ∈ (0..^(♯‘𝑃))) |
47 | | revfv 14328 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ (𝑘 + 1) ∈ (0..^(♯‘𝑃))) → ((reverse‘𝑃)‘(𝑘 + 1)) = (𝑃‘(((♯‘𝑃) − 1) − (𝑘 + 1)))) |
48 | 6, 46, 47 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((reverse‘𝑃)‘(𝑘 + 1)) = (𝑃‘(((♯‘𝑃) − 1) − (𝑘 + 1)))) |
49 | | elfzoelz 13243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(0..^(♯‘𝐹))
→ 𝑘 ∈
ℤ) |
50 | 49 | zcnd 12283 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(0..^(♯‘𝐹))
→ 𝑘 ∈
ℂ) |
51 | 50 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → 𝑘 ∈ ℂ) |
52 | | 1cnd 10828 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → 1 ∈
ℂ) |
53 | 51, 52 | addcomd 11034 |
. . . . . . . . . . . . 13
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (𝑘 + 1) = (1 + 𝑘)) |
54 | 53 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝑃) − 1) − (𝑘 + 1)) = (((♯‘𝑃) − 1) − (1 + 𝑘))) |
55 | 6, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝑃) ∈ ℂ) |
56 | 55 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (♯‘𝑃) ∈ ℂ) |
57 | 56, 52 | subcld 11189 |
. . . . . . . . . . . . 13
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((♯‘𝑃) − 1) ∈
ℂ) |
58 | 57, 52, 51 | subsub4d 11220 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((((♯‘𝑃) − 1) − 1) −
𝑘) = (((♯‘𝑃) − 1) − (1 + 𝑘))) |
59 | 36 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ (𝐹(Walks‘𝐺)𝑃 → ((((♯‘𝑃) − 1) − 1) − 𝑘) = (((♯‘𝑃) − 2) − 𝑘)) |
60 | 59 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((((♯‘𝑃) − 1) − 1) −
𝑘) = (((♯‘𝑃) − 2) − 𝑘)) |
61 | 54, 58, 60 | 3eqtr2d 2783 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝑃) − 1) − (𝑘 + 1)) = (((♯‘𝑃) − 2) − 𝑘)) |
62 | 61 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (𝑃‘(((♯‘𝑃) − 1) − (𝑘 + 1))) = (𝑃‘(((♯‘𝑃) − 2) − 𝑘))) |
63 | 48, 62 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((reverse‘𝑃)‘(𝑘 + 1)) = (𝑃‘(((♯‘𝑃) − 2) − 𝑘))) |
64 | 63 | sneqd 4553 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → {((reverse‘𝑃)‘(𝑘 + 1))} = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}) |
65 | 64 | adantr 484 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → {((reverse‘𝑃)‘(𝑘 + 1))} = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}) |
66 | | sneq 4551 |
. . . . . . . 8
⊢
(((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)) → {((reverse‘𝑃)‘𝑘)} = {((reverse‘𝑃)‘(𝑘 + 1))}) |
67 | 66 | adantl 485 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → {((reverse‘𝑃)‘𝑘)} = {((reverse‘𝑃)‘(𝑘 + 1))}) |
68 | | eqcom 2744 |
. . . . . . . . . 10
⊢
(((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)) ↔ ((reverse‘𝑃)‘(𝑘 + 1)) = ((reverse‘𝑃)‘𝑘)) |
69 | | fzossfzop1 13320 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝐹)
∈ ℕ0 → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1))) |
70 | 18, 69 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐹(Walks‘𝐺)𝑃 → (0..^(♯‘𝐹)) ⊆
(0..^((♯‘𝐹) +
1))) |
71 | 70, 14 | sseqtrrd 3942 |
. . . . . . . . . . . . . 14
⊢ (𝐹(Walks‘𝐺)𝑃 → (0..^(♯‘𝐹)) ⊆
(0..^(♯‘𝑃))) |
72 | 71 | sselda 3901 |
. . . . . . . . . . . . 13
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → 𝑘 ∈ (0..^(♯‘𝑃))) |
73 | | revfv 14328 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Word (Vtx‘𝐺) ∧ 𝑘 ∈ (0..^(♯‘𝑃))) → ((reverse‘𝑃)‘𝑘) = (𝑃‘(((♯‘𝑃) − 1) − 𝑘))) |
74 | 6, 72, 73 | syl2an2r 685 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((reverse‘𝑃)‘𝑘) = (𝑃‘(((♯‘𝑃) − 1) − 𝑘))) |
75 | 57, 51, 52 | sub32d 11221 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((((♯‘𝑃) − 1) − 𝑘) − 1) =
((((♯‘𝑃)
− 1) − 1) − 𝑘)) |
76 | 75 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((((♯‘𝑃) − 1) − 𝑘) − 1) + 1) =
(((((♯‘𝑃)
− 1) − 1) − 𝑘) + 1)) |
77 | 57, 51 | subcld 11189 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝑃) − 1) − 𝑘) ∈
ℂ) |
78 | 77, 52 | npcand 11193 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((((♯‘𝑃) − 1) − 𝑘) − 1) + 1) =
(((♯‘𝑃) −
1) − 𝑘)) |
79 | 59 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝐹(Walks‘𝐺)𝑃 → (((((♯‘𝑃) − 1) − 1) − 𝑘) + 1) = ((((♯‘𝑃) − 2) − 𝑘) + 1)) |
80 | 79 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((((♯‘𝑃) − 1) − 1) −
𝑘) + 1) =
((((♯‘𝑃)
− 2) − 𝑘) +
1)) |
81 | 76, 78, 80 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝑃) − 1) − 𝑘) = ((((♯‘𝑃) − 2) − 𝑘) + 1)) |
82 | 81 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (𝑃‘(((♯‘𝑃) − 1) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))) |
83 | 74, 82 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((reverse‘𝑃)‘𝑘) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))) |
84 | 63, 83 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((reverse‘𝑃)‘(𝑘 + 1)) = ((reverse‘𝑃)‘𝑘) ↔ (𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)))) |
85 | 68, 84 | syl5bb 286 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)) ↔ (𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)))) |
86 | | wkslem1 27695 |
. . . . . . . . . . . 12
⊢ (𝑥 = (((♯‘𝑃) − 2) − 𝑘) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑥))) ↔ if-((𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)), ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}, {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))))) |
87 | 5, 1 | wlkprop 27699 |
. . . . . . . . . . . . . 14
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom (iEdg‘𝐺) ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑥))))) |
88 | 87 | simp3d 1146 |
. . . . . . . . . . . . 13
⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑥 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑥)))) |
89 | 88 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ∀𝑥 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), ((iEdg‘𝐺)‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘𝑥)))) |
90 | 18 | nn0cnd 12152 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℂ) |
91 | 90 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℂ) |
92 | 91, 51, 52 | sub32d 11221 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝐹) − 𝑘) − 1) = (((♯‘𝐹) − 1) − 𝑘)) |
93 | 37 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((♯‘𝐹) − 1) = ((♯‘𝑃) − 2)) |
94 | 93 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝐹) − 1) − 𝑘) = (((♯‘𝑃) − 2) − 𝑘)) |
95 | 92, 94 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝐹) − 𝑘) − 1) = (((♯‘𝑃) − 2) − 𝑘)) |
96 | | ubmelm1fzo 13338 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(0..^(♯‘𝐹))
→ (((♯‘𝐹)
− 𝑘) − 1)
∈ (0..^(♯‘𝐹))) |
97 | 96 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝐹) − 𝑘) − 1) ∈ (0..^(♯‘𝐹))) |
98 | 95, 97 | eqeltrrd 2839 |
. . . . . . . . . . . 12
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((♯‘𝑃) − 2) − 𝑘) ∈
(0..^(♯‘𝐹))) |
99 | 86, 89, 98 | rspcdva 3539 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → if-((𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)), ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}, {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))))) |
100 | | dfifp2 1065 |
. . . . . . . . . . 11
⊢
(if-((𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)), ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}, {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))) ↔ (((𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)) → ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}) ∧ (¬ (𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)) → {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))))) |
101 | 99, 100 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)) → ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}) ∧ (¬ (𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)) → {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))))) |
102 | 101 | simpld 498 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → ((𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)) → ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))})) |
103 | 85, 102 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)) → ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))})) |
104 | 103 | imp 410 |
. . . . . . 7
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘))}) |
105 | 65, 67, 104 | 3eqtr4rd 2788 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))) = {((reverse‘𝑃)‘𝑘)}) |
106 | 42, 105 | eqtrd 2777 |
. . . . 5
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = {((reverse‘𝑃)‘𝑘)}) |
107 | 85 | notbid 321 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (¬ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)) ↔ ¬ (𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)))) |
108 | 101 | simprd 499 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (¬ (𝑃‘(((♯‘𝑃) − 2) − 𝑘)) = (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1)) → {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))))) |
109 | 107, 108 | sylbid 243 |
. . . . . . 7
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → (¬ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)) → {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘))))) |
110 | 109 | imp 410 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ¬ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))} ⊆ ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))) |
111 | | prcom 4648 |
. . . . . . . 8
⊢
{((reverse‘𝑃)‘(𝑘 + 1)), ((reverse‘𝑃)‘𝑘)} = {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} |
112 | 63, 83 | preq12d 4657 |
. . . . . . . 8
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → {((reverse‘𝑃)‘(𝑘 + 1)), ((reverse‘𝑃)‘𝑘)} = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))}) |
113 | 111, 112 | eqtr3id 2792 |
. . . . . . 7
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))}) |
114 | 113 | adantr 484 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ¬ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} = {(𝑃‘(((♯‘𝑃) − 2) − 𝑘)), (𝑃‘((((♯‘𝑃) − 2) − 𝑘) + 1))}) |
115 | 41 | adantr 484 |
. . . . . 6
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ¬ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = ((iEdg‘𝐺)‘(𝐹‘(((♯‘𝑃) − 2) − 𝑘)))) |
116 | 110, 114,
115 | 3sstr4d 3948 |
. . . . 5
⊢ (((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) ∧ ¬ ((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1))) → {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘))) |
117 | 106, 116 | ifpimpda 1083 |
. . . 4
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈ (0..^(♯‘𝐹))) → if-(((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)), ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = {((reverse‘𝑃)‘𝑘)}, {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)))) |
118 | 28, 117 | syldan 594 |
. . 3
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝑘 ∈
(0..^(♯‘(reverse‘𝐹)))) → if-(((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)), ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = {((reverse‘𝑃)‘𝑘)}, {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)))) |
119 | 118 | ralrimiva 3105 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈
(0..^(♯‘(reverse‘𝐹)))if-(((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)), ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = {((reverse‘𝑃)‘𝑘)}, {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)))) |
120 | | wlkv 27700 |
. . . 4
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) |
121 | 120 | simp1d 1144 |
. . 3
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐺 ∈ V) |
122 | 5, 1 | iswlkg 27701 |
. . 3
⊢ (𝐺 ∈ V →
((reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃) ↔ ((reverse‘𝐹) ∈ Word dom (iEdg‘𝐺) ∧ (reverse‘𝑃):(0...(♯‘(reverse‘𝐹)))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘(reverse‘𝐹)))if-(((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)), ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = {((reverse‘𝑃)‘𝑘)}, {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)))))) |
123 | 121, 122 | syl 17 |
. 2
⊢ (𝐹(Walks‘𝐺)𝑃 → ((reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃) ↔ ((reverse‘𝐹) ∈ Word dom (iEdg‘𝐺) ∧ (reverse‘𝑃):(0...(♯‘(reverse‘𝐹)))⟶(Vtx‘𝐺) ∧ ∀𝑘 ∈
(0..^(♯‘(reverse‘𝐹)))if-(((reverse‘𝑃)‘𝑘) = ((reverse‘𝑃)‘(𝑘 + 1)), ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)) = {((reverse‘𝑃)‘𝑘)}, {((reverse‘𝑃)‘𝑘), ((reverse‘𝑃)‘(𝑘 + 1))} ⊆ ((iEdg‘𝐺)‘((reverse‘𝐹)‘𝑘)))))) |
124 | 4, 25, 119, 123 | mpbir3and 1344 |
1
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)) |