Metamath Proof Explorer

Theorem extwwlkfabel

Description: Characterization of an element of the set ( X C N ) , i.e., a double loop of length N on vertex X with a construction from the set F of closed walks on X with length smaller by 2 than the fixed length by appending a neighbor of the last vertex and afterwards the last vertex (which is the first vertex) itself ("walking forth and back" from the last vertex). (Contributed by AV, 22-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v ⊢ V = Vtx ⁡ G
extwwlkfab.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
extwwlkfab.f ⊢ F = X ClWWalksNOn ⁡ G N − 2
Assertion extwwlkfabel ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ X C N ↔ W ∈ N ClWWalksN G ∧ W prefix N − 2 ∈ F ∧ W ⁡ N − 1 ∈ G NeighbVtx X ∧ W ⁡ N − 2 = X

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢ V = Vtx ⁡ G
2 extwwlkfab.c ⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v
3 extwwlkfab.f ⊢ F = X ClWWalksNOn ⁡ G N − 2
4 1 2 3 extwwlkfab ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X C N = w ∈ N ClWWalksN G | w prefix N − 2 ∈ F ∧ w ⁡ N − 1 ∈ G NeighbVtx X ∧ w ⁡ N − 2 = X
5 4 eleq2d ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ X C N ↔ W ∈ w ∈ N ClWWalksN G | w prefix N − 2 ∈ F ∧ w ⁡ N − 1 ∈ G NeighbVtx X ∧ w ⁡ N − 2 = X
6 oveq1 ⊢ w = W → w prefix N − 2 = W prefix N − 2
7 6 eleq1d ⊢ w = W → w prefix N − 2 ∈ F ↔ W prefix N − 2 ∈ F
8 fveq1 ⊢ w = W → w ⁡ N − 1 = W ⁡ N − 1
9 8 eleq1d ⊢ w = W → w ⁡ N − 1 ∈ G NeighbVtx X ↔ W ⁡ N − 1 ∈ G NeighbVtx X
10 fveq1 ⊢ w = W → w ⁡ N − 2 = W ⁡ N − 2
11 10 eqeq1d ⊢ w = W → w ⁡ N − 2 = X ↔ W ⁡ N − 2 = X
12 7 9 11 3anbi123d ⊢ w = W → w prefix N − 2 ∈ F ∧ w ⁡ N − 1 ∈ G NeighbVtx X ∧ w ⁡ N − 2 = X ↔ W prefix N − 2 ∈ F ∧ W ⁡ N − 1 ∈ G NeighbVtx X ∧ W ⁡ N − 2 = X
13 12 elrab ⊢ W ∈ w ∈ N ClWWalksN G | w prefix N − 2 ∈ F ∧ w ⁡ N − 1 ∈ G NeighbVtx X ∧ w ⁡ N − 2 = X ↔ W ∈ N ClWWalksN G ∧ W prefix N − 2 ∈ F ∧ W ⁡ N − 1 ∈ G NeighbVtx X ∧ W ⁡ N − 2 = X
14 5 13 bitrdi ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → W ∈ X C N ↔ W ∈ N ClWWalksN G ∧ W prefix N − 2 ∈ F ∧ W ⁡ N − 1 ∈ G NeighbVtx X ∧ W ⁡ N − 2 = X