Database
GRAPH THEORY
Walks, paths and cycles
Circuits and cycles
crctcshlem2
Next ⟩
crctcshlem3
Metamath Proof Explorer
Ascii
Unicode
Theorem
crctcshlem2
Description:
Lemma for
crctcsh
.
(Contributed by
AV
, 10-Mar-2021)
Ref
Expression
Hypotheses
crctcsh.v
⊢
V
=
Vtx
⁡
G
crctcsh.i
⊢
I
=
iEdg
⁡
G
crctcsh.d
⊢
φ
→
F
Circuits
⁡
G
P
crctcsh.n
⊢
N
=
F
crctcsh.s
⊢
φ
→
S
∈
0
..^
N
crctcsh.h
⊢
H
=
F
cyclShift
S
Assertion
crctcshlem2
⊢
φ
→
H
=
N
Proof
Step
Hyp
Ref
Expression
1
crctcsh.v
⊢
V
=
Vtx
⁡
G
2
crctcsh.i
⊢
I
=
iEdg
⁡
G
3
crctcsh.d
⊢
φ
→
F
Circuits
⁡
G
P
4
crctcsh.n
⊢
N
=
F
5
crctcsh.s
⊢
φ
→
S
∈
0
..^
N
6
crctcsh.h
⊢
H
=
F
cyclShift
S
7
crctiswlk
⊢
F
Circuits
⁡
G
P
→
F
Walks
⁡
G
P
8
2
wlkf
⊢
F
Walks
⁡
G
P
→
F
∈
Word
dom
⁡
I
9
3
7
8
3syl
⊢
φ
→
F
∈
Word
dom
⁡
I
10
elfzoelz
⊢
S
∈
0
..^
N
→
S
∈
ℤ
11
5
10
syl
⊢
φ
→
S
∈
ℤ
12
cshwlen
⊢
F
∈
Word
dom
⁡
I
∧
S
∈
ℤ
→
F
cyclShift
S
=
F
13
9
11
12
syl2anc
⊢
φ
→
F
cyclShift
S
=
F
14
6
fveq2i
⊢
H
=
F
cyclShift
S
15
13
14
4
3eqtr4g
⊢
φ
→
H
=
N