Metamath Proof Explorer


Theorem 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 φ F Walks G P
wlkres.n φ N 0 ..^ F
wlkres.s φ Vtx S = V
wlkres.e φ iEdg S = I F 0 ..^ N
wlkres.h H = F prefix N
wlkres.q Q = P 0 N
Assertion wlkres φ H Walks S Q

Proof

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