numclwwlk1lem2foa

Description: Going forth and back from the end of a (closed) walk: W represents the closed walk p_0, ..., p_(n-2), p_0 = p_(n-2). With X = p_(n-2) = p_0 and Y = p_(n-1), ( ( W ++ <" X "> ) ++ <" Y "> ) represents the closed walk p_0, ..., p_(n-2), p_(n-1), p_n = p_0 which is a double loop of length N on vertex X . (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 5-Mar-2022) (Proof shortened by AV, 2-Nov-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	numclwwlk1lem2foa	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((W \in F \land Y \in (G NeighbVtx X)) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X C N))$

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		simpl2	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to X \in V$
5	1	nbgrisvtx	$⊢ Y \in (G NeighbVtx X) \to Y \in V$
6	5	ad2antll	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to Y \in V$
7		simpl3	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to N \in ℤ_{\geq 3}$
8		nbgrsym	$⊢ Y \in (G NeighbVtx X) \leftrightarrow X \in (G NeighbVtx Y)$
9		eqid	$⊢ Edg (G) = Edg (G)$
10	9	nbusgreledg	$⊢ G \in USGraph \to (X \in (G NeighbVtx Y) \leftrightarrow \{X, Y\} \in Edg (G))$
11	10	biimpd	$⊢ G \in USGraph \to (X \in (G NeighbVtx Y) \to \{X, Y\} \in Edg (G))$
12	8 11	syl5bi	$⊢ G \in USGraph \to (Y \in (G NeighbVtx X) \to \{X, Y\} \in Edg (G))$
13	12	adantld	$⊢ G \in USGraph \to ((W \in F \land Y \in (G NeighbVtx X)) \to \{X, Y\} \in Edg (G))$
14	13	3ad2ant1	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((W \in F \land Y \in (G NeighbVtx X)) \to \{X, Y\} \in Edg (G))$
15	14	imp	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to \{X, Y\} \in Edg (G)$
16		simprl	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to W \in F$
17	16 3	eleqtrdi	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to W \in (X ClWWalksNOn (G) (N - 2))$
18	1 9	clwwlknonex2	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in Edg (G) \land W \in (X ClWWalksNOn (G) (N - 2))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G)$
19	4 6 7 15 17 18	syl311anc	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G)$
20	3	eleq2i	$⊢ W \in F \leftrightarrow W \in (X ClWWalksNOn (G) (N - 2))$
21		uz3m2nn	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in ℕ$
22	21	nnne0d	$⊢ N \in ℤ_{\geq 3} \to N - 2 \neq 0$
23	1 9	clwwlknonel	$⊢ N - 2 \neq 0 \to (W \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land \|W\| = N - 2 \land W (0) = X))$
24	22 23	syl	$⊢ N \in ℤ_{\geq 3} \to (W \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land \|W\| = N - 2 \land W (0) = X))$
25	24	3ad2ant3	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (W \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land \|W\| = N - 2 \land W (0) = X))$
26	20 25	syl5bb	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (W \in F \leftrightarrow ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land \|W\| = N - 2 \land W (0) = X))$
27		3simpa	$⊢ (W \in Word V \land \|W\| = N - 2 \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \to (W \in Word V \land \|W\| = N - 2)$
28	27	adantr	$⊢ ((W \in Word V \land \|W\| = N - 2 \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \land Y \in (G NeighbVtx X)) \to (W \in Word V \land \|W\| = N - 2)$
29		simp32	$⊢ (W \in Word V \land \|W\| = N - 2 \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \to X \in V$
30	29 5	anim12i	$⊢ ((W \in Word V \land \|W\| = N - 2 \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \land Y \in (G NeighbVtx X)) \to (X \in V \land Y \in V)$
31		simpl33	$⊢ ((W \in Word V \land \|W\| = N - 2 \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \land Y \in (G NeighbVtx X)) \to N \in ℤ_{\geq 3}$
32	28 30 31	3jca	$⊢ ((W \in Word V \land \|W\| = N - 2 \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \land Y \in (G NeighbVtx X)) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3})$
33	32	3exp1	$⊢ W \in Word V \to (\|W\| = N - 2 \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (Y \in (G NeighbVtx X) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}))))$
34	33	3ad2ant1	$⊢ (W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \to (\|W\| = N - 2 \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (Y \in (G NeighbVtx X) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}))))$
35	34	imp	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land \|W\| = N - 2) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (Y \in (G NeighbVtx X) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3})))$
36	35	3adant3	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land \|W\| = N - 2 \land W (0) = X) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (Y \in (G NeighbVtx X) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3})))$
37	36	com12	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \land \|W\| = N - 2 \land W (0) = X) \to (Y \in (G NeighbVtx X) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3})))$
38	26 37	sylbid	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (W \in F \to (Y \in (G NeighbVtx X) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3})))$
39	38	imp32	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3})$
40		numclwwlk1lem2foalem	$⊢ ((W \in Word V \land \|W\| = N - 2) \land (X \in V \land Y \in V) \land N \in ℤ_{\geq 3}) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)$
41	39 40	syl	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)$
42		eleq1a	$⊢ W \in F \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) \in F)$
43	16 42	syl	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) \in F)$
44		eleq1a	$⊢ Y \in (G NeighbVtx X) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) \in (G NeighbVtx X))$
45	44	ad2antll	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) \in (G NeighbVtx X))$
46		idd	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)$
47	43 45 46	3anim123d	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to ((((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) = W \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) = Y \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) \in F \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) \in (G NeighbVtx X) \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X))$
48	41 47	mpd	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) \in F \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) \in (G NeighbVtx X) \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)$
49	1 2 3	extwwlkfabel	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X C N) \leftrightarrow ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G) \land (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) \in F \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) \in (G NeighbVtx X) \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)))$
50	49	adantr	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X C N) \leftrightarrow ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G) \land (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) prefix (N - 2) \in F \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 1) \in (G NeighbVtx X) \land ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (N - 2) = X)))$
51	19 48 50	mpbir2and	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (W \in F \land Y \in (G NeighbVtx X))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X C N)$
52	51	ex	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((W \in F \land Y \in (G NeighbVtx X)) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (X C N))$

Metamath Proof Explorer

Theorem numclwwlk1lem2foa

Proof