wwlksext2clwwlk

Description: If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Revised by AV, 14-Mar-2022)

	Ref	Expression
Hypotheses	clwwlkext2edg.v	$⊢ V = Vtx (G)$
	clwwlkext2edg.e	$⊢ E = Edg (G)$
Assertion	wwlksext2clwwlk	$⊢ (W \in (N WWalksN G) \land Z \in V) \to ((\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E) \to W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G))$

Proof

Step	Hyp	Ref	Expression
1		clwwlkext2edg.v	$⊢ V = Vtx (G)$
2		clwwlkext2edg.e	$⊢ E = Edg (G)$
3		wwlknbp1	$⊢ W \in (N WWalksN G) \to (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)$
4	1	wrdeqi	$⊢ Word V = Word Vtx (G)$
5	4	eleq2i	$⊢ W \in Word V \leftrightarrow W \in Word Vtx (G)$
6	5	biimpri	$⊢ W \in Word Vtx (G) \to W \in Word V$
7	6	3ad2ant2	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to W \in Word V$
8	7	ad2antlr	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to W \in Word V$
9		s1cl	$⊢ Z \in V \to ⟨“ Z ”⟩ \in Word V$
10	9	adantl	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to ⟨“ Z ”⟩ \in Word V$
11		ccatcl	$⊢ (W \in Word V \land ⟨“ Z ”⟩ \in Word V) \to W ++ ⟨“ Z ”⟩ \in Word V$
12	8 10 11	syl2anc	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to W ++ ⟨“ Z ”⟩ \in Word V$
13	12	adantr	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)) \to W ++ ⟨“ Z ”⟩ \in Word V$
14	1 2	wwlknp	$⊢ W \in (N WWalksN G) \to (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E)$
15		simplll	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to W \in Word V$
16	9	adantr	$⊢ (Z \in V \land N \in ℕ_{0}) \to ⟨“ Z ”⟩ \in Word V$
17	16	ad2antlr	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to ⟨“ Z ”⟩ \in Word V$
18		elfzo0	$⊢ i \in (0 ..^N) \leftrightarrow (i \in ℕ_{0} \land N \in ℕ \land i < N)$
19		simp1	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to i \in ℕ_{0}$
20		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
21	20	3ad2ant2	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to N + 1 \in ℕ$
22		nn0re	$⊢ i \in ℕ_{0} \to i \in ℝ$
23	22	3ad2ant1	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to i \in ℝ$
24		nnre	$⊢ N \in ℕ \to N \in ℝ$
25	24	3ad2ant2	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to N \in ℝ$
26		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
27	24 26	syl	$⊢ N \in ℕ \to N + 1 \in ℝ$
28	27	3ad2ant2	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to N + 1 \in ℝ$
29		simp3	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to i < N$
30	24	ltp1d	$⊢ N \in ℕ \to N < N + 1$
31	30	3ad2ant2	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to N < N + 1$
32	23 25 28 29 31	lttrd	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to i < N + 1$
33		elfzo0	$⊢ i \in (0 ..^N + 1) \leftrightarrow (i \in ℕ_{0} \land N + 1 \in ℕ \land i < N + 1)$
34	19 21 32 33	syl3anbrc	$⊢ (i \in ℕ_{0} \land N \in ℕ \land i < N) \to i \in (0 ..^N + 1)$
35	18 34	sylbi	$⊢ i \in (0 ..^N) \to i \in (0 ..^N + 1)$
36	35	adantl	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to i \in (0 ..^N + 1)$
37		oveq2	$⊢ \|W\| = N + 1 \to (0 ..^\|W\|) = (0 ..^N + 1)$
38	37	adantl	$⊢ (W \in Word V \land \|W\| = N + 1) \to (0 ..^\|W\|) = (0 ..^N + 1)$
39	38	eleq2d	$⊢ (W \in Word V \land \|W\| = N + 1) \to (i \in (0 ..^\|W\|) \leftrightarrow i \in (0 ..^N + 1))$
40	39	ad2antrr	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (i \in (0 ..^\|W\|) \leftrightarrow i \in (0 ..^N + 1))$
41	36 40	mpbird	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to i \in (0 ..^\|W\|)$
42		ccatval1	$⊢ (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land i \in (0 ..^\|W\|)) \to (W ++ ⟨“ Z ”⟩) (i) = W (i)$
43	15 17 41 42	syl3anc	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (W ++ ⟨“ Z ”⟩) (i) = W (i)$
44		fzonn0p1p1	$⊢ i \in (0 ..^N) \to i + 1 \in (0 ..^N + 1)$
45	44	adantl	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to i + 1 \in (0 ..^N + 1)$
46	37	eleq2d	$⊢ \|W\| = N + 1 \to (i + 1 \in (0 ..^\|W\|) \leftrightarrow i + 1 \in (0 ..^N + 1))$
47	46	ad3antlr	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (i + 1 \in (0 ..^\|W\|) \leftrightarrow i + 1 \in (0 ..^N + 1))$
48	45 47	mpbird	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to i + 1 \in (0 ..^\|W\|)$
49		ccatval1	$⊢ (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land i + 1 \in (0 ..^\|W\|)) \to (W ++ ⟨“ Z ”⟩) (i + 1) = W (i + 1)$
50	15 17 48 49	syl3anc	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to (W ++ ⟨“ Z ”⟩) (i + 1) = W (i + 1)$
51	43 50	preq12d	$⊢ (((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \land i \in (0 ..^N)) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\}$
52	51	ex	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to (i \in (0 ..^N) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\})$
53	52	expcom	$⊢ (Z \in V \land N \in ℕ_{0}) \to ((W \in Word V \land \|W\| = N + 1) \to (i \in (0 ..^N) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\}))$
54	53	expcom	$⊢ N \in ℕ_{0} \to (Z \in V \to ((W \in Word V \land \|W\| = N + 1) \to (i \in (0 ..^N) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\})))$
55	54	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (Z \in V \to ((W \in Word V \land \|W\| = N + 1) \to (i \in (0 ..^N) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\})))$
56	55	imp	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to ((W \in Word V \land \|W\| = N + 1) \to (i \in (0 ..^N) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\}))$
57	56	expdcom	$⊢ W \in Word V \to (\|W\| = N + 1 \to (((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to (i \in (0 ..^N) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\})))$
58	57	3imp1	$⊢ ((W \in Word V \land \|W\| = N + 1 \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land i \in (0 ..^N)) \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{W (i), W (i + 1)\}$
59	58	eleq1d	$⊢ ((W \in Word V \land \|W\| = N + 1 \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land i \in (0 ..^N)) \to (\{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \{W (i), W (i + 1)\} \in E)$
60	59	ralbidva	$⊢ (W \in Word V \land \|W\| = N + 1 \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to (\forall i \in (0 ..^N) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E)$
61	60	biimprd	$⊢ (W \in Word V \land \|W\| = N + 1 \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to (\forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E \to \forall i \in (0 ..^N) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)$
62	61	3exp	$⊢ W \in Word V \to (\|W\| = N + 1 \to (((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to (\forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E \to \forall i \in (0 ..^N) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)))$
63	62	com34	$⊢ W \in Word V \to (\|W\| = N + 1 \to (\forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E \to (((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to \forall i \in (0 ..^N) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)))$
64	63	3imp1	$⊢ ((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to \forall i \in (0 ..^N) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
65	64	adantr	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \forall i \in (0 ..^N) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
66		simpll	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to W \in Word V$
67	9	ad2antrl	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to ⟨“ Z ”⟩ \in Word V$
68		nn0p1gt0	$⊢ N \in ℕ_{0} \to 0 < N + 1$
69	68	ad2antll	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to 0 < N + 1$
70		breq2	$⊢ \|W\| = N + 1 \to (0 < \|W\| \leftrightarrow 0 < N + 1)$
71	70	ad2antlr	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to (0 < \|W\| \leftrightarrow 0 < N + 1)$
72	69 71	mpbird	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to 0 < \|W\|$
73		hashneq0	$⊢ W \in Word V \to (0 < \|W\| \leftrightarrow W \neq \emptyset)$
74	73	ad2antrr	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to (0 < \|W\| \leftrightarrow W \neq \emptyset)$
75	72 74	mpbid	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to W \neq \emptyset$
76		ccatval1lsw	$⊢ (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land W \neq \emptyset) \to (W ++ ⟨“ Z ”⟩) (\|W\| - 1) = lastS (W)$
77	66 67 75 76	syl3anc	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to (W ++ ⟨“ Z ”⟩) (\|W\| - 1) = lastS (W)$
78		oveq1	$⊢ \|W\| = N + 1 \to \|W\| - 1 = N + 1 - 1$
79	78	ad2antlr	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to \|W\| - 1 = N + 1 - 1$
80		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
81	80	ad2antll	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to N \in ℂ$
82		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
83	81 82	syl	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to N + 1 - 1 = N$
84	79 83	eqtrd	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to \|W\| - 1 = N$
85	84	fveq2d	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to (W ++ ⟨“ Z ”⟩) (\|W\| - 1) = (W ++ ⟨“ Z ”⟩) (N)$
86	77 85	eqtr3d	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to lastS (W) = (W ++ ⟨“ Z ”⟩) (N)$
87		ccatws1ls	$⊢ (W \in Word V \land Z \in V) \to (W ++ ⟨“ Z ”⟩) (\|W\|) = Z$
88	87	ad2ant2r	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to (W ++ ⟨“ Z ”⟩) (\|W\|) = Z$
89		fveq2	$⊢ \|W\| = N + 1 \to (W ++ ⟨“ Z ”⟩) (\|W\|) = (W ++ ⟨“ Z ”⟩) (N + 1)$
90	89	ad2antlr	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to (W ++ ⟨“ Z ”⟩) (\|W\|) = (W ++ ⟨“ Z ”⟩) (N + 1)$
91	88 90	eqtr3d	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to Z = (W ++ ⟨“ Z ”⟩) (N + 1)$
92	86 91	preq12d	$⊢ ((W \in Word V \land \|W\| = N + 1) \land (Z \in V \land N \in ℕ_{0})) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\}$
93	92	expcom	$⊢ (Z \in V \land N \in ℕ_{0}) \to ((W \in Word V \land \|W\| = N + 1) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\})$
94	93	expcom	$⊢ N \in ℕ_{0} \to (Z \in V \to ((W \in Word V \land \|W\| = N + 1) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\}))$
95	94	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (Z \in V \to ((W \in Word V \land \|W\| = N + 1) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\}))$
96	95	imp	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to ((W \in Word V \land \|W\| = N + 1) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\})$
97	96	com12	$⊢ (W \in Word V \land \|W\| = N + 1) \to (((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\})$
98	97	3adant3	$⊢ (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \to (((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\})$
99	98	imp	$⊢ ((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to \{lastS (W), Z\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\}$
100	99	eleq1d	$⊢ ((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to (\{lastS (W), Z\} \in E \leftrightarrow \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\} \in E)$
101	100	biimpa	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\} \in E$
102		simprl1	$⊢ ((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to N \in ℕ_{0}$
103	102	adantr	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to N \in ℕ_{0}$
104		fveq2	$⊢ i = N \to (W ++ ⟨“ Z ”⟩) (i) = (W ++ ⟨“ Z ”⟩) (N)$
105		fvoveq1	$⊢ i = N \to (W ++ ⟨“ Z ”⟩) (i + 1) = (W ++ ⟨“ Z ”⟩) (N + 1)$
106	104 105	preq12d	$⊢ i = N \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\}$
107	106	eleq1d	$⊢ i = N \to (\{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\} \in E)$
108	107	ralsng	$⊢ N \in ℕ_{0} \to (\forall i \in \{N\} \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\} \in E)$
109	103 108	syl	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to (\forall i \in \{N\} \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \{(W ++ ⟨“ Z ”⟩) (N), (W ++ ⟨“ Z ”⟩) (N + 1)\} \in E)$
110	101 109	mpbird	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \forall i \in \{N\} \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
111		ralunb	$⊢ \forall i \in ((0 ..^N) \cup \{N\}) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow (\forall i \in (0 ..^N) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \land \forall i \in \{N\} \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)$
112	65 110 111	sylanbrc	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \forall i \in ((0 ..^N) \cup \{N\}) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
113		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
114	102 113	sylib	$⊢ ((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to N \in ℤ_{\geq 0}$
115	114	adantr	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to N \in ℤ_{\geq 0}$
116		fzosplitsn	$⊢ N \in ℤ_{\geq 0} \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
117	115 116	syl	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
118	117	raleqdv	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to (\forall i \in (0 ..^N + 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \forall i \in ((0 ..^N) \cup \{N\}) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)$
119	112 118	mpbird	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \forall i \in (0 ..^N + 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
120		ccatws1len	$⊢ W \in Word V \to \|W ++ ⟨“ Z ”⟩\| = \|W\| + 1$
121	120	3ad2ant1	$⊢ (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \to \|W ++ ⟨“ Z ”⟩\| = \|W\| + 1$
122	121	ad2antrr	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \|W ++ ⟨“ Z ”⟩\| = \|W\| + 1$
123	122	oveq1d	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \|W ++ ⟨“ Z ”⟩\| - 1 = \|W\| + 1 - 1$
124		oveq1	$⊢ \|W\| = N + 1 \to \|W\| + 1 = N + 1 + 1$
125	124	oveq1d	$⊢ \|W\| = N + 1 \to \|W\| + 1 - 1 = (N + 1) + 1 - 1$
126		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
127	80 126	addcld	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
128	127 126	pncand	$⊢ N \in ℕ_{0} \to (N + 1) + 1 - 1 = N + 1$
129	128	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (N + 1) + 1 - 1 = N + 1$
130	129	adantr	$⊢ ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V) \to (N + 1) + 1 - 1 = N + 1$
131	125 130	sylan9eq	$⊢ (\|W\| = N + 1 \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to \|W\| + 1 - 1 = N + 1$
132	131	3ad2antl2	$⊢ ((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \to \|W\| + 1 - 1 = N + 1$
133	132	adantr	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \|W\| + 1 - 1 = N + 1$
134	123 133	eqtrd	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \|W ++ ⟨“ Z ”⟩\| - 1 = N + 1$
135	134	oveq2d	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) = (0 ..^N + 1)$
136	135	raleqdv	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to (\forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \forall i \in (0 ..^N + 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)$
137	119 136	mpbird	$⊢ (((W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \land ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \land Z \in V)) \land \{lastS (W), Z\} \in E) \to \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
138	137	exp42	$⊢ (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in E) \to ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (Z \in V \to (\{lastS (W), Z\} \in E \to \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)))$
139	14 138	syl	$⊢ W \in (N WWalksN G) \to ((N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (Z \in V \to (\{lastS (W), Z\} \in E \to \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E)))$
140	139	imp41	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land \{lastS (W), Z\} \in E) \to \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
141	140	adantrr	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)) \to \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E$
142		lswccats1	$⊢ (W \in Word V \land Z \in V) \to lastS (W ++ ⟨“ Z ”⟩) = Z$
143	8 142	sylancom	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to lastS (W ++ ⟨“ Z ”⟩) = Z$
144	68	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to 0 < N + 1$
145	70	3ad2ant3	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (0 < \|W\| \leftrightarrow 0 < N + 1)$
146	144 145	mpbird	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to 0 < \|W\|$
147	146	ad2antlr	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to 0 < \|W\|$
148		ccatfv0	$⊢ (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land 0 < \|W\|) \to (W ++ ⟨“ Z ”⟩) (0) = W (0)$
149	8 10 147 148	syl3anc	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to (W ++ ⟨“ Z ”⟩) (0) = W (0)$
150	143 149	preq12d	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} = \{Z, W (0)\}$
151	150	eleq1d	$⊢ ((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to (\{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E \leftrightarrow \{Z, W (0)\} \in E)$
152	151	biimprcd	$⊢ \{Z, W (0)\} \in E \to (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E)$
153	152	adantl	$⊢ (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E) \to (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E)$
154	153	impcom	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)) \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E$
155	13 141 154	3jca	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)) \to (W ++ ⟨“ Z ”⟩ \in Word V \land \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \land \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E)$
156		ccatws1len	$⊢ W \in Word Vtx (G) \to \|W ++ ⟨“ Z ”⟩\| = \|W\| + 1$
157	156	3ad2ant2	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W ++ ⟨“ Z ”⟩\| = \|W\| + 1$
158	124	3ad2ant3	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W\| + 1 = N + 1 + 1$
159	80 126 126	addassd	$⊢ N \in ℕ_{0} \to N + 1 + 1 = N + 1 + 1$
160		1p1e2	$⊢ 1 + 1 = 2$
161	160	oveq2i	$⊢ N + 1 + 1 = N + 2$
162	159 161	eqtrdi	$⊢ N \in ℕ_{0} \to N + 1 + 1 = N + 2$
163	162	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to N + 1 + 1 = N + 2$
164	157 158 163	3eqtrd	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to \|W ++ ⟨“ Z ”⟩\| = N + 2$
165	164	ad3antlr	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)) \to \|W ++ ⟨“ Z ”⟩\| = N + 2$
166		2nn	$⊢ 2 \in ℕ$
167		nn0nnaddcl	$⊢ (N \in ℕ_{0} \land 2 \in ℕ) \to N + 2 \in ℕ$
168	166 167	mpan2	$⊢ N \in ℕ_{0} \to N + 2 \in ℕ$
169	168	3ad2ant1	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to N + 2 \in ℕ$
170	1 2	isclwwlknx	$⊢ N + 2 \in ℕ \to (W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G) \leftrightarrow ((W ++ ⟨“ Z ”⟩ \in Word V \land \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \land \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E) \land \|W ++ ⟨“ Z ”⟩\| = N + 2))$
171	169 170	syl	$⊢ (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1) \to (W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G) \leftrightarrow ((W ++ ⟨“ Z ”⟩ \in Word V \land \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \land \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E) \land \|W ++ ⟨“ Z ”⟩\| = N + 2))$
172	171	ad3antlr	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)) \to (W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G) \leftrightarrow ((W ++ ⟨“ Z ”⟩ \in Word V \land \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \land \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E) \land \|W ++ ⟨“ Z ”⟩\| = N + 2))$
173	155 165 172	mpbir2and	$⊢ (((W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \land Z \in V) \land (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)) \to W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G)$
174	173	exp31	$⊢ (W \in (N WWalksN G) \land (N \in ℕ_{0} \land W \in Word Vtx (G) \land \|W\| = N + 1)) \to (Z \in V \to ((\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E) \to W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G)))$
175	3 174	mpdan	$⊢ W \in (N WWalksN G) \to (Z \in V \to ((\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E) \to W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G)))$
176	175	imp	$⊢ (W \in (N WWalksN G) \land Z \in V) \to ((\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E) \to W ++ ⟨“ Z ”⟩ \in ((N + 2) ClWWalksN G))$

Metamath Proof Explorer

Theorem wwlksext2clwwlk

Proof