clwwlknonex2

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 28-Mar-2022)

	Ref	Expression
Hypotheses	clwwlknonex2.v	$⊢ V = Vtx (G)$
	clwwlknonex2.e	$⊢ E = Edg (G)$
Assertion	clwwlknonex2	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G)$

Proof

Step	Hyp	Ref	Expression
1		clwwlknonex2.v	$⊢ V = Vtx (G)$
2		clwwlknonex2.e	$⊢ E = Edg (G)$
3		uz3m2nn	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in ℕ$
4	3	nnne0d	$⊢ N \in ℤ_{\geq 3} \to N - 2 \neq 0$
5	4	3ad2ant3	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to N - 2 \neq 0$
6	1 2	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 E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X))$
7	5 6	syl	$⊢ (X \in V \land Y \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 E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X))$
8		simpr11	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \to W \in Word V$
9	8	adantr	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to W \in Word V$
10		simpll1	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to X \in V$
11		simpll2	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to Y \in V$
12		ccatw2s1cl	$⊢ (W \in Word V \land X \in V \land Y \in V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V$
13	9 10 11 12	syl3anc	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V$
14	1 2	clwwlknonex2lem2	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \forall i \in ((0 ..^\|W\| - 1) \cup \{\|W\| - 1, \|W\|\}) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E$
15		simp11	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to W \in Word V$
16	15	ad2antlr	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to W \in Word V$
17		ccatw2s1len	$⊢ W \in Word V \to \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = \|W\| + 2$
18	16 17	syl	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = \|W\| + 2$
19	18	oveq1d	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1 = \|W\| + 2 - 1$
20	19	oveq2d	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) = (0 ..^\|W\| + 2 - 1)$
21		simp3	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to N \in ℤ_{\geq 3}$
22		simp2	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to \|W\| = N - 2$
23	21 22	anim12i	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \to (N \in ℤ_{\geq 3} \land \|W\| = N - 2)$
24	23	adantr	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (N \in ℤ_{\geq 3} \land \|W\| = N - 2)$
25		clwwlknonex2lem1	$⊢ (N \in ℤ_{\geq 3} \land \|W\| = N - 2) \to (0 ..^\|W\| + 2 - 1) = (0 ..^\|W\| - 1) \cup \{\|W\| - 1, \|W\|\}$
26	24 25	syl	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (0 ..^\|W\| + 2 - 1) = (0 ..^\|W\| - 1) \cup \{\|W\| - 1, \|W\|\}$
27	20 26	eqtrd	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) = (0 ..^\|W\| - 1) \cup \{\|W\| - 1, \|W\|\}$
28	27	raleqdv	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (\forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \leftrightarrow \forall i \in ((0 ..^\|W\| - 1) \cup \{\|W\| - 1, \|W\|\}) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E)$
29	14 28	mpbird	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E$
30		ccatws1cl	$⊢ (W \in Word V \land X \in V) \to W ++ ⟨“ X ”⟩ \in Word V$
31		lswccats1	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land Y \in V) \to lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) = Y$
32	30 31	stoic3	$⊢ (W \in Word V \land X \in V \land Y \in V) \to lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) = Y$
33	16 10 11 32	syl3anc	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) = Y$
34	3	nngt0d	$⊢ N \in ℤ_{\geq 3} \to 0 < N - 2$
35		breq2	$⊢ \|W\| = N - 2 \to (0 < \|W\| \leftrightarrow 0 < N - 2)$
36	34 35	imbitrrid	$⊢ \|W\| = N - 2 \to (N \in ℤ_{\geq 3} \to 0 < \|W\|)$
37	36	3ad2ant2	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to (N \in ℤ_{\geq 3} \to 0 < \|W\|)$
38	37	com12	$⊢ N \in ℤ_{\geq 3} \to (((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to 0 < \|W\|)$
39	38	3ad2ant3	$⊢ (X \in V \land Y \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 E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to 0 < \|W\|)$
40	39	imp	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \to 0 < \|W\|$
41	40	adantr	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to 0 < \|W\|$
42		ccat2s1fst	$⊢ (W \in Word V \land 0 < \|W\|) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = W (0)$
43	16 41 42	syl2anc	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0) = W (0)$
44	33 43	preq12d	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} = \{Y, W (0)\}$
45		prcom	$⊢ \{X, Y\} = \{Y, X\}$
46	45	eleq1i	$⊢ \{X, Y\} \in E \leftrightarrow \{Y, X\} \in E$
47	46	biimpi	$⊢ \{X, Y\} \in E \to \{Y, X\} \in E$
48	47	adantl	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \{Y, X\} \in E$
49		preq2	$⊢ W (0) = X \to \{Y, W (0)\} = \{Y, X\}$
50	49	eleq1d	$⊢ W (0) = X \to (\{Y, W (0)\} \in E \leftrightarrow \{Y, X\} \in E)$
51	50	3ad2ant3	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to (\{Y, W (0)\} \in E \leftrightarrow \{Y, X\} \in E)$
52	51	ad2antlr	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (\{Y, W (0)\} \in E \leftrightarrow \{Y, X\} \in E)$
53	48 52	mpbird	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \{Y, W (0)\} \in E$
54	44 53	eqeltrd	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E$
55	13 29 54	3jca	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E)$
56	17	3ad2ant1	$⊢ (W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \to \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = \|W\| + 2$
57	56	3ad2ant1	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = \|W\| + 2$
58	57	ad2antlr	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = \|W\| + 2$
59		oveq1	$⊢ \|W\| = N - 2 \to \|W\| + 2 = N - 2 + 2$
60		eluzelcn	$⊢ N \in ℤ_{\geq 3} \to N \in ℂ$
61		2cn	$⊢ 2 \in ℂ$
62		npcan	$⊢ (N \in ℂ \land 2 \in ℂ) \to N - 2 + 2 = N$
63	60 61 62	sylancl	$⊢ N \in ℤ_{\geq 3} \to N - 2 + 2 = N$
64	59 63	sylan9eq	$⊢ (\|W\| = N - 2 \land N \in ℤ_{\geq 3}) \to \|W\| + 2 = N$
65	64	ex	$⊢ \|W\| = N - 2 \to (N \in ℤ_{\geq 3} \to \|W\| + 2 = N)$
66	65	3ad2ant2	$⊢ ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to (N \in ℤ_{\geq 3} \to \|W\| + 2 = N)$
67	66	com12	$⊢ N \in ℤ_{\geq 3} \to (((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to \|W\| + 2 = N)$
68	67	3ad2ant3	$⊢ (X \in V \land Y \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 E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to \|W\| + 2 = N)$
69	68	imp	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \to \|W\| + 2 = N$
70	69	adantr	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \|W\| + 2 = N$
71	58 70	eqtrd	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N$
72	55 71	jca	$⊢ (((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land ((W \in Word V \land \forall i \in (0 ..^\|W\| - 1) \{W (i), W (i + 1)\} \in E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X)) \land \{X, Y\} \in E) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N)$
73	72	exp31	$⊢ (X \in V \land Y \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 E \land \{lastS (W), W (0)\} \in E) \land \|W\| = N - 2 \land W (0) = X) \to (\{X, Y\} \in E \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N)))$
74	7 73	sylbid	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to (W \in (X ClWWalksNOn (G) (N - 2)) \to (\{X, Y\} \in E \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N)))$
75	74	com23	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to (\{X, Y\} \in E \to (W \in (X ClWWalksNOn (G) (N - 2)) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N)))$
76	75	3imp	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N)$
77		eluzge3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
78	1 2	isclwwlknx	$⊢ N \in ℕ \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G) \leftrightarrow (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N))$
79	77 78	syl	$⊢ N \in ℤ_{\geq 3} \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G) \leftrightarrow (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N))$
80	79	3ad2ant3	$⊢ (X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G) \leftrightarrow (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N))$
81	80	3ad2ant1	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G) \leftrightarrow (((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in Word V \land \forall i \in (0 ..^\|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| - 1) \{((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (i + 1)\} \in E \land \{lastS ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩), ((W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩) (0)\} \in E) \land \|(W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩\| = N))$
82	76 81	mpbird	$⊢ ((X \in V \land Y \in V \land N \in ℤ_{\geq 3}) \land \{X, Y\} \in E \land W \in (X ClWWalksNOn (G) (N - 2))) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ \in (N ClWWalksN G)$

Metamath Proof Explorer

Theorem clwwlknonex2

Proof