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∈vClWWalksNOn⁡Gn|w⁡n−2=v
extwwlkfab.f ⊢F=XClWWalksNOn⁡GN−2
Assertion extwwlkfabel ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→W∈XCN↔W∈NClWWalksNG∧WprefixN−2∈F∧W⁡N−1∈GNeighbVtxX∧W⁡N−2=X

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢V=Vtx⁡G
2 extwwlkfab.c ⊢C=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2=v
3 extwwlkfab.f ⊢F=XClWWalksNOn⁡GN−2
4 1 2 3 extwwlkfab ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→XCN=w∈NClWWalksNG|wprefixN−2∈F∧w⁡N−1∈GNeighbVtxX∧w⁡N−2=X
5 4 eleq2d ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→W∈XCN↔W∈w∈NClWWalksNG|wprefixN−2∈F∧w⁡N−1∈GNeighbVtxX∧w⁡N−2=X
6 oveq1 ⊢w=W→wprefixN−2=WprefixN−2
7 6 eleq1d ⊢w=W→wprefixN−2∈F↔WprefixN−2∈F
8 fveq1 ⊢w=W→w⁡N−1=W⁡N−1
9 8 eleq1d ⊢w=W→w⁡N−1∈GNeighbVtxX↔W⁡N−1∈GNeighbVtxX
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→wprefixN−2∈F∧w⁡N−1∈GNeighbVtxX∧w⁡N−2=X↔WprefixN−2∈F∧W⁡N−1∈GNeighbVtxX∧W⁡N−2=X
13 12 elrab ⊢W∈w∈NClWWalksNG|wprefixN−2∈F∧w⁡N−1∈GNeighbVtxX∧w⁡N−2=X↔W∈NClWWalksNG∧WprefixN−2∈F∧W⁡N−1∈GNeighbVtxX∧W⁡N−2=X
14 5 13 bitrdi ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→W∈XCN↔W∈NClWWalksNG∧WprefixN−2∈F∧W⁡N−1∈GNeighbVtxX∧W⁡N−2=X