Metamath Proof Explorer

Theorem iswwlks

Description: A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 wwlks.v ⊢ V = Vtx ⁡ G
2 wwlks.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 3 11 anbi12d ⊢ w = W → w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ↔ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
13 12 elrab ⊢ W ∈ w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
14 1 2 wwlks ⊢ WWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
15 14 eleq2i ⊢ W ∈ WWalks ⁡ G ↔ W ∈ w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
16 3anan12 ⊢ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
17 13 15 16 3bitr4i ⊢ W ∈ WWalks ⁡ G ↔ W ≠ ∅ ∧ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E