clwwlkext2edg

Description: If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

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

Proof

Step	Hyp	Ref	Expression
1		clwwlkext2edg.v	$⊢ V = Vtx (G)$
2		clwwlkext2edg.e	$⊢ E = Edg (G)$
3		clwwlknnn	$⊢ W ++ ⟨“ Z ”⟩ \in (N ClWWalksN G) \to N \in ℕ$
4	1 2	isclwwlknx	$⊢ N \in ℕ \to (W ++ ⟨“ Z ”⟩ \in (N 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))$
5		ige2m2fzo	$⊢ N \in ℤ_{\geq 2} \to N - 2 \in (0 ..^N - 1)$
6	5	3ad2ant3	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to N - 2 \in (0 ..^N - 1)$
7	6	adantr	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to N - 2 \in (0 ..^N - 1)$
8		oveq1	$⊢ \|W ++ ⟨“ Z ”⟩\| = N \to \|W ++ ⟨“ Z ”⟩\| - 1 = N - 1$
9	8	oveq2d	$⊢ \|W ++ ⟨“ Z ”⟩\| = N \to (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) = (0 ..^N - 1)$
10	9	eleq2d	$⊢ \|W ++ ⟨“ Z ”⟩\| = N \to (N - 2 \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \leftrightarrow N - 2 \in (0 ..^N - 1))$
11	10	adantl	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (N - 2 \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \leftrightarrow N - 2 \in (0 ..^N - 1))$
12	7 11	mpbird	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to N - 2 \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1)$
13		fveq2	$⊢ i = N - 2 \to (W ++ ⟨“ Z ”⟩) (i) = (W ++ ⟨“ Z ”⟩) (N - 2)$
14		fvoveq1	$⊢ i = N - 2 \to (W ++ ⟨“ Z ”⟩) (i + 1) = (W ++ ⟨“ Z ”⟩) (N - 2 + 1)$
15	13 14	preq12d	$⊢ i = N - 2 \to \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} = \{(W ++ ⟨“ Z ”⟩) (N - 2), (W ++ ⟨“ Z ”⟩) (N - 2 + 1)\}$
16	15	eleq1d	$⊢ i = N - 2 \to (\{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \leftrightarrow \{(W ++ ⟨“ Z ”⟩) (N - 2), (W ++ ⟨“ Z ”⟩) (N - 2 + 1)\} \in E)$
17	16	rspcv	$⊢ N - 2 \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \to (\forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \to \{(W ++ ⟨“ Z ”⟩) (N - 2), (W ++ ⟨“ Z ”⟩) (N - 2 + 1)\} \in E)$
18	12 17	syl	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (\forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \to \{(W ++ ⟨“ Z ”⟩) (N - 2), (W ++ ⟨“ Z ”⟩) (N - 2 + 1)\} \in E)$
19		wrdlenccats1lenm1	$⊢ W \in Word V \to \|W ++ ⟨“ Z ”⟩\| - 1 = \|W\|$
20	19	eqcomd	$⊢ W \in Word V \to \|W\| = \|W ++ ⟨“ Z ”⟩\| - 1$
21	20	adantr	$⊢ (W \in Word V \land Z \in V) \to \|W\| = \|W ++ ⟨“ Z ”⟩\| - 1$
22	21 8	sylan9eq	$⊢ ((W \in Word V \land Z \in V) \land \|W ++ ⟨“ Z ”⟩\| = N) \to \|W\| = N - 1$
23	22	ex	$⊢ (W \in Word V \land Z \in V) \to (\|W ++ ⟨“ Z ”⟩\| = N \to \|W\| = N - 1)$
24	23	3adant3	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W ++ ⟨“ Z ”⟩\| = N \to \|W\| = N - 1)$
25		eluzelcn	$⊢ N \in ℤ_{\geq 2} \to N \in ℂ$
26		1cnd	$⊢ N \in ℤ_{\geq 2} \to 1 \in ℂ$
27	25 26 26	subsub4d	$⊢ N \in ℤ_{\geq 2} \to N - 1 - 1 = N - (1 + 1)$
28		1p1e2	$⊢ 1 + 1 = 2$
29	28	a1i	$⊢ N \in ℤ_{\geq 2} \to 1 + 1 = 2$
30	29	oveq2d	$⊢ N \in ℤ_{\geq 2} \to N - (1 + 1) = N - 2$
31	27 30	eqtr2d	$⊢ N \in ℤ_{\geq 2} \to N - 2 = N - 1 - 1$
32	31	3ad2ant3	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to N - 2 = N - 1 - 1$
33		oveq1	$⊢ \|W\| = N - 1 \to \|W\| - 1 = N - 1 - 1$
34	33	eqcomd	$⊢ \|W\| = N - 1 \to N - 1 - 1 = \|W\| - 1$
35	32 34	sylan9eq	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to N - 2 = \|W\| - 1$
36	35	ex	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W\| = N - 1 \to N - 2 = \|W\| - 1)$
37	24 36	syld	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W ++ ⟨“ Z ”⟩\| = N \to N - 2 = \|W\| - 1)$
38	37	imp	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to N - 2 = \|W\| - 1$
39	38	fveq2d	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W ++ ⟨“ Z ”⟩) (N - 2) = (W ++ ⟨“ Z ”⟩) (\|W\| - 1)$
40		simpl1	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to W \in Word V$
41		s1cl	$⊢ Z \in V \to ⟨“ Z ”⟩ \in Word V$
42	41	3ad2ant2	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to ⟨“ Z ”⟩ \in Word V$
43	42	adantr	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to ⟨“ Z ”⟩ \in Word V$
44		eluz2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land N \in ℤ \land 2 \leq N)$
45		zre	$⊢ N \in ℤ \to N \in ℝ$
46		1red	$⊢ (N \in ℝ \land 2 \leq N) \to 1 \in ℝ$
47		2re	$⊢ 2 \in ℝ$
48	47	a1i	$⊢ (N \in ℝ \land 2 \leq N) \to 2 \in ℝ$
49		simpl	$⊢ (N \in ℝ \land 2 \leq N) \to N \in ℝ$
50		1lt2	$⊢ 1 < 2$
51	50	a1i	$⊢ (N \in ℝ \land 2 \leq N) \to 1 < 2$
52		simpr	$⊢ (N \in ℝ \land 2 \leq N) \to 2 \leq N$
53	46 48 49 51 52	ltletrd	$⊢ (N \in ℝ \land 2 \leq N) \to 1 < N$
54		1red	$⊢ N \in ℝ \to 1 \in ℝ$
55		id	$⊢ N \in ℝ \to N \in ℝ$
56	54 55	posdifd	$⊢ N \in ℝ \to (1 < N \leftrightarrow 0 < N - 1)$
57	56	adantr	$⊢ (N \in ℝ \land 2 \leq N) \to (1 < N \leftrightarrow 0 < N - 1)$
58	53 57	mpbid	$⊢ (N \in ℝ \land 2 \leq N) \to 0 < N - 1$
59	58	ex	$⊢ N \in ℝ \to (2 \leq N \to 0 < N - 1)$
60	45 59	syl	$⊢ N \in ℤ \to (2 \leq N \to 0 < N - 1)$
61	60	a1i	$⊢ 2 \in ℤ \to (N \in ℤ \to (2 \leq N \to 0 < N - 1))$
62	61	3imp	$⊢ (2 \in ℤ \land N \in ℤ \land 2 \leq N) \to 0 < N - 1$
63	44 62	sylbi	$⊢ N \in ℤ_{\geq 2} \to 0 < N - 1$
64	63	ad2antlr	$⊢ ((W \in Word V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to 0 < N - 1$
65		breq2	$⊢ \|W\| = N - 1 \to (0 < \|W\| \leftrightarrow 0 < N - 1)$
66	65	adantl	$⊢ ((W \in Word V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to (0 < \|W\| \leftrightarrow 0 < N - 1)$
67	64 66	mpbird	$⊢ ((W \in Word V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to 0 < \|W\|$
68		hashneq0	$⊢ W \in Word V \to (0 < \|W\| \leftrightarrow W \neq \emptyset)$
69	68	adantr	$⊢ (W \in Word V \land N \in ℤ_{\geq 2}) \to (0 < \|W\| \leftrightarrow W \neq \emptyset)$
70	69	adantr	$⊢ ((W \in Word V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to (0 < \|W\| \leftrightarrow W \neq \emptyset)$
71	67 70	mpbid	$⊢ ((W \in Word V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to W \neq \emptyset$
72	71	3adantl2	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to W \neq \emptyset$
73	40 43 72	3jca	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land W \neq \emptyset)$
74	73	ex	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W\| = N - 1 \to (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land W \neq \emptyset))$
75	24 74	syld	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W ++ ⟨“ Z ”⟩\| = N \to (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land W \neq \emptyset))$
76	75	imp	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land W \neq \emptyset)$
77		ccatval1lsw	$⊢ (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land W \neq \emptyset) \to (W ++ ⟨“ Z ”⟩) (\|W\| - 1) = lastS (W)$
78	76 77	syl	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W ++ ⟨“ Z ”⟩) (\|W\| - 1) = lastS (W)$
79	39 78	eqtrd	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W ++ ⟨“ Z ”⟩) (N - 2) = lastS (W)$
80		2m1e1	$⊢ 2 - 1 = 1$
81	80	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 - 1 = 1$
82	81	eqcomd	$⊢ N \in ℤ_{\geq 2} \to 1 = 2 - 1$
83	82	oveq2d	$⊢ N \in ℤ_{\geq 2} \to N - 1 = N - (2 - 1)$
84		2cnd	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℂ$
85	25 84 26	subsubd	$⊢ N \in ℤ_{\geq 2} \to N - (2 - 1) = N - 2 + 1$
86	83 85	eqtr2d	$⊢ N \in ℤ_{\geq 2} \to N - 2 + 1 = N - 1$
87	86	3ad2ant3	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to N - 2 + 1 = N - 1$
88		eqeq2	$⊢ \|W\| = N - 1 \to (N - 2 + 1 = \|W\| \leftrightarrow N - 2 + 1 = N - 1)$
89	87 88	syl5ibrcom	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W\| = N - 1 \to N - 2 + 1 = \|W\|)$
90	24 89	syld	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W ++ ⟨“ Z ”⟩\| = N \to N - 2 + 1 = \|W\|)$
91	90	imp	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to N - 2 + 1 = \|W\|$
92	91	fveq2d	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W ++ ⟨“ Z ”⟩) (N - 2 + 1) = (W ++ ⟨“ Z ”⟩) (\|W\|)$
93		id	$⊢ (W \in Word V \land Z \in V) \to (W \in Word V \land Z \in V)$
94	93	3adant3	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (W \in Word V \land Z \in V)$
95	94	adantr	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W \in Word V \land Z \in V)$
96		ccatws1ls	$⊢ (W \in Word V \land Z \in V) \to (W ++ ⟨“ Z ”⟩) (\|W\|) = Z$
97	95 96	syl	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W ++ ⟨“ Z ”⟩) (\|W\|) = Z$
98	92 97	eqtrd	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (W ++ ⟨“ Z ”⟩) (N - 2 + 1) = Z$
99	79 98	preq12d	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to \{(W ++ ⟨“ Z ”⟩) (N - 2), (W ++ ⟨“ Z ”⟩) (N - 2 + 1)\} = \{lastS (W), Z\}$
100	99	eleq1d	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (\{(W ++ ⟨“ Z ”⟩) (N - 2), (W ++ ⟨“ Z ”⟩) (N - 2 + 1)\} \in E \leftrightarrow \{lastS (W), Z\} \in E)$
101	18 100	sylibd	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W ++ ⟨“ Z ”⟩\| = N) \to (\forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \to \{lastS (W), Z\} \in E)$
102	101	ex	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W ++ ⟨“ Z ”⟩\| = N \to (\forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \to \{lastS (W), Z\} \in E))$
103	102	com13	$⊢ \forall i \in (0 ..^\|W ++ ⟨“ Z ”⟩\| - 1) \{(W ++ ⟨“ Z ”⟩) (i), (W ++ ⟨“ Z ”⟩) (i + 1)\} \in E \to (\|W ++ ⟨“ Z ”⟩\| = N \to ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to \{lastS (W), Z\} \in E))$
104	103	3ad2ant2	$⊢ (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) \to (\|W ++ ⟨“ Z ”⟩\| = N \to ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to \{lastS (W), Z\} \in E))$
105	104	imp31	$⊢ (((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) \land (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2})) \to \{lastS (W), Z\} \in E$
106	94	adantr	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to (W \in Word V \land Z \in V)$
107		lswccats1	$⊢ (W \in Word V \land Z \in V) \to lastS (W ++ ⟨“ Z ”⟩) = Z$
108	106 107	syl	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to lastS (W ++ ⟨“ Z ”⟩) = Z$
109	63	3ad2ant3	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to 0 < N - 1$
110	109	adantr	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to 0 < N - 1$
111	65	adantl	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to (0 < \|W\| \leftrightarrow 0 < N - 1)$
112	110 111	mpbird	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to 0 < \|W\|$
113		ccatfv0	$⊢ (W \in Word V \land ⟨“ Z ”⟩ \in Word V \land 0 < \|W\|) \to (W ++ ⟨“ Z ”⟩) (0) = W (0)$
114	40 43 112 113	syl3anc	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to (W ++ ⟨“ Z ”⟩) (0) = W (0)$
115	108 114	preq12d	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land \|W\| = N - 1) \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} = \{Z, W (0)\}$
116	115	ex	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W\| = N - 1 \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} = \{Z, W (0)\})$
117	24 116	syld	$⊢ (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\|W ++ ⟨“ Z ”⟩\| = N \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} = \{Z, W (0)\})$
118	117	impcom	$⊢ (\|W ++ ⟨“ Z ”⟩\| = N \land (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2})) \to \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} = \{Z, W (0)\}$
119	118	eleq1d	$⊢ (\|W ++ ⟨“ Z ”⟩\| = N \land (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2})) \to (\{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E \leftrightarrow \{Z, W (0)\} \in E)$
120	119	biimpcd	$⊢ \{lastS (W ++ ⟨“ Z ”⟩), (W ++ ⟨“ Z ”⟩) (0)\} \in E \to ((\|W ++ ⟨“ Z ”⟩\| = N \land (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2})) \to \{Z, W (0)\} \in E)$
121	120	3ad2ant3	$⊢ (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) \to ((\|W ++ ⟨“ Z ”⟩\| = N \land (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2})) \to \{Z, W (0)\} \in E)$
122	121	impl	$⊢ (((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) \land (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2})) \to \{Z, W (0)\} \in E$
123	105 122	jca	$⊢ (((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) \land (W \in Word V \land Z \in V \land N \in ℤ_{\geq 2})) \to (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)$
124	123	ex	$⊢ ((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) \to ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E))$
125	4 124	biimtrdi	$⊢ N \in ℕ \to (W ++ ⟨“ Z ”⟩ \in (N ClWWalksN G) \to ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)))$
126	3 125	mpcom	$⊢ W ++ ⟨“ Z ”⟩ \in (N ClWWalksN G) \to ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \to (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E))$
127	126	impcom	$⊢ ((W \in Word V \land Z \in V \land N \in ℤ_{\geq 2}) \land W ++ ⟨“ Z ”⟩ \in (N ClWWalksN G)) \to (\{lastS (W), Z\} \in E \land \{Z, W (0)\} \in E)$

Metamath Proof Explorer

Theorem clwwlkext2edg

Proof