extwwlkfab

Description: The set ( X C N ) of double loops of length N on vertex X can be constructed 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). 3 <_ N is required since for N = 2 : F = ( X ( ClWWalksNOnG ) 0 ) = (/) (see clwwlk0on0 stating that a closed walk of length 0 is not represented as word), which would result in an empty set on the right hand side, but ( X C N ) needs not be empty, see 2clwwlk2 . (Contributed by Alexander van der Vekens, 18-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 31-Oct-2022)

	Ref	Expression
Hypotheses	extwwlkfab.v	$⊢ V = Vtx (G)$
	extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
	extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
Assertion	extwwlkfab	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to X C N = \{w \in (N ClWWalksN G) \| (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X)\}$

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	$⊢ V = Vtx (G)$
2		extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
3		extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
4		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
5	2	2clwwlk	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to X C N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
6	4 5	sylan2	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to X C N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
7	6	3adant1	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to X C N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
8		clwwlknon	$⊢ X ClWWalksNOn (G) N = \{w \in (N ClWWalksN G) \| w (0) = X\}$
9	8	rabeqi	$⊢ \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} = \{w \in \{w \in (N ClWWalksN G) \| w (0) = X\} \| w (N - 2) = X\}$
10		rabrab	$⊢ \{w \in \{w \in (N ClWWalksN G) \| w (0) = X\} \| w (N - 2) = X\} = \{w \in (N ClWWalksN G) \| (w (0) = X \land w (N - 2) = X)\}$
11		simpll3	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to N \in ℤ_{\geq 3}$
12		simplr	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to w \in (N ClWWalksN G)$
13		simpr	$⊢ (w (0) = X \land w (N - 2) = X) \to w (N - 2) = X$
14		simpl	$⊢ (w (0) = X \land w (N - 2) = X) \to w (0) = X$
15	14	eqcomd	$⊢ (w (0) = X \land w (N - 2) = X) \to X = w (0)$
16	13 15	eqtrd	$⊢ (w (0) = X \land w (N - 2) = X) \to w (N - 2) = w (0)$
17	16	adantl	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to w (N - 2) = w (0)$
18		clwwnrepclwwn	$⊢ (N \in ℤ_{\geq 3} \land w \in (N ClWWalksN G) \land w (N - 2) = w (0)) \to w prefix (N - 2) \in ((N - 2) ClWWalksN G)$
19	11 12 17 18	syl3anc	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to w prefix (N - 2) \in ((N - 2) ClWWalksN G)$
20	14	adantl	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to w (0) = X$
21	19 20	jca	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to (w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X)$
22		simp1	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to G \in USGraph$
23	22	anim1i	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to (G \in USGraph \land w \in (N ClWWalksN G))$
24	23	adantr	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to (G \in USGraph \land w \in (N ClWWalksN G))$
25		clwwlknlbonbgr1	$⊢ (G \in USGraph \land w \in (N ClWWalksN G)) \to w (N - 1) \in (G NeighbVtx w (0))$
26	24 25	syl	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to w (N - 1) \in (G NeighbVtx w (0))$
27		oveq2	$⊢ X = w (0) \to G NeighbVtx X = G NeighbVtx w (0)$
28	27	eqcoms	$⊢ w (0) = X \to G NeighbVtx X = G NeighbVtx w (0)$
29	28	adantr	$⊢ (w (0) = X \land w (N - 2) = X) \to G NeighbVtx X = G NeighbVtx w (0)$
30	29	adantl	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to G NeighbVtx X = G NeighbVtx w (0)$
31	26 30	eleqtrrd	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to w (N - 1) \in (G NeighbVtx X)$
32	13	adantl	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to w (N - 2) = X$
33	21 31 32	3jca	$⊢ (((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \land (w (0) = X \land w (N - 2) = X)) \to ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X)$
34	33	ex	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to ((w (0) = X \land w (N - 2) = X) \to ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X))$
35		simpr	$⊢ (w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \to w (0) = X$
36	35	anim1i	$⊢ ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \land w (N - 2) = X) \to (w (0) = X \land w (N - 2) = X)$
37	36	3adant2	$⊢ ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X) \to (w (0) = X \land w (N - 2) = X)$
38	34 37	impbid1	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to ((w (0) = X \land w (N - 2) = X) \leftrightarrow ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X))$
39		2clwwlklem	$⊢ (w \in (N ClWWalksN G) \land N \in ℤ_{\geq 3}) \to (w prefix (N - 2)) (0) = w (0)$
40	39	3ad2antr3	$⊢ (w \in (N ClWWalksN G) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \to (w prefix (N - 2)) (0) = w (0)$
41	40	ancoms	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to (w prefix (N - 2)) (0) = w (0)$
42	41	eqcomd	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to w (0) = (w prefix (N - 2)) (0)$
43	42	eqeq1d	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to (w (0) = X \leftrightarrow (w prefix (N - 2)) (0) = X)$
44	43	anbi2d	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \leftrightarrow (w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X))$
45	44	3anbi1d	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to (((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land w (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X) \leftrightarrow ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X))$
46	3	eleq2i	$⊢ w prefix (N - 2) \in F \leftrightarrow w prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2))$
47		isclwwlknon	$⊢ w prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow (w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X)$
48	47	a1i	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (w prefix (N - 2) \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow (w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X))$
49	46 48	syl5bb	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (w prefix (N - 2) \in F \leftrightarrow (w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X))$
50	49	3anbi1d	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X) \leftrightarrow ((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X))$
51	50	bicomd	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X) \leftrightarrow (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X))$
52	51	adantr	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to (((w prefix (N - 2) \in ((N - 2) ClWWalksN G) \land (w prefix (N - 2)) (0) = X) \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X) \leftrightarrow (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X))$
53	38 45 52	3bitrd	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land w \in (N ClWWalksN G)) \to ((w (0) = X \land w (N - 2) = X) \leftrightarrow (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X))$
54	53	rabbidva	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \{w \in (N ClWWalksN G) \| (w (0) = X \land w (N - 2) = X)\} = \{w \in (N ClWWalksN G) \| (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X)\}$
55	10 54	syl5eq	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \{w \in \{w \in (N ClWWalksN G) \| w (0) = X\} \| w (N - 2) = X\} = \{w \in (N ClWWalksN G) \| (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X)\}$
56	9 55	syl5eq	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} = \{w \in (N ClWWalksN G) \| (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X)\}$
57	7 56	eqtrd	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to X C N = \{w \in (N ClWWalksN G) \| (w prefix (N - 2) \in F \land w (N - 1) \in (G NeighbVtx X) \land w (N - 2) = X)\}$

Metamath Proof Explorer

Theorem extwwlkfab

Proof