clwwlkel

Description: Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018) (Revised by AV, 25-Apr-2021)

		Ref	Expression
	Hypothesis	clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
	Assertion	clwwlkel	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to P ++ ⟨“ P (0) ”⟩ \in D$

Proof

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
2		ccatws1n0	$⊢ P \in Word Vtx (G) \to P ++ ⟨“ P (0) ”⟩ \neq \emptyset$
3	2	adantr	$⊢ (P \in Word Vtx (G) \land \|P\| = N) \to P ++ ⟨“ P (0) ”⟩ \neq \emptyset$
4	3	3ad2ant2	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to P ++ ⟨“ P (0) ”⟩ \neq \emptyset$
5		simprl	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to P \in Word Vtx (G)$
6		fstwrdne0	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to P (0) \in Vtx (G)$
7	6	s1cld	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to ⟨“ P (0) ”⟩ \in Word Vtx (G)$
8		ccatcl	$⊢ (P \in Word Vtx (G) \land ⟨“ P (0) ”⟩ \in Word Vtx (G)) \to P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G)$
9	5 7 8	syl2anc	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G)$
10	9	3adant3	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G)$
11	5	adantr	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to P \in Word Vtx (G)$
12	7	adantr	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to ⟨“ P (0) ”⟩ \in Word Vtx (G)$
13		elfzonn0	$⊢ i \in (0 ..^N - 1) \to i \in ℕ_{0}$
14	13	adantl	$⊢ (N \in ℕ \land i \in (0 ..^N - 1)) \to i \in ℕ_{0}$
15		nnz	$⊢ N \in ℕ \to N \in ℤ$
16	15	adantr	$⊢ (N \in ℕ \land i \in (0 ..^N - 1)) \to N \in ℤ$
17		elfzo0	$⊢ i \in (0 ..^N - 1) \leftrightarrow (i \in ℕ_{0} \land N - 1 \in ℕ \land i < N - 1)$
18		nn0re	$⊢ i \in ℕ_{0} \to i \in ℝ$
19	18	adantr	$⊢ (i \in ℕ_{0} \land N \in ℕ) \to i \in ℝ$
20		nnre	$⊢ N \in ℕ \to N \in ℝ$
21		peano2rem	$⊢ N \in ℝ \to N - 1 \in ℝ$
22	20 21	syl	$⊢ N \in ℕ \to N - 1 \in ℝ$
23	22	adantl	$⊢ (i \in ℕ_{0} \land N \in ℕ) \to N - 1 \in ℝ$
24	20	adantl	$⊢ (i \in ℕ_{0} \land N \in ℕ) \to N \in ℝ$
25	19 23 24	3jca	$⊢ (i \in ℕ_{0} \land N \in ℕ) \to (i \in ℝ \land N - 1 \in ℝ \land N \in ℝ)$
26	25	adantr	$⊢ ((i \in ℕ_{0} \land N \in ℕ) \land i < N - 1) \to (i \in ℝ \land N - 1 \in ℝ \land N \in ℝ)$
27	20	ltm1d	$⊢ N \in ℕ \to N - 1 < N$
28	27	adantl	$⊢ (i \in ℕ_{0} \land N \in ℕ) \to N - 1 < N$
29	28	anim1ci	$⊢ ((i \in ℕ_{0} \land N \in ℕ) \land i < N - 1) \to (i < N - 1 \land N - 1 < N)$
30		lttr	$⊢ (i \in ℝ \land N - 1 \in ℝ \land N \in ℝ) \to ((i < N - 1 \land N - 1 < N) \to i < N)$
31	26 29 30	sylc	$⊢ ((i \in ℕ_{0} \land N \in ℕ) \land i < N - 1) \to i < N$
32	31	ex	$⊢ (i \in ℕ_{0} \land N \in ℕ) \to (i < N - 1 \to i < N)$
33	32	impancom	$⊢ (i \in ℕ_{0} \land i < N - 1) \to (N \in ℕ \to i < N)$
34	33	3adant2	$⊢ (i \in ℕ_{0} \land N - 1 \in ℕ \land i < N - 1) \to (N \in ℕ \to i < N)$
35	17 34	sylbi	$⊢ i \in (0 ..^N - 1) \to (N \in ℕ \to i < N)$
36	35	impcom	$⊢ (N \in ℕ \land i \in (0 ..^N - 1)) \to i < N$
37		elfzo0z	$⊢ i \in (0 ..^N) \leftrightarrow (i \in ℕ_{0} \land N \in ℤ \land i < N)$
38	14 16 36 37	syl3anbrc	$⊢ (N \in ℕ \land i \in (0 ..^N - 1)) \to i \in (0 ..^N)$
39	38	adantlr	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to i \in (0 ..^N)$
40		oveq2	$⊢ \|P\| = N \to (0 ..^\|P\|) = (0 ..^N)$
41	40	eleq2d	$⊢ \|P\| = N \to (i \in (0 ..^\|P\|) \leftrightarrow i \in (0 ..^N))$
42	41	ad2antll	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (i \in (0 ..^\|P\|) \leftrightarrow i \in (0 ..^N))$
43	42	adantr	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to (i \in (0 ..^\|P\|) \leftrightarrow i \in (0 ..^N))$
44	39 43	mpbird	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to i \in (0 ..^\|P\|)$
45		ccatval1	$⊢ (P \in Word Vtx (G) \land ⟨“ P (0) ”⟩ \in Word Vtx (G) \land i \in (0 ..^\|P\|)) \to (P ++ ⟨“ P (0) ”⟩) (i) = P (i)$
46	11 12 44 45	syl3anc	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to (P ++ ⟨“ P (0) ”⟩) (i) = P (i)$
47		elfzom1p1elfzo	$⊢ (N \in ℕ \land i \in (0 ..^N - 1)) \to i + 1 \in (0 ..^N)$
48	47	adantlr	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to i + 1 \in (0 ..^N)$
49	40	ad2antll	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (0 ..^\|P\|) = (0 ..^N)$
50	49	adantr	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to (0 ..^\|P\|) = (0 ..^N)$
51	48 50	eleqtrrd	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to i + 1 \in (0 ..^\|P\|)$
52		ccatval1	$⊢ (P \in Word Vtx (G) \land ⟨“ P (0) ”⟩ \in Word Vtx (G) \land i + 1 \in (0 ..^\|P\|)) \to (P ++ ⟨“ P (0) ”⟩) (i + 1) = P (i + 1)$
53	11 12 51 52	syl3anc	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to (P ++ ⟨“ P (0) ”⟩) (i + 1) = P (i + 1)$
54	46 53	preq12d	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} = \{P (i), P (i + 1)\}$
55	54	eleq1d	$⊢ ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \land i \in (0 ..^N - 1)) \to (\{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow \{P (i), P (i + 1)\} \in Edg (G))$
56	55	ralbidva	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (\forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G))$
57	56	biimprcd	$⊢ \forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \to ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G))$
58	57	adantr	$⊢ (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G)) \to ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G))$
59	58	expdcom	$⊢ N \in ℕ \to ((P \in Word Vtx (G) \land \|P\| = N) \to ((\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G)) \to \forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)))$
60	59	3imp	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to \forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)$
61		fzo0end	$⊢ N \in ℕ \to N - 1 \in (0 ..^N)$
62	40	eleq2d	$⊢ \|P\| = N \to (N - 1 \in (0 ..^\|P\|) \leftrightarrow N - 1 \in (0 ..^N))$
63	62	adantl	$⊢ (P \in Word Vtx (G) \land \|P\| = N) \to (N - 1 \in (0 ..^\|P\|) \leftrightarrow N - 1 \in (0 ..^N))$
64	61 63	syl5ibrcom	$⊢ N \in ℕ \to ((P \in Word Vtx (G) \land \|P\| = N) \to N - 1 \in (0 ..^\|P\|))$
65	64	imp	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to N - 1 \in (0 ..^\|P\|)$
66		ccatval1	$⊢ (P \in Word Vtx (G) \land ⟨“ P (0) ”⟩ \in Word Vtx (G) \land N - 1 \in (0 ..^\|P\|)) \to (P ++ ⟨“ P (0) ”⟩) (N - 1) = P (N - 1)$
67	5 7 65 66	syl3anc	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (P ++ ⟨“ P (0) ”⟩) (N - 1) = P (N - 1)$
68		lsw	$⊢ P \in Word Vtx (G) \to lastS (P) = P (\|P\| - 1)$
69	68	adantr	$⊢ (P \in Word Vtx (G) \land \|P\| = N) \to lastS (P) = P (\|P\| - 1)$
70		fvoveq1	$⊢ \|P\| = N \to P (\|P\| - 1) = P (N - 1)$
71	70	adantl	$⊢ (P \in Word Vtx (G) \land \|P\| = N) \to P (\|P\| - 1) = P (N - 1)$
72	69 71	eqtr2d	$⊢ (P \in Word Vtx (G) \land \|P\| = N) \to P (N - 1) = lastS (P)$
73	72	adantl	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to P (N - 1) = lastS (P)$
74	67 73	eqtr2d	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to lastS (P) = (P ++ ⟨“ P (0) ”⟩) (N - 1)$
75		nncn	$⊢ N \in ℕ \to N \in ℂ$
76		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
77	75 76	npcand	$⊢ N \in ℕ \to N - 1 + 1 = N$
78	77	fveq2d	$⊢ N \in ℕ \to (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1) = (P ++ ⟨“ P (0) ”⟩) (N)$
79	78	adantr	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1) = (P ++ ⟨“ P (0) ”⟩) (N)$
80		fveq2	$⊢ \|P\| = N \to (P ++ ⟨“ P (0) ”⟩) (\|P\|) = (P ++ ⟨“ P (0) ”⟩) (N)$
81	80	ad2antll	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (P ++ ⟨“ P (0) ”⟩) (\|P\|) = (P ++ ⟨“ P (0) ”⟩) (N)$
82		ccatws1ls	$⊢ (P \in Word Vtx (G) \land P (0) \in Vtx (G)) \to (P ++ ⟨“ P (0) ”⟩) (\|P\|) = P (0)$
83	5 6 82	syl2anc	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (P ++ ⟨“ P (0) ”⟩) (\|P\|) = P (0)$
84	79 81 83	3eqtr2rd	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to P (0) = (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)$
85	74 84	preq12d	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \{lastS (P), P (0)\} = \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\}$
86	85	eleq1d	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (\{lastS (P), P (0)\} \in Edg (G) \leftrightarrow \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\} \in Edg (G))$
87	86	biimpcd	$⊢ \{lastS (P), P (0)\} \in Edg (G) \to ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\} \in Edg (G))$
88	87	adantl	$⊢ (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G)) \to ((N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\} \in Edg (G))$
89	88	expdcom	$⊢ N \in ℕ \to ((P \in Word Vtx (G) \land \|P\| = N) \to ((\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G)) \to \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\} \in Edg (G)))$
90	89	3imp	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\} \in Edg (G)$
91		ovex	$⊢ N - 1 \in V$
92		fveq2	$⊢ i = N - 1 \to (P ++ ⟨“ P (0) ”⟩) (i) = (P ++ ⟨“ P (0) ”⟩) (N - 1)$
93		fvoveq1	$⊢ i = N - 1 \to (P ++ ⟨“ P (0) ”⟩) (i + 1) = (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)$
94	92 93	preq12d	$⊢ i = N - 1 \to \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} = \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\}$
95	94	eleq1d	$⊢ i = N - 1 \to (\{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\} \in Edg (G))$
96	91 95	ralsn	$⊢ \forall i \in \{N - 1\} \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow \{(P ++ ⟨“ P (0) ”⟩) (N - 1), (P ++ ⟨“ P (0) ”⟩) (N - 1 + 1)\} \in Edg (G)$
97	90 96	sylibr	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to \forall i \in \{N - 1\} \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)$
98	75 76 76	addsubd	$⊢ N \in ℕ \to N + 1 - 1 = N - 1 + 1$
99	98	oveq2d	$⊢ N \in ℕ \to (0 ..^N + 1 - 1) = (0 ..^N - 1 + 1)$
100		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
101		elnn0uz	$⊢ N - 1 \in ℕ_{0} \leftrightarrow N - 1 \in ℤ_{\geq 0}$
102	100 101	sylib	$⊢ N \in ℕ \to N - 1 \in ℤ_{\geq 0}$
103		fzosplitsn	$⊢ N - 1 \in ℤ_{\geq 0} \to (0 ..^N - 1 + 1) = (0 ..^N - 1) \cup \{N - 1\}$
104	102 103	syl	$⊢ N \in ℕ \to (0 ..^N - 1 + 1) = (0 ..^N - 1) \cup \{N - 1\}$
105	99 104	eqtrd	$⊢ N \in ℕ \to (0 ..^N + 1 - 1) = (0 ..^N - 1) \cup \{N - 1\}$
106	105	raleqdv	$⊢ N \in ℕ \to (\forall i \in (0 ..^N + 1 - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in ((0 ..^N - 1) \cup \{N - 1\}) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G))$
107		ralunb	$⊢ \forall i \in ((0 ..^N - 1) \cup \{N - 1\}) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow (\forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \land \forall i \in \{N - 1\} \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G))$
108	106 107	bitrdi	$⊢ N \in ℕ \to (\forall i \in (0 ..^N + 1 - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow (\forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \land \forall i \in \{N - 1\} \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)))$
109	108	3ad2ant1	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to (\forall i \in (0 ..^N + 1 - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow (\forall i \in (0 ..^N - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \land \forall i \in \{N - 1\} \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)))$
110	60 97 109	mpbir2and	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to \forall i \in (0 ..^N + 1 - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)$
111		ccatlen	$⊢ (P \in Word Vtx (G) \land ⟨“ P (0) ”⟩ \in Word Vtx (G)) \to \|P ++ ⟨“ P (0) ”⟩\| = \|P\| + \|⟨“ P (0) ”⟩\|$
112	5 7 111	syl2anc	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \|P ++ ⟨“ P (0) ”⟩\| = \|P\| + \|⟨“ P (0) ”⟩\|$
113		id	$⊢ \|P\| = N \to \|P\| = N$
114		s1len	$⊢ \|⟨“ P (0) ”⟩\| = 1$
115	114	a1i	$⊢ \|P\| = N \to \|⟨“ P (0) ”⟩\| = 1$
116	113 115	oveq12d	$⊢ \|P\| = N \to \|P\| + \|⟨“ P (0) ”⟩\| = N + 1$
117	116	ad2antll	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \|P\| + \|⟨“ P (0) ”⟩\| = N + 1$
118	112 117	eqtrd	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to \|P ++ ⟨“ P (0) ”⟩\| = N + 1$
119	118	3adant3	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to \|P ++ ⟨“ P (0) ”⟩\| = N + 1$
120	119	oveq1d	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to \|P ++ ⟨“ P (0) ”⟩\| - 1 = N + 1 - 1$
121	120	oveq2d	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) = (0 ..^N + 1 - 1)$
122	121	raleqdv	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to (\forall i \in (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^N + 1 - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G))$
123	110 122	mpbird	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to \forall i \in (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)$
124	4 10 123	3jca	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to (P ++ ⟨“ P (0) ”⟩ \neq \emptyset \land P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G) \land \forall i \in (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G))$
125		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
126		iswwlksn	$⊢ N \in ℕ_{0} \to (P ++ ⟨“ P (0) ”⟩ \in (N WWalksN G) \leftrightarrow (P ++ ⟨“ P (0) ”⟩ \in WWalks (G) \land \|P ++ ⟨“ P (0) ”⟩\| = N + 1))$
127	125 126	syl	$⊢ N \in ℕ \to (P ++ ⟨“ P (0) ”⟩ \in (N WWalksN G) \leftrightarrow (P ++ ⟨“ P (0) ”⟩ \in WWalks (G) \land \|P ++ ⟨“ P (0) ”⟩\| = N + 1))$
128		eqid	$⊢ Vtx (G) = Vtx (G)$
129		eqid	$⊢ Edg (G) = Edg (G)$
130	128 129	iswwlks	$⊢ P ++ ⟨“ P (0) ”⟩ \in WWalks (G) \leftrightarrow (P ++ ⟨“ P (0) ”⟩ \neq \emptyset \land P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G) \land \forall i \in (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G))$
131	130	anbi1i	$⊢ (P ++ ⟨“ P (0) ”⟩ \in WWalks (G) \land \|P ++ ⟨“ P (0) ”⟩\| = N + 1) \leftrightarrow ((P ++ ⟨“ P (0) ”⟩ \neq \emptyset \land P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G) \land \forall i \in (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)) \land \|P ++ ⟨“ P (0) ”⟩\| = N + 1)$
132	127 131	bitrdi	$⊢ N \in ℕ \to (P ++ ⟨“ P (0) ”⟩ \in (N WWalksN G) \leftrightarrow ((P ++ ⟨“ P (0) ”⟩ \neq \emptyset \land P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G) \land \forall i \in (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)) \land \|P ++ ⟨“ P (0) ”⟩\| = N + 1))$
133	132	3ad2ant1	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to (P ++ ⟨“ P (0) ”⟩ \in (N WWalksN G) \leftrightarrow ((P ++ ⟨“ P (0) ”⟩ \neq \emptyset \land P ++ ⟨“ P (0) ”⟩ \in Word Vtx (G) \land \forall i \in (0 ..^\|P ++ ⟨“ P (0) ”⟩\| - 1) \{(P ++ ⟨“ P (0) ”⟩) (i), (P ++ ⟨“ P (0) ”⟩) (i + 1)\} \in Edg (G)) \land \|P ++ ⟨“ P (0) ”⟩\| = N + 1))$
134	124 119 133	mpbir2and	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to P ++ ⟨“ P (0) ”⟩ \in (N WWalksN G)$
135		lswccats1	$⊢ (P \in Word Vtx (G) \land P (0) \in Vtx (G)) \to lastS (P ++ ⟨“ P (0) ”⟩) = P (0)$
136	5 6 135	syl2anc	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to lastS (P ++ ⟨“ P (0) ”⟩) = P (0)$
137		lbfzo0	$⊢ 0 \in (0 ..^N) \leftrightarrow N \in ℕ$
138	137	biimpri	$⊢ N \in ℕ \to 0 \in (0 ..^N)$
139	40	eleq2d	$⊢ \|P\| = N \to (0 \in (0 ..^\|P\|) \leftrightarrow 0 \in (0 ..^N))$
140	139	adantl	$⊢ (P \in Word Vtx (G) \land \|P\| = N) \to (0 \in (0 ..^\|P\|) \leftrightarrow 0 \in (0 ..^N))$
141	138 140	syl5ibrcom	$⊢ N \in ℕ \to ((P \in Word Vtx (G) \land \|P\| = N) \to 0 \in (0 ..^\|P\|))$
142	141	imp	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to 0 \in (0 ..^\|P\|)$
143		ccatval1	$⊢ (P \in Word Vtx (G) \land ⟨“ P (0) ”⟩ \in Word Vtx (G) \land 0 \in (0 ..^\|P\|)) \to (P ++ ⟨“ P (0) ”⟩) (0) = P (0)$
144	5 7 142 143	syl3anc	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to (P ++ ⟨“ P (0) ”⟩) (0) = P (0)$
145	136 144	eqtr4d	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N)) \to lastS (P ++ ⟨“ P (0) ”⟩) = (P ++ ⟨“ P (0) ”⟩) (0)$
146	145	3adant3	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to lastS (P ++ ⟨“ P (0) ”⟩) = (P ++ ⟨“ P (0) ”⟩) (0)$
147		fveq2	$⊢ w = P ++ ⟨“ P (0) ”⟩ \to lastS (w) = lastS (P ++ ⟨“ P (0) ”⟩)$
148		fveq1	$⊢ w = P ++ ⟨“ P (0) ”⟩ \to w (0) = (P ++ ⟨“ P (0) ”⟩) (0)$
149	147 148	eqeq12d	$⊢ w = P ++ ⟨“ P (0) ”⟩ \to (lastS (w) = w (0) \leftrightarrow lastS (P ++ ⟨“ P (0) ”⟩) = (P ++ ⟨“ P (0) ”⟩) (0))$
150	149 1	elrab2	$⊢ P ++ ⟨“ P (0) ”⟩ \in D \leftrightarrow (P ++ ⟨“ P (0) ”⟩ \in (N WWalksN G) \land lastS (P ++ ⟨“ P (0) ”⟩) = (P ++ ⟨“ P (0) ”⟩) (0))$
151	134 146 150	sylanbrc	$⊢ (N \in ℕ \land (P \in Word Vtx (G) \land \|P\| = N) \land (\forall i \in (0 ..^N - 1) \{P (i), P (i + 1)\} \in Edg (G) \land \{lastS (P), P (0)\} \in Edg (G))) \to P ++ ⟨“ P (0) ”⟩ \in D$

Metamath Proof Explorer

Theorem clwwlkel

Proof