Database
GRAPH THEORY
Walks, paths and cycles
Closed walks as words
Closed walks as words
clwlkclwwlklem2a3
Next ⟩
clwlkclwwlklem2fv1
Metamath Proof Explorer
Ascii
Unicode
Theorem
clwlkclwwlklem2a3
Description:
Lemma 3 for
clwlkclwwlklem2a
.
(Contributed by
Alexander van der Vekens
, 21-Jun-2018)
Ref
Expression
Hypothesis
clwlkclwwlklem2.f
⊢
F
=
x
∈
0
..^
P
−
1
⟼
if
x
<
P
−
2
E
-1
⁡
P
⁡
x
P
⁡
x
+
1
E
-1
⁡
P
⁡
x
P
⁡
0
Assertion
clwlkclwwlklem2a3
⊢
P
∈
Word
V
∧
2
≤
P
→
P
⁡
F
=
lastS
⁡
P
Proof
Step
Hyp
Ref
Expression
1
clwlkclwwlklem2.f
⊢
F
=
x
∈
0
..^
P
−
1
⟼
if
x
<
P
−
2
E
-1
⁡
P
⁡
x
P
⁡
x
+
1
E
-1
⁡
P
⁡
x
P
⁡
0
2
lsw
⊢
P
∈
Word
V
→
lastS
⁡
P
=
P
⁡
P
−
1
3
2
adantr
⊢
P
∈
Word
V
∧
2
≤
P
→
lastS
⁡
P
=
P
⁡
P
−
1
4
1
clwlkclwwlklem2a2
⊢
P
∈
Word
V
∧
2
≤
P
→
F
=
P
−
1
5
4
eqcomd
⊢
P
∈
Word
V
∧
2
≤
P
→
P
−
1
=
F
6
5
fveq2d
⊢
P
∈
Word
V
∧
2
≤
P
→
P
⁡
P
−
1
=
P
⁡
F
7
3
6
eqtr2d
⊢
P
∈
Word
V
∧
2
≤
P
→
P
⁡
F
=
lastS
⁡
P