pfxwlk

Description: A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023)

		Ref	Expression
	Assertion	pfxwlk	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (F prefix L) Walks (G) (P prefix (L + 1))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ iEdg (G) = iEdg (G)$
2	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom iEdg (G)$
3	2	adantr	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to F \in Word dom iEdg (G)$
4		pfxcl	$⊢ F \in Word dom iEdg (G) \to F prefix L \in Word dom iEdg (G)$
5	3 4	syl	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to F prefix L \in Word dom iEdg (G)$
6		eqid	$⊢ Vtx (G) = Vtx (G)$
7	6	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
8	7	adantr	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
9		elfzuz3	$⊢ L \in (0 \dots \|F\|) \to \|F\| \in ℤ_{\geq L}$
10		fzss2	$⊢ \|F\| \in ℤ_{\geq L} \to (0 \dots L) \subseteq (0 \dots \|F\|)$
11	9 10	syl	$⊢ L \in (0 \dots \|F\|) \to (0 \dots L) \subseteq (0 \dots \|F\|)$
12	11	adantl	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (0 \dots L) \subseteq (0 \dots \|F\|)$
13	8 12	fssresd	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to ({P ↾}_{(0 \dots L)}) : (0 \dots L) ⟶ Vtx (G)$
14		pfxlen	$⊢ (F \in Word dom iEdg (G) \land L \in (0 \dots \|F\|)) \to \|F prefix L\| = L$
15	2 14	sylan	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to \|F prefix L\| = L$
16	15	oveq2d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (0 \dots \|F prefix L\|) = (0 \dots L)$
17	16	feq2d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (({P ↾}_{(0 \dots L)}) : (0 \dots \|F prefix L\|) ⟶ Vtx (G) \leftrightarrow ({P ↾}_{(0 \dots L)}) : (0 \dots L) ⟶ Vtx (G))$
18	13 17	mpbird	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to ({P ↾}_{(0 \dots L)}) : (0 \dots \|F prefix L\|) ⟶ Vtx (G)$
19	6	wlkpwrd	$⊢ F Walks (G) P \to P \in Word Vtx (G)$
20		fzp1elp1	$⊢ L \in (0 \dots \|F\|) \to L + 1 \in (0 \dots \|F\| + 1)$
21	20	adantl	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to L + 1 \in (0 \dots \|F\| + 1)$
22		wlklenvp1	$⊢ F Walks (G) P \to \|P\| = \|F\| + 1$
23	22	oveq2d	$⊢ F Walks (G) P \to (0 \dots \|P\|) = (0 \dots \|F\| + 1)$
24	23	adantr	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (0 \dots \|P\|) = (0 \dots \|F\| + 1)$
25	21 24	eleqtrrd	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to L + 1 \in (0 \dots \|P\|)$
26		pfxres	$⊢ (P \in Word Vtx (G) \land L + 1 \in (0 \dots \|P\|)) \to P prefix (L + 1) = {P ↾}_{(0 ..^L + 1)}$
27	19 25 26	syl2an2r	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to P prefix (L + 1) = {P ↾}_{(0 ..^L + 1)}$
28		elfzelz	$⊢ L \in (0 \dots \|F\|) \to L \in ℤ$
29		fzval3	$⊢ L \in ℤ \to (0 \dots L) = (0 ..^L + 1)$
30	28 29	syl	$⊢ L \in (0 \dots \|F\|) \to (0 \dots L) = (0 ..^L + 1)$
31	30	adantl	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (0 \dots L) = (0 ..^L + 1)$
32	31	reseq2d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to {P ↾}_{(0 \dots L)} = {P ↾}_{(0 ..^L + 1)}$
33	27 32	eqtr4d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to P prefix (L + 1) = {P ↾}_{(0 \dots L)}$
34	33	feq1d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to ((P prefix (L + 1)) : (0 \dots \|F prefix L\|) ⟶ Vtx (G) \leftrightarrow ({P ↾}_{(0 \dots L)}) : (0 \dots \|F prefix L\|) ⟶ Vtx (G))$
35	18 34	mpbird	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (P prefix (L + 1)) : (0 \dots \|F prefix L\|) ⟶ Vtx (G)$
36	6 1	wlkprop	$⊢ F Walks (G) P \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x))))$
37	36	simp3d	$⊢ F Walks (G) P \to \forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x)))$
38	37	adantr	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to \forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x)))$
39	38	adantr	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to \forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x)))$
40	15	oveq2d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (0 ..^\|F prefix L\|) = (0 ..^L)$
41	40	eleq2d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (k \in (0 ..^\|F prefix L\|) \leftrightarrow k \in (0 ..^L))$
42	33	fveq1d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (P prefix (L + 1)) (k) = ({P ↾}_{(0 \dots L)}) (k)$
43	42	adantr	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to (P prefix (L + 1)) (k) = ({P ↾}_{(0 \dots L)}) (k)$
44		fzossfz	$⊢ (0 ..^L) \subseteq (0 \dots L)$
45	44	a1i	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (0 ..^L) \subseteq (0 \dots L)$
46	45	sselda	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to k \in (0 \dots L)$
47	46	fvresd	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to ({P ↾}_{(0 \dots L)}) (k) = P (k)$
48	43 47	eqtr2d	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to P (k) = (P prefix (L + 1)) (k)$
49	33	fveq1d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (P prefix (L + 1)) (k + 1) = ({P ↾}_{(0 \dots L)}) (k + 1)$
50	49	adantr	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to (P prefix (L + 1)) (k + 1) = ({P ↾}_{(0 \dots L)}) (k + 1)$
51		fzofzp1	$⊢ k \in (0 ..^L) \to k + 1 \in (0 \dots L)$
52	51	adantl	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to k + 1 \in (0 \dots L)$
53	52	fvresd	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to ({P ↾}_{(0 \dots L)}) (k + 1) = P (k + 1)$
54	50 53	eqtr2d	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to P (k + 1) = (P prefix (L + 1)) (k + 1)$
55	48 54	jca	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to (P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1))$
56	55	ex	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (k \in (0 ..^L) \to (P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)))$
57	41 56	sylbid	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (k \in (0 ..^\|F prefix L\|) \to (P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)))$
58	57	imp	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to (P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1))$
59	3	ancli	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land F \in Word dom iEdg (G))$
60		simpr	$⊢ (((F Walks (G) P \land L \in (0 \dots \|F\|)) \land F \in Word dom iEdg (G)) \land k \in (0 ..^L)) \to k \in (0 ..^L)$
61	60	fvresd	$⊢ (((F Walks (G) P \land L \in (0 \dots \|F\|)) \land F \in Word dom iEdg (G)) \land k \in (0 ..^L)) \to ({F ↾}_{(0 ..^L)}) (k) = F (k)$
62	61	fveq2d	$⊢ (((F Walks (G) P \land L \in (0 \dots \|F\|)) \land F \in Word dom iEdg (G)) \land k \in (0 ..^L)) \to iEdg (G) (({F ↾}_{(0 ..^L)}) (k)) = iEdg (G) (F (k))$
63	59 62	sylan	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to iEdg (G) (({F ↾}_{(0 ..^L)}) (k)) = iEdg (G) (F (k))$
64	63	eqcomd	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^L)) \to iEdg (G) (F (k)) = iEdg (G) (({F ↾}_{(0 ..^L)}) (k))$
65	64	ex	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (k \in (0 ..^L) \to iEdg (G) (F (k)) = iEdg (G) (({F ↾}_{(0 ..^L)}) (k)))$
66	41 65	sylbid	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (k \in (0 ..^\|F prefix L\|) \to iEdg (G) (F (k)) = iEdg (G) (({F ↾}_{(0 ..^L)}) (k)))$
67	66	imp	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to iEdg (G) (F (k)) = iEdg (G) (({F ↾}_{(0 ..^L)}) (k))$
68		simplr	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to L \in (0 \dots \|F\|)$
69		pfxres	$⊢ (F \in Word dom iEdg (G) \land L \in (0 \dots \|F\|)) \to F prefix L = {F ↾}_{(0 ..^L)}$
70	3 68 69	syl2an2r	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to F prefix L = {F ↾}_{(0 ..^L)}$
71	70	fveq1d	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to (F prefix L) (k) = ({F ↾}_{(0 ..^L)}) (k)$
72	71	fveq2d	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to iEdg (G) ((F prefix L) (k)) = iEdg (G) (({F ↾}_{(0 ..^L)}) (k))$
73	67 72	eqtr4d	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))$
74	58 73	jca	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k)))$
75	9	adantl	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to \|F\| \in ℤ_{\geq L}$
76	15	fveq2d	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to ℤ_{\geq \|F prefix L\|} = ℤ_{\geq L}$
77	75 76	eleqtrrd	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to \|F\| \in ℤ_{\geq \|F prefix L\|}$
78		fzoss2	$⊢ \|F\| \in ℤ_{\geq \|F prefix L\|} \to (0 ..^\|F prefix L\|) \subseteq (0 ..^\|F\|)$
79	77 78	syl	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (0 ..^\|F prefix L\|) \subseteq (0 ..^\|F\|)$
80	79	sselda	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to k \in (0 ..^\|F\|)$
81		wkslem1	$⊢ x = k \to (if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x))) \leftrightarrow if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
82	81	rspcv	$⊢ k \in (0 ..^\|F\|) \to (\forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x))) \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
83	80 82	syl	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to (\forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x))) \to if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))))$
84		eqeq12	$⊢ (P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \to (P (k) = P (k + 1) \leftrightarrow (P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1))$
85	84	adantr	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to (P (k) = P (k + 1) \leftrightarrow (P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1))$
86		simpr	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))$
87		sneq	$⊢ P (k) = (P prefix (L + 1)) (k) \to \{P (k)\} = \{(P prefix (L + 1)) (k)\}$
88	87	adantr	$⊢ (P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \to \{P (k)\} = \{(P prefix (L + 1)) (k)\}$
89	88	adantr	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to \{P (k)\} = \{(P prefix (L + 1)) (k)\}$
90	86 89	eqeq12d	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to (iEdg (G) (F (k)) = \{P (k)\} \leftrightarrow iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\})$
91		preq12	$⊢ (P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \to \{P (k), P (k + 1)\} = \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\}$
92	91	adantr	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to \{P (k), P (k + 1)\} = \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\}$
93	92 86	sseq12d	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to (\{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k)) \leftrightarrow \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k)))$
94	85 90 93	ifpbi123d	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to (if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \leftrightarrow if- ((P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1), iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\}, \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k))))$
95	94	biimpd	$⊢ ((P (k) = (P prefix (L + 1)) (k) \land P (k + 1) = (P prefix (L + 1)) (k + 1)) \land iEdg (G) (F (k)) = iEdg (G) ((F prefix L) (k))) \to (if- (P (k) = P (k + 1), iEdg (G) (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq iEdg (G) (F (k))) \to if- ((P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1), iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\}, \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k))))$
96	74 83 95	sylsyld	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to (\forall x \in (0 ..^\|F\|) if- (P (x) = P (x + 1), iEdg (G) (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq iEdg (G) (F (x))) \to if- ((P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1), iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\}, \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k))))$
97	39 96	mpd	$⊢ ((F Walks (G) P \land L \in (0 \dots \|F\|)) \land k \in (0 ..^\|F prefix L\|)) \to if- ((P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1), iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\}, \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k)))$
98	97	ralrimiva	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to \forall k \in (0 ..^\|F prefix L\|) if- ((P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1), iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\}, \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k)))$
99		wlkv	$⊢ F Walks (G) P \to (G \in V \land F \in V \land P \in V)$
100	99	simp1d	$⊢ F Walks (G) P \to G \in V$
101	100	adantr	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to G \in V$
102	6 1	iswlkg	$⊢ G \in V \to ((F prefix L) Walks (G) (P prefix (L + 1)) \leftrightarrow (F prefix L \in Word dom iEdg (G) \land (P prefix (L + 1)) : (0 \dots \|F prefix L\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F prefix L\|) if- ((P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1), iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\}, \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k)))))$
103	101 102	syl	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to ((F prefix L) Walks (G) (P prefix (L + 1)) \leftrightarrow (F prefix L \in Word dom iEdg (G) \land (P prefix (L + 1)) : (0 \dots \|F prefix L\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F prefix L\|) if- ((P prefix (L + 1)) (k) = (P prefix (L + 1)) (k + 1), iEdg (G) ((F prefix L) (k)) = \{(P prefix (L + 1)) (k)\}, \{(P prefix (L + 1)) (k), (P prefix (L + 1)) (k + 1)\} \subseteq iEdg (G) ((F prefix L) (k)))))$
104	5 35 98 103	mpbir3and	$⊢ (F Walks (G) P \land L \in (0 \dots \|F\|)) \to (F prefix L) Walks (G) (P prefix (L + 1))$

Metamath Proof Explorer

Theorem pfxwlk

Proof