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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	extwwlkfab.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
	extwwlkfab.f	⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
Assertion	extwwlkfabel	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		extwwlkfab.c	⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3		extwwlkfab.f	⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4	1 2 3	extwwlkfab	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) = { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } )
5	4	eleq2d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ 𝑊 ∈ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } ) )
6		oveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 prefix ( 𝑁 − 2 ) ) = ( 𝑊 prefix ( 𝑁 − 2 ) ) )
7	6	eleq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ↔ ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ) )
8		fveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ ( 𝑁 − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) )
9	8	eleq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
10		fveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ ( 𝑁 − 2 ) ) )
11	10	eqeq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ↔ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
12	7 9 11	3anbi123d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
13	12	elrab	⊢ ( 𝑊 ∈ { 𝑤 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∣ ( ( 𝑤 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑤 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑤 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) } ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
14	5 13	bitrdi	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )