swrdwlk

Description: Two matching subwords of a walk also represent a walk. (Contributed by BTernaryTau, 7-Dec-2023)

		Ref	Expression
	Assertion	swrdwlk	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to (F substr ⟨B, L⟩) Walks (G) (P substr ⟨B, L + 1⟩)$

Proof

Step	Hyp	Ref	Expression
1		pfxwlk	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (F prefix L) Walks (G) (P prefix (L + 1))$
2	1	3adant2	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to (F prefix L) Walks (G) (P prefix (L + 1))$
3		revwlk	$⊢ (F prefix L) Walks (G) (P prefix (L + 1)) \to reverse (F prefix L) Walks (G) reverse (P prefix (L + 1))$
4	2 3	syl	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to reverse (F prefix L) Walks (G) reverse (P prefix (L + 1))$
5		fznn0sub2	$⊢ B \in (0 \dots L) \to L - B \in (0 \dots L)$
6	5	3ad2ant2	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to L - B \in (0 \dots L)$
7		eqid	$⊢ iEdg (G) = iEdg (G)$
8	7	wlkf	$⊢ F Walks (G) P \to F \in Word dom iEdg (G)$
9	8	3ad2ant1	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to F \in Word dom iEdg (G)$
10		pfxcl	$⊢ F \in Word dom iEdg (G) \to F prefix L \in Word dom iEdg (G)$
11		revlen	$⊢ F prefix L \in Word dom iEdg (G) \to \|reverse (F prefix L)\| = \|F prefix L\|$
12	9 10 11	3syl	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to \|reverse (F prefix L)\| = \|F prefix L\|$
13		pfxlen	$⊢ (F \in Word dom iEdg (G) \land L \in (0 \dots \|F\|)) \to \|F prefix L\| = L$
14	8 13	sylan	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to \|F prefix L\| = L$
15	14	3adant2	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to \|F prefix L\| = L$
16	12 15	eqtrd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to \|reverse (F prefix L)\| = L$
17	16	oveq2d	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to (0 \dots \|reverse (F prefix L)\|) = (0 \dots L)$
18	6 17	eleqtrrd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to L - B \in (0 \dots \|reverse (F prefix L)\|)$
19		pfxwlk	$⊢ (reverse (F prefix L) Walks (G) reverse (P prefix (L + 1)) \land L - B \in (0 \dots \|reverse (F prefix L)\|)) \to (reverse (F prefix L) prefix (L - B)) Walks (G) (reverse (P prefix (L + 1)) prefix (L - B + 1))$
20	4 18 19	syl2anc	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to (reverse (F prefix L) prefix (L - B)) Walks (G) (reverse (P prefix (L + 1)) prefix (L - B + 1))$
21		elfzel2	$⊢ B \in (0 \dots L) \to L \in ℤ$
22	21	3ad2ant2	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to L \in ℤ$
23	22	zcnd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to L \in ℂ$
24		1cnd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to 1 \in ℂ$
25		elfzelz	$⊢ B \in (0 \dots L) \to B \in ℤ$
26	25	3ad2ant2	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to B \in ℤ$
27	26	zcnd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to B \in ℂ$
28	23 24 27	addsubd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to L + 1 - B = L - B + 1$
29	28	oveq2d	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to reverse (P prefix (L + 1)) prefix (L + 1 - B) = reverse (P prefix (L + 1)) prefix (L - B + 1)$
30	20 29	breqtrrd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to (reverse (F prefix L) prefix (L - B)) Walks (G) (reverse (P prefix (L + 1)) prefix (L + 1 - B))$
31		revwlk	$⊢ (reverse (F prefix L) prefix (L - B)) Walks (G) (reverse (P prefix (L + 1)) prefix (L + 1 - B)) \to reverse (reverse (F prefix L) prefix (L - B)) Walks (G) reverse (reverse (P prefix (L + 1)) prefix (L + 1 - B))$
32	30 31	syl	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to reverse (reverse (F prefix L) prefix (L - B)) Walks (G) reverse (reverse (P prefix (L + 1)) prefix (L + 1 - B))$
33		swrdrevpfx	$⊢ (F \in Word dom iEdg (G) \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to F substr ⟨B, L⟩ = reverse (reverse (F prefix L) prefix (L - B))$
34	8 33	syl3an1	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to F substr ⟨B, L⟩ = reverse (reverse (F prefix L) prefix (L - B))$
35		eqid	$⊢ Vtx (G) = Vtx (G)$
36	35	wlkpwrd	$⊢ F Walks (G) P \to P \in Word Vtx (G)$
37	36	3ad2ant1	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to P \in Word Vtx (G)$
38		fzelp1	$⊢ B \in (0 \dots L) \to B \in (0 \dots L + 1)$
39	38	3ad2ant2	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to B \in (0 \dots L + 1)$
40		fzp1elp1	$⊢ L \in (0 \dots \|F\|) \to L + 1 \in (0 \dots \|F\| + 1)$
41	40	3ad2ant3	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to L + 1 \in (0 \dots \|F\| + 1)$
42		wlklenvp1	$⊢ F Walks (G) P \to \|P\| = \|F\| + 1$
43	42	3ad2ant1	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to \|P\| = \|F\| + 1$
44	43	oveq2d	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to (0 \dots \|P\|) = (0 \dots \|F\| + 1)$
45	41 44	eleqtrrd	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to L + 1 \in (0 \dots \|P\|)$
46		swrdrevpfx	$⊢ (P \in Word Vtx (G) \land B \in (0 \dots L + 1) \land L + 1 \in (0 \dots \|P\|)) \to P substr ⟨B, L + 1⟩ = reverse (reverse (P prefix (L + 1)) prefix (L + 1 - B))$
47	37 39 45 46	syl3anc	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to P substr ⟨B, L + 1⟩ = reverse (reverse (P prefix (L + 1)) prefix (L + 1 - B))$
48	32 34 47	3brtr4d	$⊢ (F Walks (G) P \land B \in (0 \dots L) \land L \in (0 \dots \|F\|)) \to (F substr ⟨B, L⟩) Walks (G) (P substr ⟨B, L + 1⟩)$

Metamath Proof Explorer

Theorem swrdwlk

Proof