Database
GRAPH THEORY
Walks, paths and cycles
Closed walks as words
Closed walks on a vertex of a fixed length as words
clwwlknon0
Next ⟩
clwwlknonfin
Metamath Proof Explorer
Ascii
Unicode
Theorem
clwwlknon0
Description:
Sufficient conditions for
ClWWalksNOn
to be empty.
(Contributed by
AV
, 25-Mar-2022)
Ref
Expression
Assertion
clwwlknon0
⊢
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
→
X
ClWWalksNOn
⁡
G
N
=
∅
Proof
Step
Hyp
Ref
Expression
1
oveq2
⊢
N
=
0
→
X
ClWWalksNOn
⁡
G
N
=
X
ClWWalksNOn
⁡
G
0
2
clwwlk0on0
⊢
X
ClWWalksNOn
⁡
G
0
=
∅
3
1
2
eqtrdi
⊢
N
=
0
→
X
ClWWalksNOn
⁡
G
N
=
∅
4
3
a1d
⊢
N
=
0
→
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
→
X
ClWWalksNOn
⁡
G
N
=
∅
5
simprl
⊢
N
≠
0
∧
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
0
→
X
∈
Vtx
⁡
G
6
elnnne0
⊢
N
∈
ℕ
↔
N
∈
ℕ
0
∧
N
≠
0
7
6
simplbi2
⊢
N
∈
ℕ
0
→
N
≠
0
→
N
∈
ℕ
8
7
adantl
⊢
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
0
→
N
≠
0
→
N
∈
ℕ
9
8
impcom
⊢
N
≠
0
∧
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
0
→
N
∈
ℕ
10
5
9
jca
⊢
N
≠
0
∧
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
0
→
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
11
10
stoic1a
⊢
N
≠
0
∧
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
→
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
0
12
clwwlknonmpo
⊢
ClWWalksNOn
⁡
G
=
v
∈
Vtx
⁡
G
,
n
∈
ℕ
0
⟼
w
∈
n
ClWWalksN
G
|
w
⁡
0
=
v
13
12
mpondm0
⊢
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
0
→
X
ClWWalksNOn
⁡
G
N
=
∅
14
11
13
syl
⊢
N
≠
0
∧
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
→
X
ClWWalksNOn
⁡
G
N
=
∅
15
14
ex
⊢
N
≠
0
→
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
→
X
ClWWalksNOn
⁡
G
N
=
∅
16
4
15
pm2.61ine
⊢
¬
X
∈
Vtx
⁡
G
∧
N
∈
ℕ
→
X
ClWWalksNOn
⁡
G
N
=
∅