2clwwlk2clwwlklem

		Ref	Expression
	Assertion	2clwwlk2clwwlklem	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2)$

Proof

Step	Hyp	Ref	Expression
1		isclwwlknon	$⊢ W \in (X ClWWalksNOn (G) N) \leftrightarrow (W \in (N ClWWalksN G) \land W (0) = X)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	clwwlknbp	$⊢ W \in (N ClWWalksN G) \to (W \in Word Vtx (G) \land \|W\| = N)$
4		simpll	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to W \in Word Vtx (G)$
5		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
6		eluzfz2	$⊢ N \in ℤ_{\geq 2} \to N \in (2 \dots N)$
7	5 6	syl	$⊢ N \in ℤ_{\geq 3} \to N \in (2 \dots N)$
8	7	adantl	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to N \in (2 \dots N)$
9		oveq2	$⊢ \|W\| = N \to (2 \dots \|W\|) = (2 \dots N)$
10	9	eleq2d	$⊢ \|W\| = N \to (N \in (2 \dots \|W\|) \leftrightarrow N \in (2 \dots N))$
11	10	ad2antlr	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to (N \in (2 \dots \|W\|) \leftrightarrow N \in (2 \dots N))$
12	8 11	mpbird	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to N \in (2 \dots \|W\|)$
13	4 12	jca	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to (W \in Word Vtx (G) \land N \in (2 \dots \|W\|))$
14	13	ex	$⊢ (W \in Word Vtx (G) \land \|W\| = N) \to (N \in ℤ_{\geq 3} \to (W \in Word Vtx (G) \land N \in (2 \dots \|W\|)))$
15	3 14	syl	$⊢ W \in (N ClWWalksN G) \to (N \in ℤ_{\geq 3} \to (W \in Word Vtx (G) \land N \in (2 \dots \|W\|)))$
16	15	adantr	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to (N \in ℤ_{\geq 3} \to (W \in Word Vtx (G) \land N \in (2 \dots \|W\|)))$
17	1 16	sylbi	$⊢ W \in (X ClWWalksNOn (G) N) \to (N \in ℤ_{\geq 3} \to (W \in Word Vtx (G) \land N \in (2 \dots \|W\|)))$
18	17	impcom	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N)) \to (W \in Word Vtx (G) \land N \in (2 \dots \|W\|))$
19		swrds2m	$⊢ (W \in Word Vtx (G) \land N \in (2 \dots \|W\|)) \to W substr ⟨N - 2, N⟩ = ⟨“ W (N - 2) W (N - 1) ”⟩$
20	18 19	syl	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N)) \to W substr ⟨N - 2, N⟩ = ⟨“ W (N - 2) W (N - 1) ”⟩$
21	20	3adant3	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W substr ⟨N - 2, N⟩ = ⟨“ W (N - 2) W (N - 1) ”⟩$
22		simp3	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W (N - 2) = W (0)$
23		eqidd	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W (N - 1) = W (N - 1)$
24	22 23	s2eqd	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to ⟨“ W (N - 2) W (N - 1) ”⟩ = ⟨“ W (0) W (N - 1) ”⟩$
25		simpr	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to W (0) = X$
26		eqidd	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to W (N - 1) = W (N - 1)$
27	25 26	s2eqd	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to ⟨“ W (0) W (N - 1) ”⟩ = ⟨“ X W (N - 1) ”⟩$
28	1 27	sylbi	$⊢ W \in (X ClWWalksNOn (G) N) \to ⟨“ W (0) W (N - 1) ”⟩ = ⟨“ X W (N - 1) ”⟩$
29	28	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to ⟨“ W (0) W (N - 1) ”⟩ = ⟨“ X W (N - 1) ”⟩$
30	21 24 29	3eqtrd	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W substr ⟨N - 2, N⟩ = ⟨“ X W (N - 1) ”⟩$
31		clwwlknonmpo	$⊢ ClWWalksNOn (G) = (v \in Vtx (G), n \in ℕ_{0} ⟼ \{w \in (n ClWWalksN G) \| w (0) = v\})$
32	31	elmpocl1	$⊢ W \in (X ClWWalksNOn (G) N) \to X \in Vtx (G)$
33	32	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to X \in Vtx (G)$
34		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
35		fzo0end	$⊢ N \in ℕ \to N - 1 \in (0 ..^N)$
36	34 35	syl	$⊢ N \in ℤ_{\geq 3} \to N - 1 \in (0 ..^N)$
37	36	adantl	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to N - 1 \in (0 ..^N)$
38		oveq2	$⊢ \|W\| = N \to (0 ..^\|W\|) = (0 ..^N)$
39	38	ad2antlr	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to (0 ..^\|W\|) = (0 ..^N)$
40	39	eleq2d	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to (N - 1 \in (0 ..^\|W\|) \leftrightarrow N - 1 \in (0 ..^N))$
41	37 40	mpbird	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to N - 1 \in (0 ..^\|W\|)$
42		wrdsymbcl	$⊢ (W \in Word Vtx (G) \land N - 1 \in (0 ..^\|W\|)) \to W (N - 1) \in Vtx (G)$
43	4 41 42	syl2anc	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land N \in ℤ_{\geq 3}) \to W (N - 1) \in Vtx (G)$
44	43	ex	$⊢ (W \in Word Vtx (G) \land \|W\| = N) \to (N \in ℤ_{\geq 3} \to W (N - 1) \in Vtx (G))$
45	3 44	syl	$⊢ W \in (N ClWWalksN G) \to (N \in ℤ_{\geq 3} \to W (N - 1) \in Vtx (G))$
46	45	adantr	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to (N \in ℤ_{\geq 3} \to W (N - 1) \in Vtx (G))$
47	1 46	sylbi	$⊢ W \in (X ClWWalksNOn (G) N) \to (N \in ℤ_{\geq 3} \to W (N - 1) \in Vtx (G))$
48	47	impcom	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N)) \to W (N - 1) \in Vtx (G)$
49	48	3adant3	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W (N - 1) \in Vtx (G)$
50		preq1	$⊢ W (0) = X \to \{W (0), W (N - 1)\} = \{X, W (N - 1)\}$
51	50	adantl	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to \{W (0), W (N - 1)\} = \{X, W (N - 1)\}$
52	51	eqcomd	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to \{X, W (N - 1)\} = \{W (0), W (N - 1)\}$
53	52	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to \{X, W (N - 1)\} = \{W (0), W (N - 1)\}$
54		prcom	$⊢ \{W (0), W (N - 1)\} = \{W (N - 1), W (0)\}$
55	53 54	eqtrdi	$⊢ (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to \{X, W (N - 1)\} = \{W (N - 1), W (0)\}$
56		eqid	$⊢ Edg (G) = Edg (G)$
57	2 56	clwwlknp	$⊢ W \in (N ClWWalksN G) \to ((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G))$
58	57	adantr	$⊢ (W \in (N ClWWalksN G) \land W (0) = X) \to ((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G))$
59	58	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to ((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G))$
60		lsw	$⊢ W \in Word Vtx (G) \to lastS (W) = W (\|W\| - 1)$
61		fvoveq1	$⊢ \|W\| = N \to W (\|W\| - 1) = W (N - 1)$
62	60 61	sylan9eq	$⊢ (W \in Word Vtx (G) \land \|W\| = N) \to lastS (W) = W (N - 1)$
63	62	adantr	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0))) \to lastS (W) = W (N - 1)$
64	63	preq1d	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0))) \to \{lastS (W), W (0)\} = \{W (N - 1), W (0)\}$
65	64	eleq1d	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0))) \to (\{lastS (W), W (0)\} \in Edg (G) \leftrightarrow \{W (N - 1), W (0)\} \in Edg (G))$
66	65	biimpd	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0))) \to (\{lastS (W), W (0)\} \in Edg (G) \to \{W (N - 1), W (0)\} \in Edg (G))$
67	66	ex	$⊢ (W \in Word Vtx (G) \land \|W\| = N) \to ((N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to (\{lastS (W), W (0)\} \in Edg (G) \to \{W (N - 1), W (0)\} \in Edg (G)))$
68	67	com23	$⊢ (W \in Word Vtx (G) \land \|W\| = N) \to (\{lastS (W), W (0)\} \in Edg (G) \to ((N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to \{W (N - 1), W (0)\} \in Edg (G)))$
69	68	a1d	$⊢ (W \in Word Vtx (G) \land \|W\| = N) \to (\forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \to (\{lastS (W), W (0)\} \in Edg (G) \to ((N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to \{W (N - 1), W (0)\} \in Edg (G))))$
70	69	3imp	$⊢ ((W \in Word Vtx (G) \land \|W\| = N) \land \forall i \in (0 ..^N - 1) \{W (i), W (i + 1)\} \in Edg (G) \land \{lastS (W), W (0)\} \in Edg (G)) \to ((N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to \{W (N - 1), W (0)\} \in Edg (G))$
71	59 70	mpcom	$⊢ (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to \{W (N - 1), W (0)\} \in Edg (G)$
72	55 71	eqeltrd	$⊢ (N \in ℤ_{\geq 3} \land (W \in (N ClWWalksN G) \land W (0) = X) \land W (N - 2) = W (0)) \to \{X, W (N - 1)\} \in Edg (G)$
73	1 72	syl3an2b	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to \{X, W (N - 1)\} \in Edg (G)$
74		eqid	$⊢ ClWWalksNOn (G) = ClWWalksNOn (G)$
75	74 2 56	s2elclwwlknon2	$⊢ (X \in Vtx (G) \land W (N - 1) \in Vtx (G) \land \{X, W (N - 1)\} \in Edg (G)) \to ⟨“ X W (N - 1) ”⟩ \in (X ClWWalksNOn (G) 2)$
76	33 49 73 75	syl3anc	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to ⟨“ X W (N - 1) ”⟩ \in (X ClWWalksNOn (G) 2)$
77	30 76	eqeltrd	$⊢ (N \in ℤ_{\geq 3} \land W \in (X ClWWalksNOn (G) N) \land W (N - 2) = W (0)) \to W substr ⟨N - 2, N⟩ \in (X ClWWalksNOn (G) 2)$

Metamath Proof Explorer

Theorem 2clwwlk2clwwlklem

Proof