clwwlknonwwlknonb

Description: A word over vertices represents a closed walk of a fixed length N on vertex X iff the word concatenated with X represents a walk of length N on X and X . This theorem would not hold for N = 0 and W = (/) , see clwwlknwwlksnb . (Contributed by AV, 4-Mar-2022) (Revised by AV, 27-Mar-2022)

		Ref	Expression
	Hypothesis	clwwlknonwwlknonb.v	$⊢ V = Vtx (G)$
	Assertion	clwwlknonwwlknonb	$⊢ (W \in Word V \land N \in ℕ) \to (W \in (X ClWWalksNOn (G) N) \leftrightarrow W ++ ⟨“ X ”⟩ \in (X (N WWalksNOn G) X))$

Proof

Step	Hyp	Ref	Expression
1		clwwlknonwwlknonb.v	$⊢ V = Vtx (G)$
2		isclwwlknon	$⊢ W \in (X ClWWalksNOn (G) N) \leftrightarrow (W \in (N ClWWalksN G) \land W (0) = X)$
3		3anan32	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (0) = X \land (W ++ ⟨“ X ”⟩) (N) = X) \leftrightarrow ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \land (W ++ ⟨“ X ”⟩) (0) = X)$
4		s1eq	$⊢ W (0) = X \to ⟨“ W (0) ”⟩ = ⟨“ X ”⟩$
5	4	oveq2d	$⊢ W (0) = X \to W ++ ⟨“ W (0) ”⟩ = W ++ ⟨“ X ”⟩$
6	5	eleq1d	$⊢ W (0) = X \to (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \leftrightarrow W ++ ⟨“ X ”⟩ \in (N WWalksN G))$
7	6	biimpac	$⊢ (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X) \to W ++ ⟨“ X ”⟩ \in (N WWalksN G)$
8	7	adantl	$⊢ ((W \in Word V \land N \in ℕ) \land (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)) \to W ++ ⟨“ X ”⟩ \in (N WWalksN G)$
9		fvex	$⊢ W (0) \in V$
10		eleq1	$⊢ W (0) = X \to (W (0) \in V \leftrightarrow X \in V)$
11	9 10	mpbii	$⊢ W (0) = X \to X \in V$
12		eqid	$⊢ Edg (G) = Edg (G)$
13	1 12	wwlknp	$⊢ W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1 \land \forall i \in (0 ..^N) \{(W ++ ⟨“ X ”⟩) (i), (W ++ ⟨“ X ”⟩) (i + 1)\} \in Edg (G))$
14		simprrl	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (X \in V \land (W \in Word V \land N \in ℕ))) \to W \in Word V$
15		simpl	$⊢ (W \in Word V \land N \in ℕ) \to W \in Word V$
16	15	anim2i	$⊢ (X \in V \land (W \in Word V \land N \in ℕ)) \to (X \in V \land W \in Word V)$
17	16	ancomd	$⊢ (X \in V \land (W \in Word V \land N \in ℕ)) \to (W \in Word V \land X \in V)$
18		ccats1alpha	$⊢ (W \in Word V \land X \in V) \to (W ++ ⟨“ X ”⟩ \in Word V \leftrightarrow (W \in Word V \land X \in V))$
19	17 18	syl	$⊢ (X \in V \land (W \in Word V \land N \in ℕ)) \to (W ++ ⟨“ X ”⟩ \in Word V \leftrightarrow (W \in Word V \land X \in V))$
20		simpr	$⊢ (W \in Word V \land X \in V) \to X \in V$
21	19 20	biimtrdi	$⊢ (X \in V \land (W \in Word V \land N \in ℕ)) \to (W ++ ⟨“ X ”⟩ \in Word V \to X \in V)$
22	21	com12	$⊢ W ++ ⟨“ X ”⟩ \in Word V \to ((X \in V \land (W \in Word V \land N \in ℕ)) \to X \in V)$
23	22	adantr	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \to ((X \in V \land (W \in Word V \land N \in ℕ)) \to X \in V)$
24	23	imp	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (X \in V \land (W \in Word V \land N \in ℕ))) \to X \in V$
25		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
26		ccatws1lenp1b	$⊢ (W \in Word V \land N \in ℕ_{0}) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \leftrightarrow \|W\| = N)$
27	25 26	sylan2	$⊢ (W \in Word V \land N \in ℕ) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \leftrightarrow \|W\| = N)$
28	27	biimpd	$⊢ (W \in Word V \land N \in ℕ) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \to \|W\| = N)$
29	28	adantl	$⊢ (X \in V \land (W \in Word V \land N \in ℕ)) \to (\|W ++ ⟨“ X ”⟩\| = N + 1 \to \|W\| = N)$
30	29	com12	$⊢ \|W ++ ⟨“ X ”⟩\| = N + 1 \to ((X \in V \land (W \in Word V \land N \in ℕ)) \to \|W\| = N)$
31	30	adantl	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \to ((X \in V \land (W \in Word V \land N \in ℕ)) \to \|W\| = N)$
32	31	imp	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (X \in V \land (W \in Word V \land N \in ℕ))) \to \|W\| = N$
33	32	eqcomd	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (X \in V \land (W \in Word V \land N \in ℕ))) \to N = \|W\|$
34	14 24 33	3jca	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (X \in V \land (W \in Word V \land N \in ℕ))) \to (W \in Word V \land X \in V \land N = \|W\|)$
35	34	ex	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \to ((X \in V \land (W \in Word V \land N \in ℕ)) \to (W \in Word V \land X \in V \land N = \|W\|))$
36	35	3adant3	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1 \land \forall i \in (0 ..^N) \{(W ++ ⟨“ X ”⟩) (i), (W ++ ⟨“ X ”⟩) (i + 1)\} \in Edg (G)) \to ((X \in V \land (W \in Word V \land N \in ℕ)) \to (W \in Word V \land X \in V \land N = \|W\|))$
37	13 36	syl	$⊢ W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to ((X \in V \land (W \in Word V \land N \in ℕ)) \to (W \in Word V \land X \in V \land N = \|W\|))$
38	37	expd	$⊢ W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to (X \in V \to ((W \in Word V \land N \in ℕ) \to (W \in Word V \land X \in V \land N = \|W\|)))$
39	11 38	syl5com	$⊢ W (0) = X \to (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to ((W \in Word V \land N \in ℕ) \to (W \in Word V \land X \in V \land N = \|W\|)))$
40	6 39	sylbid	$⊢ W (0) = X \to (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \to ((W \in Word V \land N \in ℕ) \to (W \in Word V \land X \in V \land N = \|W\|)))$
41	40	com13	$⊢ (W \in Word V \land N \in ℕ) \to (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \to (W (0) = X \to (W \in Word V \land X \in V \land N = \|W\|)))$
42	41	imp32	$⊢ ((W \in Word V \land N \in ℕ) \land (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)) \to (W \in Word V \land X \in V \land N = \|W\|)$
43		ccats1val2	$⊢ (W \in Word V \land X \in V \land N = \|W\|) \to (W ++ ⟨“ X ”⟩) (N) = X$
44	42 43	syl	$⊢ ((W \in Word V \land N \in ℕ) \land (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)) \to (W ++ ⟨“ X ”⟩) (N) = X$
45		ccat1st1st	$⊢ W \in Word V \to (W ++ ⟨“ W (0) ”⟩) (0) = W (0)$
46	45	adantr	$⊢ (W \in Word V \land N \in ℕ) \to (W ++ ⟨“ W (0) ”⟩) (0) = W (0)$
47	5	fveq1d	$⊢ W (0) = X \to (W ++ ⟨“ W (0) ”⟩) (0) = (W ++ ⟨“ X ”⟩) (0)$
48	47	eqeq1d	$⊢ W (0) = X \to ((W ++ ⟨“ W (0) ”⟩) (0) = W (0) \leftrightarrow (W ++ ⟨“ X ”⟩) (0) = W (0))$
49	48	adantl	$⊢ (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X) \to ((W ++ ⟨“ W (0) ”⟩) (0) = W (0) \leftrightarrow (W ++ ⟨“ X ”⟩) (0) = W (0))$
50	46 49	syl5ibcom	$⊢ (W \in Word V \land N \in ℕ) \to ((W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X) \to (W ++ ⟨“ X ”⟩) (0) = W (0))$
51	50	imp	$⊢ ((W \in Word V \land N \in ℕ) \land (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)) \to (W ++ ⟨“ X ”⟩) (0) = W (0)$
52		simprr	$⊢ ((W \in Word V \land N \in ℕ) \land (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)) \to W (0) = X$
53	51 52	eqtrd	$⊢ ((W \in Word V \land N \in ℕ) \land (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)) \to (W ++ ⟨“ X ”⟩) (0) = X$
54	8 44 53	jca31	$⊢ ((W \in Word V \land N \in ℕ) \land (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)) \to ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \land (W ++ ⟨“ X ”⟩) (0) = X)$
55	54	ex	$⊢ (W \in Word V \land N \in ℕ) \to ((W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X) \to ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \land (W ++ ⟨“ X ”⟩) (0) = X))$
56		simprl	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (W \in Word V \land N \in ℕ)) \to W \in Word V$
57	27	biimpcd	$⊢ \|W ++ ⟨“ X ”⟩\| = N + 1 \to ((W \in Word V \land N \in ℕ) \to \|W\| = N)$
58	57	adantl	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \to ((W \in Word V \land N \in ℕ) \to \|W\| = N)$
59	58	imp	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (W \in Word V \land N \in ℕ)) \to \|W\| = N$
60	59	eqcomd	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (W \in Word V \land N \in ℕ)) \to N = \|W\|$
61	56 60	jca	$⊢ ((W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \land (W \in Word V \land N \in ℕ)) \to (W \in Word V \land N = \|W\|)$
62	61	ex	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1) \to ((W \in Word V \land N \in ℕ) \to (W \in Word V \land N = \|W\|))$
63	62	3adant3	$⊢ (W ++ ⟨“ X ”⟩ \in Word V \land \|W ++ ⟨“ X ”⟩\| = N + 1 \land \forall i \in (0 ..^N) \{(W ++ ⟨“ X ”⟩) (i), (W ++ ⟨“ X ”⟩) (i + 1)\} \in Edg (G)) \to ((W \in Word V \land N \in ℕ) \to (W \in Word V \land N = \|W\|))$
64	13 63	syl	$⊢ W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to ((W \in Word V \land N \in ℕ) \to (W \in Word V \land N = \|W\|))$
65	64	imp	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W \in Word V \land N \in ℕ)) \to (W \in Word V \land N = \|W\|)$
66		eleq1	$⊢ N = \|W\| \to (N \in ℕ \leftrightarrow \|W\| \in ℕ)$
67		lbfzo0	$⊢ 0 \in (0 ..^\|W\|) \leftrightarrow \|W\| \in ℕ$
68	67	biimpri	$⊢ \|W\| \in ℕ \to 0 \in (0 ..^\|W\|)$
69	66 68	biimtrdi	$⊢ N = \|W\| \to (N \in ℕ \to 0 \in (0 ..^\|W\|))$
70	69	com12	$⊢ N \in ℕ \to (N = \|W\| \to 0 \in (0 ..^\|W\|))$
71	70	ad2antll	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W \in Word V \land N \in ℕ)) \to (N = \|W\| \to 0 \in (0 ..^\|W\|))$
72	71	anim2d	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W \in Word V \land N \in ℕ)) \to ((W \in Word V \land N = \|W\|) \to (W \in Word V \land 0 \in (0 ..^\|W\|)))$
73	65 72	mpd	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W \in Word V \land N \in ℕ)) \to (W \in Word V \land 0 \in (0 ..^\|W\|))$
74		ccats1val1	$⊢ (W \in Word V \land 0 \in (0 ..^\|W\|)) \to (W ++ ⟨“ X ”⟩) (0) = W (0)$
75	73 74	syl	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W \in Word V \land N \in ℕ)) \to (W ++ ⟨“ X ”⟩) (0) = W (0)$
76	75	eqeq1d	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W \in Word V \land N \in ℕ)) \to ((W ++ ⟨“ X ”⟩) (0) = X \leftrightarrow W (0) = X)$
77	76	biimpd	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W \in Word V \land N \in ℕ)) \to ((W ++ ⟨“ X ”⟩) (0) = X \to W (0) = X)$
78	77	ex	$⊢ W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to ((W \in Word V \land N \in ℕ) \to ((W ++ ⟨“ X ”⟩) (0) = X \to W (0) = X))$
79	78	adantr	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \to ((W \in Word V \land N \in ℕ) \to ((W ++ ⟨“ X ”⟩) (0) = X \to W (0) = X))$
80	79	com3r	$⊢ (W ++ ⟨“ X ”⟩) (0) = X \to ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \to ((W \in Word V \land N \in ℕ) \to W (0) = X))$
81	80	impcom	$⊢ ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \land (W ++ ⟨“ X ”⟩) (0) = X) \to ((W \in Word V \land N \in ℕ) \to W (0) = X)$
82	6	biimparc	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land W (0) = X) \to W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G)$
83		simpr	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land W (0) = X) \to W (0) = X$
84	82 83	jca	$⊢ (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land W (0) = X) \to (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X)$
85	84	ex	$⊢ W ++ ⟨“ X ”⟩ \in (N WWalksN G) \to (W (0) = X \to (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X))$
86	85	ad2antrr	$⊢ ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \land (W ++ ⟨“ X ”⟩) (0) = X) \to (W (0) = X \to (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X))$
87	81 86	syldc	$⊢ (W \in Word V \land N \in ℕ) \to (((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \land (W ++ ⟨“ X ”⟩) (0) = X) \to (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X))$
88	55 87	impbid	$⊢ (W \in Word V \land N \in ℕ) \to ((W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X) \leftrightarrow ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (N) = X) \land (W ++ ⟨“ X ”⟩) (0) = X))$
89	3 88	bitr4id	$⊢ (W \in Word V \land N \in ℕ) \to ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (0) = X \land (W ++ ⟨“ X ”⟩) (N) = X) \leftrightarrow (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X))$
90	1	clwwlknwwlksnb	$⊢ (W \in Word V \land N \in ℕ) \to (W \in (N ClWWalksN G) \leftrightarrow W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G))$
91	90	anbi1d	$⊢ (W \in Word V \land N \in ℕ) \to ((W \in (N ClWWalksN G) \land W (0) = X) \leftrightarrow (W ++ ⟨“ W (0) ”⟩ \in (N WWalksN G) \land W (0) = X))$
92	89 91	bitr4d	$⊢ (W \in Word V \land N \in ℕ) \to ((W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (0) = X \land (W ++ ⟨“ X ”⟩) (N) = X) \leftrightarrow (W \in (N ClWWalksN G) \land W (0) = X))$
93	2 92	bitr4id	$⊢ (W \in Word V \land N \in ℕ) \to (W \in (X ClWWalksNOn (G) N) \leftrightarrow (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (0) = X \land (W ++ ⟨“ X ”⟩) (N) = X))$
94		wwlknon	$⊢ W ++ ⟨“ X ”⟩ \in (X (N WWalksNOn G) X) \leftrightarrow (W ++ ⟨“ X ”⟩ \in (N WWalksN G) \land (W ++ ⟨“ X ”⟩) (0) = X \land (W ++ ⟨“ X ”⟩) (N) = X)$
95	93 94	bitr4di	$⊢ (W \in Word V \land N \in ℕ) \to (W \in (X ClWWalksNOn (G) N) \leftrightarrow W ++ ⟨“ X ”⟩ \in (X (N WWalksNOn G) X))$

Metamath Proof Explorer

Theorem clwwlknonwwlknonb

Proof