Metamath Proof Explorer


Theorem eucrct2eupth

Description: Removing one edge ( I( FJ ) ) from a graph G with an Eulerian circuit <. F , P >. results in a graph S with an Eulerian path <. H , Q >. . (Contributed by AV, 17-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses eucrct2eupth1.v V = Vtx G
eucrct2eupth1.i I = iEdg G
eucrct2eupth1.d φ F EulerPaths G P
eucrct2eupth1.c φ F Circuits G P
eucrct2eupth1.s Vtx S = V
eucrct2eupth.n φ N = F
eucrct2eupth.j φ J 0 ..^ N
eucrct2eupth.e φ iEdg S = I F 0 ..^ N J
eucrct2eupth.k K = J + 1
eucrct2eupth.h H = F cyclShift K prefix N 1
eucrct2eupth.q Q = x 0 ..^ N if x N K P x + K P x + K - N
Assertion eucrct2eupth φ H EulerPaths S Q

Proof

Step Hyp Ref Expression
1 eucrct2eupth1.v V = Vtx G
2 eucrct2eupth1.i I = iEdg G
3 eucrct2eupth1.d φ F EulerPaths G P
4 eucrct2eupth1.c φ F Circuits G P
5 eucrct2eupth1.s Vtx S = V
6 eucrct2eupth.n φ N = F
7 eucrct2eupth.j φ J 0 ..^ N
8 eucrct2eupth.e φ iEdg S = I F 0 ..^ N J
9 eucrct2eupth.k K = J + 1
10 eucrct2eupth.h H = F cyclShift K prefix N 1
11 eucrct2eupth.q Q = x 0 ..^ N if x N K P x + K P x + K - N
12 3 adantl J = N 1 φ F EulerPaths G P
13 9 eqcomi J + 1 = K
14 13 oveq2i F cyclShift J + 1 = F cyclShift K
15 oveq1 J = N 1 J + 1 = N - 1 + 1
16 elfzo0 J 0 ..^ N J 0 N J < N
17 nncn N N
18 17 3ad2ant2 J 0 N J < N N
19 16 18 sylbi J 0 ..^ N N
20 npcan1 N N - 1 + 1 = N
21 7 19 20 3syl φ N - 1 + 1 = N
22 15 21 sylan9eq J = N 1 φ J + 1 = N
23 22 oveq2d J = N 1 φ F cyclShift J + 1 = F cyclShift N
24 6 oveq2d φ F cyclShift N = F cyclShift F
25 crctiswlk F Circuits G P F Walks G P
26 2 wlkf F Walks G P F Word dom I
27 25 26 syl F Circuits G P F Word dom I
28 4 27 syl φ F Word dom I
29 cshwn F Word dom I F cyclShift F = F
30 28 29 syl φ F cyclShift F = F
31 24 30 eqtrd φ F cyclShift N = F
32 31 adantl J = N 1 φ F cyclShift N = F
33 23 32 eqtrd J = N 1 φ F cyclShift J + 1 = F
34 14 33 eqtr3id J = N 1 φ F cyclShift K = F
35 eqid F = F
36 1 2 4 35 crctcshlem1 φ F 0
37 fz0sn0fz1 F 0 0 F = 0 1 F
38 36 37 syl φ 0 F = 0 1 F
39 38 eleq2d φ x 0 F x 0 1 F
40 elun x 0 1 F x 0 x 1 F
41 39 40 bitrdi φ x 0 F x 0 x 1 F
42 elsni x 0 x = 0
43 0le0 0 0
44 42 43 eqbrtrdi x 0 x 0
45 44 adantl φ x 0 x 0
46 45 iftrued φ x 0 if x 0 P x + N P x + N - N = P x + N
47 6 fveq2d φ P N = P F
48 crctprop F Circuits G P F Trails G P P 0 = P F
49 simpr F Trails G P P 0 = P F P 0 = P F
50 49 eqcomd F Trails G P P 0 = P F P F = P 0
51 4 48 50 3syl φ P F = P 0
52 47 51 eqtrd φ P N = P 0
53 52 adantr φ x = 0 P N = P 0
54 oveq1 x = 0 x + N = 0 + N
55 7 19 syl φ N
56 55 addid2d φ 0 + N = N
57 54 56 sylan9eqr φ x = 0 x + N = N
58 57 fveq2d φ x = 0 P x + N = P N
59 fveq2 x = 0 P x = P 0
60 59 adantl φ x = 0 P x = P 0
61 53 58 60 3eqtr4d φ x = 0 P x + N = P x
62 42 61 sylan2 φ x 0 P x + N = P x
63 46 62 eqtrd φ x 0 if x 0 P x + N P x + N - N = P x
64 63 ex φ x 0 if x 0 P x + N P x + N - N = P x
65 elfznn x 1 F x
66 nnnle0 x ¬ x 0
67 65 66 syl x 1 F ¬ x 0
68 67 adantl φ x 1 F ¬ x 0
69 68 iffalsed φ x 1 F if x 0 P x + N P x + N - N = P x + N - N
70 65 nncnd x 1 F x
71 70 adantl φ x 1 F x
72 55 adantr φ x 1 F N
73 71 72 pncand φ x 1 F x + N - N = x
74 73 fveq2d φ x 1 F P x + N - N = P x
75 69 74 eqtrd φ x 1 F if x 0 P x + N P x + N - N = P x
76 75 ex φ x 1 F if x 0 P x + N P x + N - N = P x
77 64 76 jaod φ x 0 x 1 F if x 0 P x + N P x + N - N = P x
78 41 77 sylbid φ x 0 F if x 0 P x + N P x + N - N = P x
79 78 imp φ x 0 F if x 0 P x + N P x + N - N = P x
80 79 mpteq2dva φ x 0 F if x 0 P x + N P x + N - N = x 0 F P x
81 80 adantl J = N 1 φ x 0 F if x 0 P x + N P x + N - N = x 0 F P x
82 9 oveq2i N K = N J + 1
83 15 oveq2d J = N 1 N J + 1 = N N - 1 + 1
84 21 oveq2d φ N N - 1 + 1 = N N
85 55 subidd φ N N = 0
86 84 85 eqtrd φ N N - 1 + 1 = 0
87 83 86 sylan9eq J = N 1 φ N J + 1 = 0
88 82 87 syl5eq J = N 1 φ N K = 0
89 88 breq2d J = N 1 φ x N K x 0
90 9 oveq2i x + K = x + J + 1
91 90 fveq2i P x + K = P x + J + 1
92 15 oveq2d J = N 1 x + J + 1 = x + N 1 + 1
93 21 oveq2d φ x + N 1 + 1 = x + N
94 92 93 sylan9eq J = N 1 φ x + J + 1 = x + N
95 94 fveq2d J = N 1 φ P x + J + 1 = P x + N
96 91 95 syl5eq J = N 1 φ P x + K = P x + N
97 90 oveq1i x + K - N = x + J + 1 - N
98 97 fveq2i P x + K - N = P x + J + 1 - N
99 92 oveq1d J = N 1 x + J + 1 - N = x + N - 1 + 1 - N
100 93 oveq1d φ x + N - 1 + 1 - N = x + N - N
101 99 100 sylan9eq J = N 1 φ x + J + 1 - N = x + N - N
102 101 fveq2d J = N 1 φ P x + J + 1 - N = P x + N - N
103 98 102 syl5eq J = N 1 φ P x + K - N = P x + N - N
104 89 96 103 ifbieq12d J = N 1 φ if x N K P x + K P x + K - N = if x 0 P x + N P x + N - N
105 104 mpteq2dv J = N 1 φ x 0 F if x N K P x + K P x + K - N = x 0 F if x 0 P x + N P x + N - N
106 4 25 syl φ F Walks G P
107 1 wlkp F Walks G P P : 0 F V
108 ffn P : 0 F V P Fn 0 F
109 106 107 108 3syl φ P Fn 0 F
110 109 adantl J = N 1 φ P Fn 0 F
111 dffn5 P Fn 0 F P = x 0 F P x
112 110 111 sylib J = N 1 φ P = x 0 F P x
113 81 105 112 3eqtr4d J = N 1 φ x 0 F if x N K P x + K P x + K - N = P
114 12 34 113 3brtr4d J = N 1 φ F cyclShift K EulerPaths G x 0 F if x N K P x + K P x + K - N
115 4 adantl J = N 1 φ F Circuits G P
116 115 34 113 3brtr4d J = N 1 φ F cyclShift K Circuits G x 0 F if x N K P x + K P x + K - N
117 elfzolt3 J 0 ..^ N 0 < N
118 7 117 syl φ 0 < N
119 elfzoelz J 0 ..^ N J
120 7 119 syl φ J
121 120 peano2zd φ J + 1
122 9 121 eqeltrid φ K
123 cshwlen F Word dom I K F cyclShift K = F
124 123 eqcomd F Word dom I K F = F cyclShift K
125 28 122 124 syl2anc φ F = F cyclShift K
126 6 125 eqtrd φ N = F cyclShift K
127 118 126 breqtrd φ 0 < F cyclShift K
128 127 adantl J = N 1 φ 0 < F cyclShift K
129 126 adantl J = N 1 φ N = F cyclShift K
130 129 oveq1d J = N 1 φ N 1 = F cyclShift K 1
131 8 adantl J = N 1 φ iEdg S = I F 0 ..^ N J
132 28 6 7 3jca φ F Word dom I N = F J 0 ..^ N
133 132 adantl J = N 1 φ F Word dom I N = F J 0 ..^ N
134 cshimadifsn0 F Word dom I N = F J 0 ..^ N F 0 ..^ N J = F cyclShift J + 1 0 ..^ N 1
135 133 134 syl J = N 1 φ F 0 ..^ N J = F cyclShift J + 1 0 ..^ N 1
136 14 imaeq1i F cyclShift J + 1 0 ..^ N 1 = F cyclShift K 0 ..^ N 1
137 135 136 eqtrdi J = N 1 φ F 0 ..^ N J = F cyclShift K 0 ..^ N 1
138 137 reseq2d J = N 1 φ I F 0 ..^ N J = I F cyclShift K 0 ..^ N 1
139 131 138 eqtrd J = N 1 φ iEdg S = I F cyclShift K 0 ..^ N 1
140 eqid F cyclShift K prefix N 1 = F cyclShift K prefix N 1
141 eqid x 0 F if x N K P x + K P x + K - N 0 N 1 = x 0 F if x N K P x + K P x + K - N 0 N 1
142 1 2 114 116 5 128 130 139 140 141 eucrct2eupth1 J = N 1 φ F cyclShift K prefix N 1 EulerPaths S x 0 F if x N K P x + K P x + K - N 0 N 1
143 10 a1i J = N 1 φ H = F cyclShift K prefix N 1
144 fzossfz 0 ..^ N 0 N
145 6 oveq2d φ 0 N = 0 F
146 144 145 sseqtrid φ 0 ..^ N 0 F
147 146 resmptd φ x 0 F if x N K P x + K P x + K - N 0 ..^ N = x 0 ..^ N if x N K P x + K P x + K - N
148 elfzoel2 J 0 ..^ N N
149 fzoval N 0 ..^ N = 0 N 1
150 7 148 149 3syl φ 0 ..^ N = 0 N 1
151 150 reseq2d φ x 0 F if x N K P x + K P x + K - N 0 ..^ N = x 0 F if x N K P x + K P x + K - N 0 N 1
152 147 151 eqtr3d φ x 0 ..^ N if x N K P x + K P x + K - N = x 0 F if x N K P x + K P x + K - N 0 N 1
153 11 152 syl5eq φ Q = x 0 F if x N K P x + K P x + K - N 0 N 1
154 153 adantl J = N 1 φ Q = x 0 F if x N K P x + K P x + K - N 0 N 1
155 142 143 154 3brtr4d J = N 1 φ H EulerPaths S Q
156 4 adantl ¬ J = N 1 φ F Circuits G P
157 peano2nn0 J 0 J + 1 0
158 157 3ad2ant1 J 0 N J < N J + 1 0
159 158 adantr J 0 N J < N ¬ J = N 1 J + 1 0
160 simpl2 J 0 N J < N ¬ J = N 1 N
161 1cnd J 0 N J < N 1
162 nn0cn J 0 J
163 162 3ad2ant1 J 0 N J < N J
164 18 161 163 subadd2d J 0 N J < N N 1 = J J + 1 = N
165 eqcom J = N 1 N 1 = J
166 eqcom N = J + 1 J + 1 = N
167 164 165 166 3bitr4g J 0 N J < N J = N 1 N = J + 1
168 167 necon3bbid J 0 N J < N ¬ J = N 1 N J + 1
169 157 nn0red J 0 J + 1
170 169 3ad2ant1 J 0 N J < N J + 1
171 nnre N N
172 171 3ad2ant2 J 0 N J < N N
173 nn0z J 0 J
174 nnz N N
175 zltp1le J N J < N J + 1 N
176 173 174 175 syl2an J 0 N J < N J + 1 N
177 176 biimp3a J 0 N J < N J + 1 N
178 170 172 177 leltned J 0 N J < N J + 1 < N N J + 1
179 178 biimprd J 0 N J < N N J + 1 J + 1 < N
180 168 179 sylbid J 0 N J < N ¬ J = N 1 J + 1 < N
181 180 imp J 0 N J < N ¬ J = N 1 J + 1 < N
182 159 160 181 3jca J 0 N J < N ¬ J = N 1 J + 1 0 N J + 1 < N
183 182 ex J 0 N J < N ¬ J = N 1 J + 1 0 N J + 1 < N
184 16 183 sylbi J 0 ..^ N ¬ J = N 1 J + 1 0 N J + 1 < N
185 elfzo0 J + 1 0 ..^ N J + 1 0 N J + 1 < N
186 184 185 syl6ibr J 0 ..^ N ¬ J = N 1 J + 1 0 ..^ N
187 7 186 syl φ ¬ J = N 1 J + 1 0 ..^ N
188 187 impcom ¬ J = N 1 φ J + 1 0 ..^ N
189 9 a1i ¬ J = N 1 φ K = J + 1
190 6 eqcomd φ F = N
191 190 oveq2d φ 0 ..^ F = 0 ..^ N
192 191 adantl ¬ J = N 1 φ 0 ..^ F = 0 ..^ N
193 188 189 192 3eltr4d ¬ J = N 1 φ K 0 ..^ F
194 eqid F cyclShift K = F cyclShift K
195 eqid x 0 F if x F K P x + K P x + K - F = x 0 F if x F K P x + K P x + K - F
196 3 adantl ¬ J = N 1 φ F EulerPaths G P
197 1 2 156 35 193 194 195 196 eucrctshift ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F
198 simprl ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F
199 simprr ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F
200 127 ad2antlr ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F 0 < F cyclShift K
201 126 oveq1d φ N 1 = F cyclShift K 1
202 201 ad2antlr ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F N 1 = F cyclShift K 1
203 8 adantl ¬ J = N 1 φ iEdg S = I F 0 ..^ N J
204 132 adantl ¬ J = N 1 φ F Word dom I N = F J 0 ..^ N
205 204 134 syl ¬ J = N 1 φ F 0 ..^ N J = F cyclShift J + 1 0 ..^ N 1
206 205 136 eqtrdi ¬ J = N 1 φ F 0 ..^ N J = F cyclShift K 0 ..^ N 1
207 206 reseq2d ¬ J = N 1 φ I F 0 ..^ N J = I F cyclShift K 0 ..^ N 1
208 203 207 eqtrd ¬ J = N 1 φ iEdg S = I F cyclShift K 0 ..^ N 1
209 208 adantr ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F iEdg S = I F cyclShift K 0 ..^ N 1
210 eqid x 0 F if x F K P x + K P x + K - F 0 N 1 = x 0 F if x F K P x + K P x + K - F 0 N 1
211 1 2 198 199 5 200 202 209 140 210 eucrct2eupth1 ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F F cyclShift K prefix N 1 EulerPaths S x 0 F if x F K P x + K P x + K - F 0 N 1
212 10 a1i ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F H = F cyclShift K prefix N 1
213 190 oveq1d φ F K = N K
214 213 breq2d φ x F K x N K
215 214 adantl ¬ J = N 1 φ x F K x N K
216 190 oveq2d φ x + K - F = x + K - N
217 216 fveq2d φ P x + K - F = P x + K - N
218 217 adantl ¬ J = N 1 φ P x + K - F = P x + K - N
219 215 218 ifbieq2d ¬ J = N 1 φ if x F K P x + K P x + K - F = if x N K P x + K P x + K - N
220 219 mpteq2dv ¬ J = N 1 φ x 0 F if x F K P x + K P x + K - F = x 0 F if x N K P x + K P x + K - N
221 150 eqcomd φ 0 N 1 = 0 ..^ N
222 221 adantl ¬ J = N 1 φ 0 N 1 = 0 ..^ N
223 220 222 reseq12d ¬ J = N 1 φ x 0 F if x F K P x + K P x + K - F 0 N 1 = x 0 F if x N K P x + K P x + K - N 0 ..^ N
224 6 adantl ¬ J = N 1 φ N = F
225 224 oveq2d ¬ J = N 1 φ 0 N = 0 F
226 144 225 sseqtrid ¬ J = N 1 φ 0 ..^ N 0 F
227 226 resmptd ¬ J = N 1 φ x 0 F if x N K P x + K P x + K - N 0 ..^ N = x 0 ..^ N if x N K P x + K P x + K - N
228 223 227 eqtrd ¬ J = N 1 φ x 0 F if x F K P x + K P x + K - F 0 N 1 = x 0 ..^ N if x N K P x + K P x + K - N
229 11 228 eqtr4id ¬ J = N 1 φ Q = x 0 F if x F K P x + K P x + K - F 0 N 1
230 229 adantr ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F Q = x 0 F if x F K P x + K P x + K - F 0 N 1
231 211 212 230 3brtr4d ¬ J = N 1 φ F cyclShift K EulerPaths G x 0 F if x F K P x + K P x + K - F F cyclShift K Circuits G x 0 F if x F K P x + K P x + K - F H EulerPaths S Q
232 197 231 mpdan ¬ J = N 1 φ H EulerPaths S Q
233 155 232 pm2.61ian φ H EulerPaths S Q