Metamath Proof Explorer

Theorem revwlk

Description: The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023)

Ref Expression
Assertion revwlk ⊢FWalks⁡GP→reverse⁡FWalks⁡Greverse⁡P

Proof

Step Hyp Ref Expression
1 eqid ⊢iEdg⁡G=iEdg⁡G
2 1 wlkf ⊢FWalks⁡GP→F∈Worddom⁡iEdg⁡G
3 revcl ⊢F∈Worddom⁡iEdg⁡G→reverse⁡F∈Worddom⁡iEdg⁡G
4 2 3 syl ⊢FWalks⁡GP→reverse⁡F∈Worddom⁡iEdg⁡G
5 eqid ⊢Vtx⁡G=Vtx⁡G
6 5 wlkpwrd ⊢FWalks⁡GP→P∈WordVtx⁡G
7 revcl ⊢P∈WordVtx⁡G→reverse⁡P∈WordVtx⁡G
8 wrdf ⊢reverse⁡P∈WordVtx⁡G→reverse⁡P:0..^reverse⁡P⟶Vtx⁡G
9 6 7 8 3syl ⊢FWalks⁡GP→reverse⁡P:0..^reverse⁡P⟶Vtx⁡G
10 revlen ⊢F∈Worddom⁡iEdg⁡G→reverse⁡F=F
11 2 10 syl ⊢FWalks⁡GP→reverse⁡F=F
12 11 oveq2d ⊢FWalks⁡GP→0…reverse⁡F=0…F
13 wlklenvp1 ⊢FWalks⁡GP→P=F+1
14 13 oveq2d ⊢FWalks⁡GP→0..^P=0..^F+1
15 revlen ⊢P∈WordVtx⁡G→reverse⁡P=P
16 6 15 syl ⊢FWalks⁡GP→reverse⁡P=P
17 16 oveq2d ⊢FWalks⁡GP→0..^reverse⁡P=0..^P
18 wlkcl ⊢FWalks⁡GP→F∈ℕ0
19 18 nn0zd ⊢FWalks⁡GP→F∈ℤ
20 fzval3 ⊢F∈ℤ→0…F=0..^F+1
21 19 20 syl ⊢FWalks⁡GP→0…F=0..^F+1
22 14 17 21 3eqtr4rd ⊢FWalks⁡GP→0…F=0..^reverse⁡P
23 12 22 eqtrd ⊢FWalks⁡GP→0…reverse⁡F=0..^reverse⁡P
24 23 feq2d ⊢FWalks⁡GP→reverse⁡P:0…reverse⁡F⟶Vtx⁡G↔reverse⁡P:0..^reverse⁡P⟶Vtx⁡G
25 9 24 mpbird ⊢FWalks⁡GP→reverse⁡P:0…reverse⁡F⟶Vtx⁡G
26 11 oveq2d ⊢FWalks⁡GP→0..^reverse⁡F=0..^F
27 26 eleq2d ⊢FWalks⁡GP→k∈0..^reverse⁡F↔k∈0..^F
28 27 biimpa ⊢FWalks⁡GP∧k∈0..^reverse⁡F→k∈0..^F
29 revfv ⊢F∈Worddom⁡iEdg⁡G∧k∈0..^F→reverse⁡F⁡k=F⁡F-1-k
30 2 29 sylan ⊢FWalks⁡GP∧k∈0..^F→reverse⁡F⁡k=F⁡F-1-k
31 wlklenvm1 ⊢FWalks⁡GP→F=P−1
32 31 oveq1d ⊢FWalks⁡GP→F−1=P-1-1
33 lencl ⊢P∈WordVtx⁡G→P∈ℕ0
34 33 nn0cnd ⊢P∈WordVtx⁡G→P∈ℂ
35 sub1m1 ⊢P∈ℂ→P-1-1=P−2
36 6 34 35 3syl ⊢FWalks⁡GP→P-1-1=P−2
37 32 36 eqtrd ⊢FWalks⁡GP→F−1=P−2
38 37 fvoveq1d ⊢FWalks⁡GP→F⁡F-1-k=F⁡P-2-k
39 38 adantr ⊢FWalks⁡GP∧k∈0..^F→F⁡F-1-k=F⁡P-2-k
40 30 39 eqtrd ⊢FWalks⁡GP∧k∈0..^F→reverse⁡F⁡k=F⁡P-2-k
41 40 fveq2d ⊢FWalks⁡GP∧k∈0..^F→iEdg⁡G⁡reverse⁡F⁡k=iEdg⁡G⁡F⁡P-2-k
42 41 adantr ⊢FWalks⁡GP∧k∈0..^F∧reverse⁡P⁡k=reverse⁡P⁡k+1→iEdg⁡G⁡reverse⁡F⁡k=iEdg⁡G⁡F⁡P-2-k
43 fzonn0p1p1 ⊢k∈0..^F→k+1∈0..^F+1
44 43 adantl ⊢FWalks⁡GP∧k∈0..^F→k+1∈0..^F+1
45 14 adantr ⊢FWalks⁡GP∧k∈0..^F→0..^P=0..^F+1
46 44 45 eleqtrrd ⊢FWalks⁡GP∧k∈0..^F→k+1∈0..^P
47 revfv ⊢P∈WordVtx⁡G∧k+1∈0..^P→reverse⁡P⁡k+1=P⁡P-1-k+1
48 6 46 47 syl2an2r ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k+1=P⁡P-1-k+1
49 elfzoelz ⊢k∈0..^F→k∈ℤ
50 49 zcnd ⊢k∈0..^F→k∈ℂ
51 50 adantl ⊢FWalks⁡GP∧k∈0..^F→k∈ℂ
52 1cnd ⊢FWalks⁡GP∧k∈0..^F→1∈ℂ
53 51 52 addcomd ⊢FWalks⁡GP∧k∈0..^F→k+1=1+k
54 53 oveq2d ⊢FWalks⁡GP∧k∈0..^F→P-1-k+1=P-1-1+k
55 6 34 syl ⊢FWalks⁡GP→P∈ℂ
56 55 adantr ⊢FWalks⁡GP∧k∈0..^F→P∈ℂ
57 56 52 subcld ⊢FWalks⁡GP∧k∈0..^F→P−1∈ℂ
58 57 52 51 subsub4d ⊢FWalks⁡GP∧k∈0..^F→P−1-1-k=P-1-1+k
59 36 oveq1d ⊢FWalks⁡GP→P−1-1-k=P-2-k
60 59 adantr ⊢FWalks⁡GP∧k∈0..^F→P−1-1-k=P-2-k
61 54 58 60 3eqtr2d ⊢FWalks⁡GP∧k∈0..^F→P-1-k+1=P-2-k
62 61 fveq2d ⊢FWalks⁡GP∧k∈0..^F→P⁡P-1-k+1=P⁡P-2-k
63 48 62 eqtrd ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k+1=P⁡P-2-k
64 63 sneqd ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k+1=P⁡P-2-k
65 64 adantr ⊢FWalks⁡GP∧k∈0..^F∧reverse⁡P⁡k=reverse⁡P⁡k+1→reverse⁡P⁡k+1=P⁡P-2-k
66 sneq ⊢reverse⁡P⁡k=reverse⁡P⁡k+1→reverse⁡P⁡k=reverse⁡P⁡k+1
67 66 adantl ⊢FWalks⁡GP∧k∈0..^F∧reverse⁡P⁡k=reverse⁡P⁡k+1→reverse⁡P⁡k=reverse⁡P⁡k+1
68 eqcom ⊢reverse⁡P⁡k=reverse⁡P⁡k+1↔reverse⁡P⁡k+1=reverse⁡P⁡k
69 fzossfzop1 ⊢F∈ℕ0→0..^F⊆0..^F+1
70 18 69 syl ⊢FWalks⁡GP→0..^F⊆0..^F+1
71 70 14 sseqtrrd ⊢FWalks⁡GP→0..^F⊆0..^P
72 71 sselda ⊢FWalks⁡GP∧k∈0..^F→k∈0..^P
73 revfv ⊢P∈WordVtx⁡G∧k∈0..^P→reverse⁡P⁡k=P⁡P-1-k
74 6 72 73 syl2an2r ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k=P⁡P-1-k
75 57 51 52 sub32d ⊢FWalks⁡GP∧k∈0..^F→P−1-k-1=P−1-1-k
76 75 oveq1d ⊢FWalks⁡GP∧k∈0..^F→P-1-k-1+1=P-1-1-k+1
77 57 51 subcld ⊢FWalks⁡GP∧k∈0..^F→P-1-k∈ℂ
78 77 52 npcand ⊢FWalks⁡GP∧k∈0..^F→P-1-k-1+1=P-1-k
79 59 oveq1d ⊢FWalks⁡GP→P-1-1-k+1=P−2-k+1
80 79 adantr ⊢FWalks⁡GP∧k∈0..^F→P-1-1-k+1=P−2-k+1
81 76 78 80 3eqtr3d ⊢FWalks⁡GP∧k∈0..^F→P-1-k=P−2-k+1
82 81 fveq2d ⊢FWalks⁡GP∧k∈0..^F→P⁡P-1-k=P⁡P−2-k+1
83 74 82 eqtrd ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k=P⁡P−2-k+1
84 63 83 eqeq12d ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k+1=reverse⁡P⁡k↔P⁡P-2-k=P⁡P−2-k+1
85 68 84 syl5bb ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k=reverse⁡P⁡k+1↔P⁡P-2-k=P⁡P−2-k+1
86 wkslem1 ⊢x=P-2-k→if-P⁡x=P⁡x+1iEdg⁡G⁡F⁡x=P⁡xP⁡xP⁡x+1⊆iEdg⁡G⁡F⁡x↔if-P⁡P-2-k=P⁡P−2-k+1iEdg⁡G⁡F⁡P-2-k=P⁡P-2-kP⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k
87 5 1 wlkprop ⊢FWalks⁡GP→F∈Worddom⁡iEdg⁡G∧P:0…F⟶Vtx⁡G∧∀x∈0..^Fif-P⁡x=P⁡x+1iEdg⁡G⁡F⁡x=P⁡xP⁡xP⁡x+1⊆iEdg⁡G⁡F⁡x
88 87 simp3d ⊢FWalks⁡GP→∀x∈0..^Fif-P⁡x=P⁡x+1iEdg⁡G⁡F⁡x=P⁡xP⁡xP⁡x+1⊆iEdg⁡G⁡F⁡x
89 88 adantr ⊢FWalks⁡GP∧k∈0..^F→∀x∈0..^Fif-P⁡x=P⁡x+1iEdg⁡G⁡F⁡x=P⁡xP⁡xP⁡x+1⊆iEdg⁡G⁡F⁡x
90 18 nn0cnd ⊢FWalks⁡GP→F∈ℂ
91 90 adantr ⊢FWalks⁡GP∧k∈0..^F→F∈ℂ
92 91 51 52 sub32d ⊢FWalks⁡GP∧k∈0..^F→F-k-1=F-1-k
93 37 adantr ⊢FWalks⁡GP∧k∈0..^F→F−1=P−2
94 93 oveq1d ⊢FWalks⁡GP∧k∈0..^F→F-1-k=P-2-k
95 92 94 eqtrd ⊢FWalks⁡GP∧k∈0..^F→F-k-1=P-2-k
96 ubmelm1fzo ⊢k∈0..^F→F-k-1∈0..^F
97 96 adantl ⊢FWalks⁡GP∧k∈0..^F→F-k-1∈0..^F
98 95 97 eqeltrrd ⊢FWalks⁡GP∧k∈0..^F→P-2-k∈0..^F
99 86 89 98 rspcdva ⊢FWalks⁡GP∧k∈0..^F→if-P⁡P-2-k=P⁡P−2-k+1iEdg⁡G⁡F⁡P-2-k=P⁡P-2-kP⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k
100 dfifp2 ⊢if-P⁡P-2-k=P⁡P−2-k+1iEdg⁡G⁡F⁡P-2-k=P⁡P-2-kP⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k↔P⁡P-2-k=P⁡P−2-k+1→iEdg⁡G⁡F⁡P-2-k=P⁡P-2-k∧¬P⁡P-2-k=P⁡P−2-k+1→P⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k
101 99 100 sylib ⊢FWalks⁡GP∧k∈0..^F→P⁡P-2-k=P⁡P−2-k+1→iEdg⁡G⁡F⁡P-2-k=P⁡P-2-k∧¬P⁡P-2-k=P⁡P−2-k+1→P⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k
102 101 simpld ⊢FWalks⁡GP∧k∈0..^F→P⁡P-2-k=P⁡P−2-k+1→iEdg⁡G⁡F⁡P-2-k=P⁡P-2-k
103 85 102 sylbid ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k=reverse⁡P⁡k+1→iEdg⁡G⁡F⁡P-2-k=P⁡P-2-k
104 103 imp ⊢FWalks⁡GP∧k∈0..^F∧reverse⁡P⁡k=reverse⁡P⁡k+1→iEdg⁡G⁡F⁡P-2-k=P⁡P-2-k
105 65 67 104 3eqtr4rd ⊢FWalks⁡GP∧k∈0..^F∧reverse⁡P⁡k=reverse⁡P⁡k+1→iEdg⁡G⁡F⁡P-2-k=reverse⁡P⁡k
106 42 105 eqtrd ⊢FWalks⁡GP∧k∈0..^F∧reverse⁡P⁡k=reverse⁡P⁡k+1→iEdg⁡G⁡reverse⁡F⁡k=reverse⁡P⁡k
107 85 notbid ⊢FWalks⁡GP∧k∈0..^F→¬reverse⁡P⁡k=reverse⁡P⁡k+1↔¬P⁡P-2-k=P⁡P−2-k+1
108 101 simprd ⊢FWalks⁡GP∧k∈0..^F→¬P⁡P-2-k=P⁡P−2-k+1→P⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k
109 107 108 sylbid ⊢FWalks⁡GP∧k∈0..^F→¬reverse⁡P⁡k=reverse⁡P⁡k+1→P⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k
110 109 imp ⊢FWalks⁡GP∧k∈0..^F∧¬reverse⁡P⁡k=reverse⁡P⁡k+1→P⁡P-2-kP⁡P−2-k+1⊆iEdg⁡G⁡F⁡P-2-k
111 prcom ⊢reverse⁡P⁡k+1reverse⁡P⁡k=reverse⁡P⁡kreverse⁡P⁡k+1
112 63 83 preq12d ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡k+1reverse⁡P⁡k=P⁡P-2-kP⁡P−2-k+1
113 111 112 eqtr3id ⊢FWalks⁡GP∧k∈0..^F→reverse⁡P⁡kreverse⁡P⁡k+1=P⁡P-2-kP⁡P−2-k+1
114 113 adantr ⊢FWalks⁡GP∧k∈0..^F∧¬reverse⁡P⁡k=reverse⁡P⁡k+1→reverse⁡P⁡kreverse⁡P⁡k+1=P⁡P-2-kP⁡P−2-k+1
115 41 adantr ⊢FWalks⁡GP∧k∈0..^F∧¬reverse⁡P⁡k=reverse⁡P⁡k+1→iEdg⁡G⁡reverse⁡F⁡k=iEdg⁡G⁡F⁡P-2-k
116 110 114 115 3sstr4d ⊢FWalks⁡GP∧k∈0..^F∧¬reverse⁡P⁡k=reverse⁡P⁡k+1→reverse⁡P⁡kreverse⁡P⁡k+1⊆iEdg⁡G⁡reverse⁡F⁡k
117 106 116 ifpimpda ⊢FWalks⁡GP∧k∈0..^F→if-reverse⁡P⁡k=reverse⁡P⁡k+1iEdg⁡G⁡reverse⁡F⁡k=reverse⁡P⁡kreverse⁡P⁡kreverse⁡P⁡k+1⊆iEdg⁡G⁡reverse⁡F⁡k
118 28 117 syldan ⊢FWalks⁡GP∧k∈0..^reverse⁡F→if-reverse⁡P⁡k=reverse⁡P⁡k+1iEdg⁡G⁡reverse⁡F⁡k=reverse⁡P⁡kreverse⁡P⁡kreverse⁡P⁡k+1⊆iEdg⁡G⁡reverse⁡F⁡k
119 118 ralrimiva ⊢FWalks⁡GP→∀k∈0..^reverse⁡Fif-reverse⁡P⁡k=reverse⁡P⁡k+1iEdg⁡G⁡reverse⁡F⁡k=reverse⁡P⁡kreverse⁡P⁡kreverse⁡P⁡k+1⊆iEdg⁡G⁡reverse⁡F⁡k
120 wlkv ⊢FWalks⁡GP→G∈V∧F∈V∧P∈V
121 120 simp1d ⊢FWalks⁡GP→G∈V
122 5 1 iswlkg ⊢G∈V→reverse⁡FWalks⁡Greverse⁡P↔reverse⁡F∈Worddom⁡iEdg⁡G∧reverse⁡P:0…reverse⁡F⟶Vtx⁡G∧∀k∈0..^reverse⁡Fif-reverse⁡P⁡k=reverse⁡P⁡k+1iEdg⁡G⁡reverse⁡F⁡k=reverse⁡P⁡kreverse⁡P⁡kreverse⁡P⁡k+1⊆iEdg⁡G⁡reverse⁡F⁡k
123 121 122 syl ⊢FWalks⁡GP→reverse⁡FWalks⁡Greverse⁡P↔reverse⁡F∈Worddom⁡iEdg⁡G∧reverse⁡P:0…reverse⁡F⟶Vtx⁡G∧∀k∈0..^reverse⁡Fif-reverse⁡P⁡k=reverse⁡P⁡k+1iEdg⁡G⁡reverse⁡F⁡k=reverse⁡P⁡kreverse⁡P⁡kreverse⁡P⁡k+1⊆iEdg⁡G⁡reverse⁡F⁡k
124 4 25 119 123 mpbir3and ⊢FWalks⁡GP→reverse⁡FWalks⁡Greverse⁡P