Metamath Proof Explorer


Theorem crctcshwlkn0

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >. . (Contributed by AV, 10-Mar-2021)

Ref Expression
Hypotheses crctcsh.v V = Vtx G
crctcsh.i I = iEdg G
crctcsh.d φ F Circuits G P
crctcsh.n N = F
crctcsh.s φ S 0 ..^ N
crctcsh.h H = F cyclShift S
crctcsh.q Q = x 0 N if x N S P x + S P x + S - N
Assertion crctcshwlkn0 φ S 0 H Walks G Q

Proof

Step Hyp Ref Expression
1 crctcsh.v V = Vtx G
2 crctcsh.i I = iEdg G
3 crctcsh.d φ F Circuits G P
4 crctcsh.n N = F
5 crctcsh.s φ S 0 ..^ N
6 crctcsh.h H = F cyclShift S
7 crctcsh.q Q = x 0 N if x N S P x + S P x + S - N
8 crctiswlk F Circuits G P F Walks G P
9 2 wlkf F Walks G P F Word dom I
10 cshwcl F Word dom I F cyclShift S Word dom I
11 3 8 9 10 4syl φ F cyclShift S Word dom I
12 6 11 eqeltrid φ H Word dom I
13 12 adantr φ S 0 H Word dom I
14 3 8 syl φ F Walks G P
15 1 wlkp F Walks G P P : 0 F V
16 simpll P : 0 F V φ x 0 N x N S P : 0 F V
17 elfznn0 x 0 N x 0
18 17 adantl S 0 ..^ N x 0 N x 0
19 elfzonn0 S 0 ..^ N S 0
20 19 adantr S 0 ..^ N x 0 N S 0
21 18 20 nn0addcld S 0 ..^ N x 0 N x + S 0
22 21 adantr S 0 ..^ N x 0 N x N S x + S 0
23 elfz3nn0 x 0 N N 0
24 4 23 eqeltrrid x 0 N F 0
25 24 ad2antlr S 0 ..^ N x 0 N x N S F 0
26 elfzelz x 0 N x
27 26 zred x 0 N x
28 27 adantl S 0 ..^ N x 0 N x
29 elfzoelz S 0 ..^ N S
30 29 zred S 0 ..^ N S
31 30 adantr S 0 ..^ N x 0 N S
32 elfzel2 x 0 N N
33 32 zred x 0 N N
34 33 adantl S 0 ..^ N x 0 N N
35 leaddsub x S N x + S N x N S
36 28 31 34 35 syl3anc S 0 ..^ N x 0 N x + S N x N S
37 36 biimpar S 0 ..^ N x 0 N x N S x + S N
38 37 4 breqtrdi S 0 ..^ N x 0 N x N S x + S F
39 22 25 38 3jca S 0 ..^ N x 0 N x N S x + S 0 F 0 x + S F
40 5 39 sylanl1 φ x 0 N x N S x + S 0 F 0 x + S F
41 elfz2nn0 x + S 0 F x + S 0 F 0 x + S F
42 40 41 sylibr φ x 0 N x N S x + S 0 F
43 42 adantll P : 0 F V φ x 0 N x N S x + S 0 F
44 16 43 ffvelcdmd P : 0 F V φ x 0 N x N S P x + S V
45 simpll P : 0 F V φ x 0 N ¬ x N S P : 0 F V
46 elfzoel2 S 0 ..^ N N
47 zaddcl x S x + S
48 47 adantrr x S N x + S
49 simprr x S N N
50 48 49 zsubcld x S N x + S - N
51 50 adantr x S N ¬ x N S x + S - N
52 zsubcl N S N S
53 52 ancoms S N N S
54 53 zred S N N S
55 zre x x
56 ltnle N S x N S < x ¬ x N S
57 54 55 56 syl2anr x S N N S < x ¬ x N S
58 zre N N
59 58 adantl S N N
60 zre S S
61 60 adantr S N S
62 55 adantr x S N x
63 ltsubadd N S x N S < x N < x + S
64 59 61 62 63 syl2an23an x S N N S < x N < x + S
65 59 adantl x S N N
66 48 zred x S N x + S
67 65 66 posdifd x S N N < x + S 0 < x + S - N
68 0red x S N 0
69 50 zred x S N x + S - N
70 ltle 0 x + S - N 0 < x + S - N 0 x + S - N
71 68 69 70 syl2anc x S N 0 < x + S - N 0 x + S - N
72 67 71 sylbid x S N N < x + S 0 x + S - N
73 64 72 sylbid x S N N S < x 0 x + S - N
74 57 73 sylbird x S N ¬ x N S 0 x + S - N
75 74 imp x S N ¬ x N S 0 x + S - N
76 51 75 jca x S N ¬ x N S x + S - N 0 x + S - N
77 76 exp31 x S N ¬ x N S x + S - N 0 x + S - N
78 77 26 syl11 S N x 0 N ¬ x N S x + S - N 0 x + S - N
79 29 46 78 syl2anc S 0 ..^ N x 0 N ¬ x N S x + S - N 0 x + S - N
80 79 imp31 S 0 ..^ N x 0 N ¬ x N S x + S - N 0 x + S - N
81 elnn0z x + S - N 0 x + S - N 0 x + S - N
82 80 81 sylibr S 0 ..^ N x 0 N ¬ x N S x + S - N 0
83 24 ad2antlr S 0 ..^ N x 0 N ¬ x N S F 0
84 elfzo0 S 0 ..^ N S 0 N S < N
85 elfz2nn0 x 0 N x 0 N 0 x N
86 nn0re S 0 S
87 86 3ad2ant1 S 0 N S < N S
88 nn0re x 0 x
89 88 3ad2ant1 x 0 N 0 x N x
90 87 89 anim12ci S 0 N S < N x 0 N 0 x N x S
91 nnre N N
92 91 91 jca N N N
93 92 3ad2ant2 S 0 N S < N N N
94 93 adantr S 0 N S < N x 0 N 0 x N N N
95 90 94 jca S 0 N S < N x 0 N 0 x N x S N N
96 simpr3 S 0 N S < N x 0 N 0 x N x N
97 ltle S N S < N S N
98 86 91 97 syl2an S 0 N S < N S N
99 98 3impia S 0 N S < N S N
100 99 adantr S 0 N S < N x 0 N 0 x N S N
101 95 96 100 jca32 S 0 N S < N x 0 N 0 x N x S N N x N S N
102 84 85 101 syl2anb S 0 ..^ N x 0 N x S N N x N S N
103 le2add x S N N x N S N x + S N + N
104 103 imp x S N N x N S N x + S N + N
105 102 104 syl S 0 ..^ N x 0 N x + S N + N
106 66 65 65 3jca x S N x + S N N
107 106 ex x S N x + S N N
108 107 26 syl11 S N x 0 N x + S N N
109 29 46 108 syl2anc S 0 ..^ N x 0 N x + S N N
110 109 imp S 0 ..^ N x 0 N x + S N N
111 lesubadd x + S N N x + S - N N x + S N + N
112 110 111 syl S 0 ..^ N x 0 N x + S - N N x + S N + N
113 105 112 mpbird S 0 ..^ N x 0 N x + S - N N
114 113 adantr S 0 ..^ N x 0 N ¬ x N S x + S - N N
115 114 4 breqtrdi S 0 ..^ N x 0 N ¬ x N S x + S - N F
116 82 83 115 3jca S 0 ..^ N x 0 N ¬ x N S x + S - N 0 F 0 x + S - N F
117 5 116 sylanl1 φ x 0 N ¬ x N S x + S - N 0 F 0 x + S - N F
118 elfz2nn0 x + S - N 0 F x + S - N 0 F 0 x + S - N F
119 117 118 sylibr φ x 0 N ¬ x N S x + S - N 0 F
120 119 adantll P : 0 F V φ x 0 N ¬ x N S x + S - N 0 F
121 45 120 ffvelcdmd P : 0 F V φ x 0 N ¬ x N S P x + S - N V
122 44 121 ifclda P : 0 F V φ x 0 N if x N S P x + S P x + S - N V
123 122 exp32 P : 0 F V φ x 0 N if x N S P x + S P x + S - N V
124 15 123 syl F Walks G P φ x 0 N if x N S P x + S P x + S - N V
125 14 124 mpcom φ x 0 N if x N S P x + S P x + S - N V
126 125 imp φ x 0 N if x N S P x + S P x + S - N V
127 126 7 fmptd φ Q : 0 N V
128 1 2 3 4 5 6 crctcshlem2 φ H = N
129 128 oveq2d φ 0 H = 0 N
130 129 feq2d φ Q : 0 H V Q : 0 N V
131 127 130 mpbird φ Q : 0 H V
132 131 adantr φ S 0 Q : 0 H V
133 1 2 wlkprop F Walks G P F Word dom I P : 0 F V i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i
134 3 8 133 3syl φ F Word dom I P : 0 F V i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i
135 134 adantr φ S 0 F Word dom I P : 0 F V i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i
136 4 eqcomi F = N
137 136 oveq2i 0 ..^ F = 0 ..^ N
138 137 raleqi i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i
139 fzo1fzo0n0 S 1 ..^ N S 0 ..^ N S 0
140 139 simplbi2 S 0 ..^ N S 0 S 1 ..^ N
141 5 140 syl φ S 0 S 1 ..^ N
142 141 imp φ S 0 S 1 ..^ N
143 142 ad2antlr F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i S 1 ..^ N
144 simplll F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i F Word dom I
145 wkslem1 i = k if- P i = P i + 1 I F i = P i P i P i + 1 I F i if- P k = P k + 1 I F k = P k P k P k + 1 I F k
146 145 cbvralvw i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
147 146 biimpi i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
148 147 adantl F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i k 0 ..^ N if- P k = P k + 1 I F k = P k P k P k + 1 I F k
149 crctprop F Circuits G P F Trails G P P 0 = P F
150 136 fveq2i P F = P N
151 150 eqeq2i P 0 = P F P 0 = P N
152 151 biimpi P 0 = P F P 0 = P N
153 152 eqcomd P 0 = P F P N = P 0
154 153 adantl F Trails G P P 0 = P F P N = P 0
155 3 149 154 3syl φ P N = P 0
156 155 ad2antrl F Word dom I P : 0 F V φ S 0 P N = P 0
157 156 adantr F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i P N = P 0
158 143 7 6 4 144 148 157 crctcshwlkn0lem7 F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i j 0 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
159 128 oveq2d φ 0 ..^ H = 0 ..^ N
160 159 raleqdv φ j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j j 0 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
161 160 ad2antrl F Word dom I P : 0 F V φ S 0 j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j j 0 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
162 161 adantr F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j j 0 ..^ N if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
163 158 162 mpbird F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
164 163 ex F Word dom I P : 0 F V φ S 0 i 0 ..^ N if- P i = P i + 1 I F i = P i P i P i + 1 I F i j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
165 138 164 biimtrid F Word dom I P : 0 F V φ S 0 i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
166 165 ex F Word dom I P : 0 F V φ S 0 i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
167 166 com23 F Word dom I P : 0 F V i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i φ S 0 j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
168 167 3impia F Word dom I P : 0 F V i 0 ..^ F if- P i = P i + 1 I F i = P i P i P i + 1 I F i φ S 0 j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
169 135 168 mpcom φ S 0 j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
170 13 132 169 3jca φ S 0 H Word dom I Q : 0 H V j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
171 1 2 3 4 5 6 7 crctcshlem3 φ G V H V Q V
172 171 adantr φ S 0 G V H V Q V
173 1 2 iswlk G V H V Q V H Walks G Q H Word dom I Q : 0 H V j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
174 172 173 syl φ S 0 H Walks G Q H Word dom I Q : 0 H V j 0 ..^ H if- Q j = Q j + 1 I H j = Q j Q j Q j + 1 I H j
175 170 174 mpbird φ S 0 H Walks G Q