clwwlkinwwlk

Description: If the initial vertex of a walk occurs another time in the walk, the walk starts with a closed walk. Since the walk is expressed as a word over vertices, the closed walk can be expressed as a subword of this word. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 23-Jan-2022) (Revised by AV, 30-Oct-2022)

		Ref	Expression
	Assertion	clwwlkinwwlk	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land W \in (M WWalksN G) \land W (N) = W (0)) \to W prefix N \in (N ClWWalksN G)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ Edg (G) = Edg (G)$
3	1 2	wwlknp	$⊢ W \in (M WWalksN G) \to (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G))$
4		pfxcl	$⊢ W \in Word Vtx (G) \to W prefix N \in Word Vtx (G)$
5	4	adantr	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1) \to W prefix N \in Word Vtx (G)$
6	5	adantr	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to W prefix N \in Word Vtx (G)$
7		simpll	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to W \in Word Vtx (G)$
8		simprl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in ℕ$
9		eluz2	$⊢ M \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land M \in ℤ \land N \leq M)$
10		zre	$⊢ N \in ℤ \to N \in ℝ$
11		zre	$⊢ M \in ℤ \to M \in ℝ$
12		id	$⊢ N \leq M \to N \leq M$
13	10 11 12	3anim123i	$⊢ (N \in ℤ \land M \in ℤ \land N \leq M) \to (N \in ℝ \land M \in ℝ \land N \leq M)$
14	9 13	sylbi	$⊢ M \in ℤ_{\geq N} \to (N \in ℝ \land M \in ℝ \land N \leq M)$
15		letrp1	$⊢ (N \in ℝ \land M \in ℝ \land N \leq M) \to N \leq M + 1$
16	14 15	syl	$⊢ M \in ℤ_{\geq N} \to N \leq M + 1$
17	16	adantl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \leq M + 1$
18	17	adantl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \leq M + 1$
19		breq2	$⊢ \|W\| = M + 1 \to (N \leq \|W\| \leftrightarrow N \leq M + 1)$
20	19	ad2antlr	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (N \leq \|W\| \leftrightarrow N \leq M + 1)$
21	18 20	mpbird	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \leq \|W\|$
22		pfxn0	$⊢ (W \in Word Vtx (G) \land N \in ℕ \land N \leq \|W\|) \to W prefix N \neq \emptyset$
23	7 8 21 22	syl3anc	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to W prefix N \neq \emptyset$
24	6 23	jca	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (W prefix N \in Word Vtx (G) \land W prefix N \neq \emptyset)$
25	24	3adantl3	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (W prefix N \in Word Vtx (G) \land W prefix N \neq \emptyset)$
26	25	adantr	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to (W prefix N \in Word Vtx (G) \land W prefix N \neq \emptyset)$
27		nnz	$⊢ N \in ℕ \to N \in ℤ$
28		1nn0	$⊢ 1 \in ℕ_{0}$
29		eluzmn	$⊢ (N \in ℤ \land 1 \in ℕ_{0}) \to N \in ℤ_{\geq (N - 1)}$
30	27 28 29	sylancl	$⊢ N \in ℕ \to N \in ℤ_{\geq (N - 1)}$
31		uzss	$⊢ N \in ℤ_{\geq (N - 1)} \to ℤ_{\geq N} \subseteq ℤ_{\geq (N - 1)}$
32	30 31	syl	$⊢ N \in ℕ \to ℤ_{\geq N} \subseteq ℤ_{\geq (N - 1)}$
33	32	sselda	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to M \in ℤ_{\geq (N - 1)}$
34		fzoss2	$⊢ M \in ℤ_{\geq (N - 1)} \to (0 ..^N - 1) \subseteq (0 ..^M)$
35	33 34	syl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to (0 ..^N - 1) \subseteq (0 ..^M)$
36	35	3ad2ant3	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1 \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (0 ..^N - 1) \subseteq (0 ..^M)$
37		ssralv	$⊢ (0 ..^N - 1) \subseteq (0 ..^M) \to (\forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))$
38	36 37	syl	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1 \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (\forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))$
39	38	3exp	$⊢ W \in Word Vtx (G) \to (\|W\| = M + 1 \to ((N \in ℕ \land M \in ℤ_{\geq N}) \to (\forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G) \to \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))))$
40	39	com34	$⊢ W \in Word Vtx (G) \to (\|W\| = M + 1 \to (\forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G) \to ((N \in ℕ \land M \in ℤ_{\geq N}) \to \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))))$
41	40	3imp1	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G)$
42	41	adantr	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G)$
43		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
44		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
45	43 44	sylib	$⊢ N \in ℕ \to N \in ℤ_{\geq 0}$
46		eluzfz	$⊢ (N \in ℤ_{\geq 0} \land M \in ℤ_{\geq N}) \to N \in (0 \dots M)$
47	45 46	sylan	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \in (0 \dots M)$
48		fzelp1	$⊢ N \in (0 \dots M) \to N \in (0 \dots M + 1)$
49	47 48	syl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \in (0 \dots M + 1)$
50	49	adantl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in (0 \dots M + 1)$
51		oveq2	$⊢ \|W\| = M + 1 \to (0 \dots \|W\|) = (0 \dots M + 1)$
52	51	eleq2d	$⊢ \|W\| = M + 1 \to (N \in (0 \dots \|W\|) \leftrightarrow N \in (0 \dots M + 1))$
53	52	ad2antlr	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (N \in (0 \dots \|W\|) \leftrightarrow N \in (0 \dots M + 1))$
54	50 53	mpbird	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in (0 \dots \|W\|)$
55		pfxlen	$⊢ (W \in Word Vtx (G) \land N \in (0 \dots \|W\|)) \to \|W prefix N\| = N$
56	7 54 55	syl2anc	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to \|W prefix N\| = N$
57	56	oveq1d	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to \|W prefix N\| - 1 = N - 1$
58	57	oveq2d	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (0 ..^\|W prefix N\| - 1) = (0 ..^N - 1)$
59	58	raleqdv	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (\forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G))$
60	7	adantr	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to W \in Word Vtx (G)$
61	54	adantr	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to N \in (0 \dots \|W\|)$
62	30	ad2antrl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in ℤ_{\geq (N - 1)}$
63		fzoss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (0 ..^N - 1) \subseteq (0 ..^N)$
64	62 63	syl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (0 ..^N - 1) \subseteq (0 ..^N)$
65	64	sselda	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to i \in (0 ..^N)$
66		pfxfv	$⊢ (W \in Word Vtx (G) \land N \in (0 \dots \|W\|) \land i \in (0 ..^N)) \to (W prefix N) (i) = W (i)$
67	60 61 65 66	syl3anc	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to (W prefix N) (i) = W (i)$
68	27	ad2antrl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in ℤ$
69		elfzom1elp1fzo	$⊢ (N \in ℤ \land i \in (0 ..^N - 1)) \to i + 1 \in (0 ..^N)$
70	68 69	sylan	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to i + 1 \in (0 ..^N)$
71		pfxfv	$⊢ (W \in Word Vtx (G) \land N \in (0 \dots \|W\|) \land i + 1 \in (0 ..^N)) \to (W prefix N) (i + 1) = W (i + 1)$
72	60 61 70 71	syl3anc	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to (W prefix N) (i + 1) = W (i + 1)$
73	67 72	preq12d	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to \{(W prefix N) (i), (W prefix N) (i + 1)\} = \{W (i), W (i + 1)\}$
74	73	eleq1d	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i \in (0 ..^N - 1)) \to (\{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \leftrightarrow \{W (i), W (i + 1)\} \in Edg (G))$
75	74	ralbidva	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (\forall i \in (0 ..^N - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))$
76	59 75	bitrd	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (\forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))$
77	76	3adantl3	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (\forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))$
78	77	adantr	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to (\forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G))$
79	42 78	mpbird	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to \forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G)$
80		elfz1uz	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \in (1 \dots M)$
81		fzelp1	$⊢ N \in (1 \dots M) \to N \in (1 \dots M + 1)$
82	80 81	syl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N \in (1 \dots M + 1)$
83	82	adantl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in (1 \dots M + 1)$
84		oveq2	$⊢ \|W\| = M + 1 \to (1 \dots \|W\|) = (1 \dots M + 1)$
85	84	eleq2d	$⊢ \|W\| = M + 1 \to (N \in (1 \dots \|W\|) \leftrightarrow N \in (1 \dots M + 1))$
86	85	ad2antlr	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (N \in (1 \dots \|W\|) \leftrightarrow N \in (1 \dots M + 1))$
87	83 86	mpbird	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in (1 \dots \|W\|)$
88		pfxfvlsw	$⊢ (W \in Word Vtx (G) \land N \in (1 \dots \|W\|)) \to lastS (W prefix N) = W (N - 1)$
89		pfxfv0	$⊢ (W \in Word Vtx (G) \land N \in (1 \dots \|W\|)) \to (W prefix N) (0) = W (0)$
90	88 89	preq12d	$⊢ (W \in Word Vtx (G) \land N \in (1 \dots \|W\|)) \to \{lastS (W prefix N), (W prefix N) (0)\} = \{W (N - 1), W (0)\}$
91	7 87 90	syl2anc	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to \{lastS (W prefix N), (W prefix N) (0)\} = \{W (N - 1), W (0)\}$
92	91	3adantl3	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to \{lastS (W prefix N), (W prefix N) (0)\} = \{W (N - 1), W (0)\}$
93	92	adantr	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to \{lastS (W prefix N), (W prefix N) (0)\} = \{W (N - 1), W (0)\}$
94		fz1fzo0m1	$⊢ N \in (1 \dots M) \to N - 1 \in (0 ..^M)$
95	80 94	syl	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to N - 1 \in (0 ..^M)$
96	95	3ad2ant3	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1 \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N - 1 \in (0 ..^M)$
97		simpr	$⊢ (N \in ℕ \land i = N - 1) \to i = N - 1$
98	97	fveq2d	$⊢ (N \in ℕ \land i = N - 1) \to W (i) = W (N - 1)$
99		oveq1	$⊢ i = N - 1 \to i + 1 = N - 1 + 1$
100		nncn	$⊢ N \in ℕ \to N \in ℂ$
101		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
102	100 101	syl	$⊢ N \in ℕ \to N - 1 + 1 = N$
103	99 102	sylan9eqr	$⊢ (N \in ℕ \land i = N - 1) \to i + 1 = N$
104	103	fveq2d	$⊢ (N \in ℕ \land i = N - 1) \to W (i + 1) = W (N)$
105	98 104	preq12d	$⊢ (N \in ℕ \land i = N - 1) \to \{W (i), W (i + 1)\} = \{W (N - 1), W (N)\}$
106	105	eleq1d	$⊢ (N \in ℕ \land i = N - 1) \to (\{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (N)\} \in Edg (G))$
107	106	ex	$⊢ N \in ℕ \to (i = N - 1 \to (\{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (N)\} \in Edg (G)))$
108	107	adantr	$⊢ (N \in ℕ \land M \in ℤ_{\geq N}) \to (i = N - 1 \to (\{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (N)\} \in Edg (G)))$
109	108	3ad2ant3	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1 \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (i = N - 1 \to (\{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (N)\} \in Edg (G)))$
110	109	imp	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1 \land (N \in ℕ \land M \in ℤ_{\geq N})) \land i = N - 1) \to (\{W (i), W (i + 1)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (N)\} \in Edg (G))$
111	96 110	rspcdv	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1 \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (\forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G) \to \{W (N - 1), W (N)\} \in Edg (G))$
112	111	3exp	$⊢ W \in Word Vtx (G) \to (\|W\| = M + 1 \to ((N \in ℕ \land M \in ℤ_{\geq N}) \to (\forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G) \to \{W (N - 1), W (N)\} \in Edg (G))))$
113	112	com34	$⊢ W \in Word Vtx (G) \to (\|W\| = M + 1 \to (\forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G) \to ((N \in ℕ \land M \in ℤ_{\geq N}) \to \{W (N - 1), W (N)\} \in Edg (G))))$
114	113	3imp1	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to \{W (N - 1), W (N)\} \in Edg (G)$
115	114	adantr	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to \{W (N - 1), W (N)\} \in Edg (G)$
116		preq2	$⊢ W (N) = W (0) \to \{W (N - 1), W (N)\} = \{W (N - 1), W (0)\}$
117	116	eleq1d	$⊢ W (N) = W (0) \to (\{W (N - 1), W (N)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (0)\} \in Edg (G))$
118	117	adantl	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to (\{W (N - 1), W (N)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (0)\} \in Edg (G))$
119	115 118	mpbid	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to \{W (N - 1), W (0)\} \in Edg (G)$
120	93 119	eqeltrd	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to \{lastS (W prefix N), (W prefix N) (0)\} \in Edg (G)$
121	26 79 120	3jca	$⊢ (((W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land (N \in ℕ \land M \in ℤ_{\geq N})) \land W (N) = W (0)) \to ((W prefix N \in Word Vtx (G) \land W prefix N \neq \emptyset) \land \forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \land \{lastS (W prefix N), (W prefix N) (0)\} \in Edg (G))$
122	121	exp31	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \to ((N \in ℕ \land M \in ℤ_{\geq N}) \to (W (N) = W (0) \to ((W prefix N \in Word Vtx (G) \land W prefix N \neq \emptyset) \land \forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \land \{lastS (W prefix N), (W prefix N) (0)\} \in Edg (G))))$
123	122	3imp21	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land W (N) = W (0)) \to ((W prefix N \in Word Vtx (G) \land W prefix N \neq \emptyset) \land \forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \land \{lastS (W prefix N), (W prefix N) (0)\} \in Edg (G))$
124	1 2	isclwwlk	$⊢ W prefix N \in ClWWalks (G) \leftrightarrow ((W prefix N \in Word Vtx (G) \land W prefix N \neq \emptyset) \land \forall i \in (0 ..^\|W prefix N\| - 1) \{(W prefix N) (i), (W prefix N) (i + 1)\} \in Edg (G) \land \{lastS (W prefix N), (W prefix N) (0)\} \in Edg (G))$
125	123 124	sylibr	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land W (N) = W (0)) \to W prefix N \in ClWWalks (G)$
126	47	adantl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in (0 \dots M)$
127	126 48	syl	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in (0 \dots M + 1)$
128	127 53	mpbird	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to N \in (0 \dots \|W\|)$
129	7 128	jca	$⊢ ((W \in Word Vtx (G) \land \|W\| = M + 1) \land (N \in ℕ \land M \in ℤ_{\geq N})) \to (W \in Word Vtx (G) \land N \in (0 \dots \|W\|))$
130	129	ex	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1) \to ((N \in ℕ \land M \in ℤ_{\geq N}) \to (W \in Word Vtx (G) \land N \in (0 \dots \|W\|)))$
131	130	3adant3	$⊢ (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \to ((N \in ℕ \land M \in ℤ_{\geq N}) \to (W \in Word Vtx (G) \land N \in (0 \dots \|W\|)))$
132	131	impcom	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G))) \to (W \in Word Vtx (G) \land N \in (0 \dots \|W\|))$
133	132	3adant3	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land W (N) = W (0)) \to (W \in Word Vtx (G) \land N \in (0 \dots \|W\|))$
134	133 55	syl	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land W (N) = W (0)) \to \|W prefix N\| = N$
135		isclwwlkn	$⊢ W prefix N \in (N ClWWalksN G) \leftrightarrow (W prefix N \in ClWWalks (G) \land \|W prefix N\| = N)$
136	125 134 135	sylanbrc	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land (W \in Word Vtx (G) \land \|W\| = M + 1 \land \forall i \in (0 ..^M) \{W (i), W (i + 1)\} \in Edg (G)) \land W (N) = W (0)) \to W prefix N \in (N ClWWalksN G)$
137	3 136	syl3an2	$⊢ ((N \in ℕ \land M \in ℤ_{\geq N}) \land W \in (M WWalksN G) \land W (N) = W (0)) \to W prefix N \in (N ClWWalksN G)$

Metamath Proof Explorer

Theorem clwwlkinwwlk

Proof