Metamath Proof Explorer

Theorem isclwwlk

Description: Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Hypotheses clwwlk.v ⊢ V = Vtx ⁡ G
clwwlk.e ⊢ E = Edg ⁡ G
Assertion isclwwlk ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E

Proof

Step Hyp Ref Expression
1 clwwlk.v ⊢ V = Vtx ⁡ G
2 clwwlk.e ⊢ E = Edg ⁡ G
3 neeq1 ⊢ w = W → w ≠ ∅ ↔ W ≠ ∅
4 fveq2 ⊢ w = W → w = W
5 4 oveq1d ⊢ w = W → w − 1 = W − 1
6 5 oveq2d ⊢ w = W → 0 ..^ w − 1 = 0 ..^ W − 1
7 fveq1 ⊢ w = W → w ⁡ i = W ⁡ i
8 fveq1 ⊢ w = W → w ⁡ i + 1 = W ⁡ i + 1
9 7 8 preq12d ⊢ w = W → w ⁡ i w ⁡ i + 1 = W ⁡ i W ⁡ i + 1
10 9 eleq1d ⊢ w = W → w ⁡ i w ⁡ i + 1 ∈ E ↔ W ⁡ i W ⁡ i + 1 ∈ E
11 6 10 raleqbidv ⊢ w = W → ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ↔ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
12 fveq2 ⊢ w = W → lastS ⁡ w = lastS ⁡ W
13 fveq1 ⊢ w = W → w ⁡ 0 = W ⁡ 0
14 12 13 preq12d ⊢ w = W → lastS ⁡ w w ⁡ 0 = lastS ⁡ W W ⁡ 0
15 14 eleq1d ⊢ w = W → lastS ⁡ w w ⁡ 0 ∈ E ↔ lastS ⁡ W W ⁡ 0 ∈ E
16 3 11 15 3anbi123d ⊢ w = W → w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E ↔ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
17 16 elrab ⊢ W ∈ w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
18 1 2 clwwlk ⊢ ClWWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
19 18 eleq2i ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
20 3anass ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
21 anass ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
22 3anass ⊢ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
23 22 bicomi ⊢ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
24 23 anbi2i ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
25 20 21 24 3bitri ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
26 17 19 25 3bitr4i ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E