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 = Vtx ⁡ G
clwwlknonel.e ⊢ E = Edg ⁡ G
Assertion clwwlknonel ⊢ N ≠ 0 → W ∈ X ClWWalksNOn ⁡ G N ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N ∧ W ⁡ 0 = X

Proof

Step Hyp Ref Expression
1 clwwlknonel.v ⊢ V = Vtx ⁡ G
2 clwwlknonel.e ⊢ E = Edg ⁡ G
3 1 2 isclwwlk ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
4 simpl ⊢ W = N ∧ W = ∅ → W = N
5 fveq2 ⊢ W = ∅ → W = ∅
6 hash0 ⊢ ∅ = 0
7 5 6 eqtrdi ⊢ W = ∅ → W = 0
8 7 adantl ⊢ W = N ∧ W = ∅ → W = 0
9 4 8 eqtr3d ⊢ W = N ∧ W = ∅ → N = 0
10 9 ex ⊢ W = N → W = ∅ → N = 0
11 10 necon3d ⊢ W = N → N ≠ 0 → W ≠ ∅
12 11 impcom ⊢ N ≠ 0 ∧ W = N → W ≠ ∅
13 12 biantrud ⊢ N ≠ 0 ∧ W = N → W ∈ Word V ↔ W ∈ Word V ∧ W ≠ ∅
14 13 bicomd ⊢ N ≠ 0 ∧ W = N → W ∈ Word V ∧ W ≠ ∅ ↔ W ∈ Word V
15 14 3anbi1d ⊢ N ≠ 0 ∧ W = N → W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
16 3 15 bitrid ⊢ N ≠ 0 ∧ W = N → W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
17 16 a1d ⊢ N ≠ 0 ∧ W = N → W ⁡ 0 = X → W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
18 17 expimpd ⊢ N ≠ 0 → W = N ∧ W ⁡ 0 = X → W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
19 18 pm5.32rd ⊢ N ≠ 0 → W ∈ ClWWalks ⁡ G ∧ W = N ∧ W ⁡ 0 = X ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N ∧ W ⁡ 0 = X
20 isclwwlknon ⊢ W ∈ X ClWWalksNOn ⁡ G N ↔ W ∈ N ClWWalksN G ∧ W ⁡ 0 = X
21 isclwwlkn ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
22 21 anbi1i ⊢ W ∈ N ClWWalksN G ∧ W ⁡ 0 = X ↔ W ∈ ClWWalks ⁡ G ∧ W = N ∧ W ⁡ 0 = X
23 anass ⊢ W ∈ ClWWalks ⁡ G ∧ W = N ∧ W ⁡ 0 = X ↔ W ∈ ClWWalks ⁡ G ∧ W = N ∧ W ⁡ 0 = X
24 20 22 23 3bitri ⊢ W ∈ X ClWWalksNOn ⁡ G N ↔ W ∈ ClWWalks ⁡ G ∧ W = N ∧ W ⁡ 0 = X
25 3anass ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N ∧ W ⁡ 0 = X ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N ∧ W ⁡ 0 = X
26 19 24 25 3bitr4g ⊢ N ≠ 0 → W ∈ X ClWWalksNOn ⁡ G N ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N ∧ W ⁡ 0 = X