wlkres

Description: The restriction <. H , Q >. of a walk <. F , P >. to an initial segment of the walk (of length N ) forms a walk on the subgraph S consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 5-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

	Ref	Expression
Hypotheses	wlkres.v	$⊢ V = Vtx (G)$
	wlkres.i	$⊢ I = iEdg (G)$
	wlkres.d	$⊢ φ \to F Walks (G) P$
	wlkres.n	$⊢ φ \to N \in (0 ..^\|F\|)$
	wlkres.s	$⊢ φ \to Vtx (S) = V$
	wlkres.e	$⊢ φ \to iEdg (S) = {I ↾}_{F [(0 ..^N)]}$
	wlkres.h	$⊢ H = F prefix N$
	wlkres.q	$⊢ Q = {P ↾}_{(0 \dots N)}$
Assertion	wlkres	$⊢ φ \to H Walks (S) Q$

Proof

Step	Hyp	Ref	Expression
1		wlkres.v	$⊢ V = Vtx (G)$
2		wlkres.i	$⊢ I = iEdg (G)$
3		wlkres.d	$⊢ φ \to F Walks (G) P$
4		wlkres.n	$⊢ φ \to N \in (0 ..^\|F\|)$
5		wlkres.s	$⊢ φ \to Vtx (S) = V$
6		wlkres.e	$⊢ φ \to iEdg (S) = {I ↾}_{F [(0 ..^N)]}$
7		wlkres.h	$⊢ H = F prefix N$
8		wlkres.q	$⊢ Q = {P ↾}_{(0 \dots N)}$
9	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
10		pfxwrdsymb	$⊢ F \in Word dom I \to F prefix N \in Word F [(0 ..^N)]$
11	3 9 10	3syl	$⊢ φ \to F prefix N \in Word F [(0 ..^N)]$
12	7	a1i	$⊢ φ \to H = F prefix N$
13	6	dmeqd	$⊢ φ \to dom iEdg (S) = dom ({I ↾}_{F [(0 ..^N)]})$
14	3 9	syl	$⊢ φ \to F \in Word dom I$
15		wrdf	$⊢ F \in Word dom I \to F : (0 ..^\|F\|) ⟶ dom I$
16		fimass	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to F [(0 ..^N)] \subseteq dom I$
17	14 15 16	3syl	$⊢ φ \to F [(0 ..^N)] \subseteq dom I$
18		ssdmres	$⊢ F [(0 ..^N)] \subseteq dom I \leftrightarrow dom ({I ↾}_{F [(0 ..^N)]}) = F [(0 ..^N)]$
19	17 18	sylib	$⊢ φ \to dom ({I ↾}_{F [(0 ..^N)]}) = F [(0 ..^N)]$
20	13 19	eqtrd	$⊢ φ \to dom iEdg (S) = F [(0 ..^N)]$
21		wrdeq	$⊢ dom iEdg (S) = F [(0 ..^N)] \to Word dom iEdg (S) = Word F [(0 ..^N)]$
22	20 21	syl	$⊢ φ \to Word dom iEdg (S) = Word F [(0 ..^N)]$
23	11 12 22	3eltr4d	$⊢ φ \to H \in Word dom iEdg (S)$
24	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
25	3 24	syl	$⊢ φ \to P : (0 \dots \|F\|) ⟶ V$
26	5	feq3d	$⊢ φ \to (P : (0 \dots \|F\|) ⟶ Vtx (S) \leftrightarrow P : (0 \dots \|F\|) ⟶ V)$
27	25 26	mpbird	$⊢ φ \to P : (0 \dots \|F\|) ⟶ Vtx (S)$
28		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
29	28 4	sseldi	$⊢ φ \to N \in (0 \dots \|F\|)$
30		elfzuz3	$⊢ N \in (0 \dots \|F\|) \to \|F\| \in ℤ_{\geq N}$
31		fzss2	$⊢ \|F\| \in ℤ_{\geq N} \to (0 \dots N) \subseteq (0 \dots \|F\|)$
32	29 30 31	3syl	$⊢ φ \to (0 \dots N) \subseteq (0 \dots \|F\|)$
33	27 32	fssresd	$⊢ φ \to ({P ↾}_{(0 \dots N)}) : (0 \dots N) ⟶ Vtx (S)$
34	7	fveq2i	$⊢ \|H\| = \|F prefix N\|$
35		pfxlen	$⊢ (F \in Word dom I \land N \in (0 \dots \|F\|)) \to \|F prefix N\| = N$
36	14 29 35	syl2anc	$⊢ φ \to \|F prefix N\| = N$
37	34 36	syl5eq	$⊢ φ \to \|H\| = N$
38	37	oveq2d	$⊢ φ \to (0 \dots \|H\|) = (0 \dots N)$
39	38	feq2d	$⊢ φ \to (({P ↾}_{(0 \dots N)}) : (0 \dots \|H\|) ⟶ Vtx (S) \leftrightarrow ({P ↾}_{(0 \dots N)}) : (0 \dots N) ⟶ Vtx (S))$
40	33 39	mpbird	$⊢ φ \to ({P ↾}_{(0 \dots N)}) : (0 \dots \|H\|) ⟶ Vtx (S)$
41	8	feq1i	$⊢ Q : (0 \dots \|H\|) ⟶ Vtx (S) \leftrightarrow ({P ↾}_{(0 \dots N)}) : (0 \dots \|H\|) ⟶ Vtx (S)$
42	40 41	sylibr	$⊢ φ \to Q : (0 \dots \|H\|) ⟶ Vtx (S)$
43	1 2	wlkprop	$⊢ F Walks (G) P \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
44	3 43	syl	$⊢ φ \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
45	44	adantr	$⊢ (φ \land x \in (0 ..^\|H\|)) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
46	37	oveq2d	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N)$
47	46	eleq2d	$⊢ φ \to (x \in (0 ..^\|H\|) \leftrightarrow x \in (0 ..^N))$
48	8	fveq1i	$⊢ Q (x) = ({P ↾}_{(0 \dots N)}) (x)$
49		fzossfz	$⊢ (0 ..^N) \subseteq (0 \dots N)$
50	49	a1i	$⊢ φ \to (0 ..^N) \subseteq (0 \dots N)$
51	50	sselda	$⊢ (φ \land x \in (0 ..^N)) \to x \in (0 \dots N)$
52	51	fvresd	$⊢ (φ \land x \in (0 ..^N)) \to ({P ↾}_{(0 \dots N)}) (x) = P (x)$
53	48 52	syl5req	$⊢ (φ \land x \in (0 ..^N)) \to P (x) = Q (x)$
54	8	fveq1i	$⊢ Q (x + 1) = ({P ↾}_{(0 \dots N)}) (x + 1)$
55		fzofzp1	$⊢ x \in (0 ..^N) \to x + 1 \in (0 \dots N)$
56	55	adantl	$⊢ (φ \land x \in (0 ..^N)) \to x + 1 \in (0 \dots N)$
57	56	fvresd	$⊢ (φ \land x \in (0 ..^N)) \to ({P ↾}_{(0 \dots N)}) (x + 1) = P (x + 1)$
58	54 57	syl5req	$⊢ (φ \land x \in (0 ..^N)) \to P (x + 1) = Q (x + 1)$
59	53 58	jca	$⊢ (φ \land x \in (0 ..^N)) \to (P (x) = Q (x) \land P (x + 1) = Q (x + 1))$
60	59	ex	$⊢ φ \to (x \in (0 ..^N) \to (P (x) = Q (x) \land P (x + 1) = Q (x + 1)))$
61	47 60	sylbid	$⊢ φ \to (x \in (0 ..^\|H\|) \to (P (x) = Q (x) \land P (x + 1) = Q (x + 1)))$
62	61	imp	$⊢ (φ \land x \in (0 ..^\|H\|)) \to (P (x) = Q (x) \land P (x + 1) = Q (x + 1))$
63	14	ancli	$⊢ φ \to (φ \land F \in Word dom I)$
64	15	ffund	$⊢ F \in Word dom I \to Fun F$
65	64	adantl	$⊢ (φ \land F \in Word dom I) \to Fun F$
66	65	adantr	$⊢ ((φ \land F \in Word dom I) \land x \in (0 ..^N)) \to Fun F$
67		fdm	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to dom F = (0 ..^\|F\|)$
68		elfzouz2	$⊢ N \in (0 ..^\|F\|) \to \|F\| \in ℤ_{\geq N}$
69		fzoss2	$⊢ \|F\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|F\|)$
70	4 68 69	3syl	$⊢ φ \to (0 ..^N) \subseteq (0 ..^\|F\|)$
71		sseq2	$⊢ dom F = (0 ..^\|F\|) \to ((0 ..^N) \subseteq dom F \leftrightarrow (0 ..^N) \subseteq (0 ..^\|F\|))$
72	70 71	syl5ibr	$⊢ dom F = (0 ..^\|F\|) \to (φ \to (0 ..^N) \subseteq dom F)$
73	15 67 72	3syl	$⊢ F \in Word dom I \to (φ \to (0 ..^N) \subseteq dom F)$
74	73	impcom	$⊢ (φ \land F \in Word dom I) \to (0 ..^N) \subseteq dom F$
75	74	adantr	$⊢ ((φ \land F \in Word dom I) \land x \in (0 ..^N)) \to (0 ..^N) \subseteq dom F$
76		simpr	$⊢ ((φ \land F \in Word dom I) \land x \in (0 ..^N)) \to x \in (0 ..^N)$
77	66 75 76	resfvresima	$⊢ ((φ \land F \in Word dom I) \land x \in (0 ..^N)) \to ({I ↾}_{F [(0 ..^N)]}) (({F ↾}_{(0 ..^N)}) (x)) = I (F (x))$
78	63 77	sylan	$⊢ (φ \land x \in (0 ..^N)) \to ({I ↾}_{F [(0 ..^N)]}) (({F ↾}_{(0 ..^N)}) (x)) = I (F (x))$
79	78	eqcomd	$⊢ (φ \land x \in (0 ..^N)) \to I (F (x)) = ({I ↾}_{F [(0 ..^N)]}) (({F ↾}_{(0 ..^N)}) (x))$
80	79	ex	$⊢ φ \to (x \in (0 ..^N) \to I (F (x)) = ({I ↾}_{F [(0 ..^N)]}) (({F ↾}_{(0 ..^N)}) (x)))$
81	47 80	sylbid	$⊢ φ \to (x \in (0 ..^\|H\|) \to I (F (x)) = ({I ↾}_{F [(0 ..^N)]}) (({F ↾}_{(0 ..^N)}) (x)))$
82	81	imp	$⊢ (φ \land x \in (0 ..^\|H\|)) \to I (F (x)) = ({I ↾}_{F [(0 ..^N)]}) (({F ↾}_{(0 ..^N)}) (x))$
83	6	adantr	$⊢ (φ \land x \in (0 ..^\|H\|)) \to iEdg (S) = {I ↾}_{F [(0 ..^N)]}$
84	7	fveq1i	$⊢ H (x) = (F prefix N) (x)$
85	14	adantr	$⊢ (φ \land x \in (0 ..^\|H\|)) \to F \in Word dom I$
86	29	adantr	$⊢ (φ \land x \in (0 ..^\|H\|)) \to N \in (0 \dots \|F\|)$
87		pfxres	$⊢ (F \in Word dom I \land N \in (0 \dots \|F\|)) \to F prefix N = {F ↾}_{(0 ..^N)}$
88	85 86 87	syl2anc	$⊢ (φ \land x \in (0 ..^\|H\|)) \to F prefix N = {F ↾}_{(0 ..^N)}$
89	88	fveq1d	$⊢ (φ \land x \in (0 ..^\|H\|)) \to (F prefix N) (x) = ({F ↾}_{(0 ..^N)}) (x)$
90	84 89	syl5eq	$⊢ (φ \land x \in (0 ..^\|H\|)) \to H (x) = ({F ↾}_{(0 ..^N)}) (x)$
91	83 90	fveq12d	$⊢ (φ \land x \in (0 ..^\|H\|)) \to iEdg (S) (H (x)) = ({I ↾}_{F [(0 ..^N)]}) (({F ↾}_{(0 ..^N)}) (x))$
92	82 91	eqtr4d	$⊢ (φ \land x \in (0 ..^\|H\|)) \to I (F (x)) = iEdg (S) (H (x))$
93	62 92	jca	$⊢ (φ \land x \in (0 ..^\|H\|)) \to ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x)))$
94	4 68	syl	$⊢ φ \to \|F\| \in ℤ_{\geq N}$
95	37	fveq2d	$⊢ φ \to ℤ_{\geq \|H\|} = ℤ_{\geq N}$
96	94 95	eleqtrrd	$⊢ φ \to \|F\| \in ℤ_{\geq \|H\|}$
97		fzoss2	$⊢ \|F\| \in ℤ_{\geq \|H\|} \to (0 ..^\|H\|) \subseteq (0 ..^\|F\|)$
98	96 97	syl	$⊢ φ \to (0 ..^\|H\|) \subseteq (0 ..^\|F\|)$
99	98	sselda	$⊢ (φ \land x \in (0 ..^\|H\|)) \to x \in (0 ..^\|F\|)$
100		wkslem1	$⊢ k = x \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow if- (P (x) = P (x + 1), I (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq I (F (x))))$
101	100	rspcv	$⊢ x \in (0 ..^\|F\|) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to if- (P (x) = P (x + 1), I (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq I (F (x))))$
102	99 101	syl	$⊢ (φ \land x \in (0 ..^\|H\|)) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to if- (P (x) = P (x + 1), I (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq I (F (x))))$
103		eqeq12	$⊢ (P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \to (P (x) = P (x + 1) \leftrightarrow Q (x) = Q (x + 1))$
104	103	adantr	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to (P (x) = P (x + 1) \leftrightarrow Q (x) = Q (x + 1))$
105		simpr	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to I (F (x)) = iEdg (S) (H (x))$
106		sneq	$⊢ P (x) = Q (x) \to \{P (x)\} = \{Q (x)\}$
107	106	adantr	$⊢ (P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \to \{P (x)\} = \{Q (x)\}$
108	107	adantr	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to \{P (x)\} = \{Q (x)\}$
109	105 108	eqeq12d	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to (I (F (x)) = \{P (x)\} \leftrightarrow iEdg (S) (H (x)) = \{Q (x)\})$
110		preq12	$⊢ (P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \to \{P (x), P (x + 1)\} = \{Q (x), Q (x + 1)\}$
111	110	adantr	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to \{P (x), P (x + 1)\} = \{Q (x), Q (x + 1)\}$
112	111 105	sseq12d	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to (\{P (x), P (x + 1)\} \subseteq I (F (x)) \leftrightarrow \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x)))$
113	104 109 112	ifpbi123d	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to (if- (P (x) = P (x + 1), I (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq I (F (x))) \leftrightarrow if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x))))$
114	113	biimpd	$⊢ ((P (x) = Q (x) \land P (x + 1) = Q (x + 1)) \land I (F (x)) = iEdg (S) (H (x))) \to (if- (P (x) = P (x + 1), I (F (x)) = \{P (x)\}, \{P (x), P (x + 1)\} \subseteq I (F (x))) \to if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x))))$
115	93 102 114	sylsyld	$⊢ (φ \land x \in (0 ..^\|H\|)) \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x))))$
116	115	com12	$⊢ \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \to ((φ \land x \in (0 ..^\|H\|)) \to if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x))))$
117	116	3ad2ant3	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))) \to ((φ \land x \in (0 ..^\|H\|)) \to if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x))))$
118	45 117	mpcom	$⊢ (φ \land x \in (0 ..^\|H\|)) \to if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x)))$
119	118	ralrimiva	$⊢ φ \to \forall x \in (0 ..^\|H\|) if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x)))$
120	1 2 3 4 5	wlkreslem	$⊢ φ \to S \in V$
121		eqid	$⊢ Vtx (S) = Vtx (S)$
122		eqid	$⊢ iEdg (S) = iEdg (S)$
123	121 122	iswlkg	$⊢ S \in V \to (H Walks (S) Q \leftrightarrow (H \in Word dom iEdg (S) \land Q : (0 \dots \|H\|) ⟶ Vtx (S) \land \forall x \in (0 ..^\|H\|) if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x)))))$
124	120 123	syl	$⊢ φ \to (H Walks (S) Q \leftrightarrow (H \in Word dom iEdg (S) \land Q : (0 \dots \|H\|) ⟶ Vtx (S) \land \forall x \in (0 ..^\|H\|) if- (Q (x) = Q (x + 1), iEdg (S) (H (x)) = \{Q (x)\}, \{Q (x), Q (x + 1)\} \subseteq iEdg (S) (H (x)))))$
125	23 42 119 124	mpbir3and	$⊢ φ \to H Walks (S) Q$

Metamath Proof Explorer

Theorem wlkres

Proof