# Metamath Proof Explorer

## Theorem clwwlknonel

Description: Characterization of a word over the set of vertices representing a closed walk on vertex X of (nonzero) length N in a graph G . This theorem would not hold for N = 0 if W = X = (/) . (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 24-Mar-2022)

Ref Expression
Hypotheses clwwlknonel.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
clwwlknonel.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
Assertion clwwlknonel ${⊢}{N}\ne 0\to \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 clwwlknonel.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 clwwlknonel.e ${⊢}{E}=\mathrm{Edg}\left({G}\right)$
3 1 2 isclwwlk ${⊢}{W}\in \mathrm{ClWWalks}\left({G}\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)$
4 simpl ${⊢}\left(\left|{W}\right|={N}\wedge {W}=\varnothing \right)\to \left|{W}\right|={N}$
5 fveq2 ${⊢}{W}=\varnothing \to \left|{W}\right|=\left|\varnothing \right|$
6 hash0 ${⊢}\left|\varnothing \right|=0$
7 5 6 syl6eq ${⊢}{W}=\varnothing \to \left|{W}\right|=0$
8 7 adantl ${⊢}\left(\left|{W}\right|={N}\wedge {W}=\varnothing \right)\to \left|{W}\right|=0$
9 4 8 eqtr3d ${⊢}\left(\left|{W}\right|={N}\wedge {W}=\varnothing \right)\to {N}=0$
10 9 ex ${⊢}\left|{W}\right|={N}\to \left({W}=\varnothing \to {N}=0\right)$
11 10 necon3d ${⊢}\left|{W}\right|={N}\to \left({N}\ne 0\to {W}\ne \varnothing \right)$
12 11 impcom ${⊢}\left({N}\ne 0\wedge \left|{W}\right|={N}\right)\to {W}\ne \varnothing$
13 12 biantrud ${⊢}\left({N}\ne 0\wedge \left|{W}\right|={N}\right)\to \left({W}\in \mathrm{Word}{V}↔\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\right)$
14 13 bicomd ${⊢}\left({N}\ne 0\wedge \left|{W}\right|={N}\right)\to \left(\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)↔{W}\in \mathrm{Word}{V}\right)$
15 14 3anbi1d ${⊢}\left({N}\ne 0\wedge \left|{W}\right|={N}\right)\to \left(\left(\left({W}\in \mathrm{Word}{V}\wedge {W}\ne \varnothing \right)\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)↔\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\right)$
16 3 15 syl5bb ${⊢}\left({N}\ne 0\wedge \left|{W}\right|={N}\right)\to \left({W}\in \mathrm{ClWWalks}\left({G}\right)↔\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\right)$
17 16 a1d ${⊢}\left({N}\ne 0\wedge \left|{W}\right|={N}\right)\to \left({W}\left(0\right)={X}\to \left({W}\in \mathrm{ClWWalks}\left({G}\right)↔\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\right)\right)$
18 17 expimpd ${⊢}{N}\ne 0\to \left(\left(\left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\to \left({W}\in \mathrm{ClWWalks}\left({G}\right)↔\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\right)\right)$
19 18 pm5.32rd ${⊢}{N}\ne 0\to \left(\left({W}\in \mathrm{ClWWalks}\left({G}\right)\wedge \left(\left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left(\left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\right)\right)$
20 isclwwlknon ${⊢}{W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)↔\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {W}\left(0\right)={X}\right)$
21 isclwwlkn ${⊢}{W}\in \left({N}\mathrm{ClWWalksN}{G}\right)↔\left({W}\in \mathrm{ClWWalks}\left({G}\right)\wedge \left|{W}\right|={N}\right)$
22 21 anbi1i ${⊢}\left({W}\in \left({N}\mathrm{ClWWalksN}{G}\right)\wedge {W}\left(0\right)={X}\right)↔\left(\left({W}\in \mathrm{ClWWalks}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge {W}\left(0\right)={X}\right)$
23 anass ${⊢}\left(\left({W}\in \mathrm{ClWWalks}\left({G}\right)\wedge \left|{W}\right|={N}\right)\wedge {W}\left(0\right)={X}\right)↔\left({W}\in \mathrm{ClWWalks}\left({G}\right)\wedge \left(\left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\right)$
24 20 22 23 3bitri ${⊢}{W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)↔\left({W}\in \mathrm{ClWWalks}\left({G}\right)\wedge \left(\left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\right)$
25 3anass ${⊢}\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left(\left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\right)$
26 19 24 25 3bitr4g ${⊢}{N}\ne 0\to \left({W}\in \left({X}\mathrm{ClWWalksNOn}\left({G}\right){N}\right)↔\left(\left({W}\in \mathrm{Word}{V}\wedge \forall {i}\in \left(0..^\left|{W}\right|-1\right)\phantom{\rule{.4em}{0ex}}\left\{{W}\left({i}\right),{W}\left({i}+1\right)\right\}\in {E}\wedge \left\{\mathrm{lastS}\left({W}\right),{W}\left(0\right)\right\}\in {E}\right)\wedge \left|{W}\right|={N}\wedge {W}\left(0\right)={X}\right)\right)$