Metamath Proof Explorer


Theorem clwwlkel

Description: Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018) (Revised by AV, 25-Apr-2021)

Ref Expression
Hypothesis clwwlkf1o.d D = w N WWalksN G | lastS w = w 0
Assertion clwwlkel N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ D

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d D = w N WWalksN G | lastS w = w 0
2 ccatws1n0 P Word Vtx G P ++ ⟨“ P 0 ”⟩
3 2 adantr P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩
4 3 3ad2ant2 N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩
5 simprl N P Word Vtx G P = N P Word Vtx G
6 fstwrdne0 N P Word Vtx G P = N P 0 Vtx G
7 6 s1cld N P Word Vtx G P = N ⟨“ P 0 ”⟩ Word Vtx G
8 ccatcl P Word Vtx G ⟨“ P 0 ”⟩ Word Vtx G P ++ ⟨“ P 0 ”⟩ Word Vtx G
9 5 7 8 syl2anc N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ Word Vtx G
10 9 3adant3 N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ Word Vtx G
11 5 adantr N P Word Vtx G P = N i 0 ..^ N 1 P Word Vtx G
12 7 adantr N P Word Vtx G P = N i 0 ..^ N 1 ⟨“ P 0 ”⟩ Word Vtx G
13 elfzonn0 i 0 ..^ N 1 i 0
14 13 adantl N i 0 ..^ N 1 i 0
15 nnz N N
16 15 adantr N i 0 ..^ N 1 N
17 elfzo0 i 0 ..^ N 1 i 0 N 1 i < N 1
18 nn0re i 0 i
19 18 adantr i 0 N i
20 nnre N N
21 peano2rem N N 1
22 20 21 syl N N 1
23 22 adantl i 0 N N 1
24 20 adantl i 0 N N
25 19 23 24 3jca i 0 N i N 1 N
26 25 adantr i 0 N i < N 1 i N 1 N
27 20 ltm1d N N 1 < N
28 27 adantl i 0 N N 1 < N
29 28 anim1ci i 0 N i < N 1 i < N 1 N 1 < N
30 lttr i N 1 N i < N 1 N 1 < N i < N
31 26 29 30 sylc i 0 N i < N 1 i < N
32 31 ex i 0 N i < N 1 i < N
33 32 impancom i 0 i < N 1 N i < N
34 33 3adant2 i 0 N 1 i < N 1 N i < N
35 17 34 sylbi i 0 ..^ N 1 N i < N
36 35 impcom N i 0 ..^ N 1 i < N
37 elfzo0z i 0 ..^ N i 0 N i < N
38 14 16 36 37 syl3anbrc N i 0 ..^ N 1 i 0 ..^ N
39 38 adantlr N P Word Vtx G P = N i 0 ..^ N 1 i 0 ..^ N
40 oveq2 P = N 0 ..^ P = 0 ..^ N
41 40 eleq2d P = N i 0 ..^ P i 0 ..^ N
42 41 ad2antll N P Word Vtx G P = N i 0 ..^ P i 0 ..^ N
43 42 adantr N P Word Vtx G P = N i 0 ..^ N 1 i 0 ..^ P i 0 ..^ N
44 39 43 mpbird N P Word Vtx G P = N i 0 ..^ N 1 i 0 ..^ P
45 ccatval1 P Word Vtx G ⟨“ P 0 ”⟩ Word Vtx G i 0 ..^ P P ++ ⟨“ P 0 ”⟩ i = P i
46 11 12 44 45 syl3anc N P Word Vtx G P = N i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i = P i
47 elfzom1p1elfzo N i 0 ..^ N 1 i + 1 0 ..^ N
48 47 adantlr N P Word Vtx G P = N i 0 ..^ N 1 i + 1 0 ..^ N
49 40 ad2antll N P Word Vtx G P = N 0 ..^ P = 0 ..^ N
50 49 adantr N P Word Vtx G P = N i 0 ..^ N 1 0 ..^ P = 0 ..^ N
51 48 50 eleqtrrd N P Word Vtx G P = N i 0 ..^ N 1 i + 1 0 ..^ P
52 ccatval1 P Word Vtx G ⟨“ P 0 ”⟩ Word Vtx G i + 1 0 ..^ P P ++ ⟨“ P 0 ”⟩ i + 1 = P i + 1
53 11 12 51 52 syl3anc N P Word Vtx G P = N i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i + 1 = P i + 1
54 46 53 preq12d N P Word Vtx G P = N i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 = P i P i + 1
55 54 eleq1d N P Word Vtx G P = N i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G P i P i + 1 Edg G
56 55 ralbidva N P Word Vtx G P = N i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i 0 ..^ N 1 P i P i + 1 Edg G
57 56 biimprcd i 0 ..^ N 1 P i P i + 1 Edg G N P Word Vtx G P = N i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
58 57 adantr i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G N P Word Vtx G P = N i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
59 58 expdcom N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
60 59 3imp N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
61 fzo0end N N 1 0 ..^ N
62 40 eleq2d P = N N 1 0 ..^ P N 1 0 ..^ N
63 62 adantl P Word Vtx G P = N N 1 0 ..^ P N 1 0 ..^ N
64 61 63 syl5ibrcom N P Word Vtx G P = N N 1 0 ..^ P
65 64 imp N P Word Vtx G P = N N 1 0 ..^ P
66 ccatval1 P Word Vtx G ⟨“ P 0 ”⟩ Word Vtx G N 1 0 ..^ P P ++ ⟨“ P 0 ”⟩ N 1 = P N 1
67 5 7 65 66 syl3anc N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ N 1 = P N 1
68 lsw P Word Vtx G lastS P = P P 1
69 68 adantr P Word Vtx G P = N lastS P = P P 1
70 fvoveq1 P = N P P 1 = P N 1
71 70 adantl P Word Vtx G P = N P P 1 = P N 1
72 69 71 eqtr2d P Word Vtx G P = N P N 1 = lastS P
73 72 adantl N P Word Vtx G P = N P N 1 = lastS P
74 67 73 eqtr2d N P Word Vtx G P = N lastS P = P ++ ⟨“ P 0 ”⟩ N 1
75 nncn N N
76 1cnd N 1
77 75 76 npcand N N - 1 + 1 = N
78 77 fveq2d N P ++ ⟨“ P 0 ”⟩ N - 1 + 1 = P ++ ⟨“ P 0 ”⟩ N
79 78 adantr N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ N - 1 + 1 = P ++ ⟨“ P 0 ”⟩ N
80 fveq2 P = N P ++ ⟨“ P 0 ”⟩ P = P ++ ⟨“ P 0 ”⟩ N
81 80 ad2antll N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ P = P ++ ⟨“ P 0 ”⟩ N
82 ccatws1ls P Word Vtx G P 0 Vtx G P ++ ⟨“ P 0 ”⟩ P = P 0
83 5 6 82 syl2anc N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ P = P 0
84 79 81 83 3eqtr2rd N P Word Vtx G P = N P 0 = P ++ ⟨“ P 0 ”⟩ N - 1 + 1
85 74 84 preq12d N P Word Vtx G P = N lastS P P 0 = P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1
86 85 eleq1d N P Word Vtx G P = N lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1 Edg G
87 86 biimpcd lastS P P 0 Edg G N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1 Edg G
88 87 adantl i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1 Edg G
89 88 expdcom N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1 Edg G
90 89 3imp N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1 Edg G
91 ovex N 1 V
92 fveq2 i = N 1 P ++ ⟨“ P 0 ”⟩ i = P ++ ⟨“ P 0 ”⟩ N 1
93 fvoveq1 i = N 1 P ++ ⟨“ P 0 ”⟩ i + 1 = P ++ ⟨“ P 0 ”⟩ N - 1 + 1
94 92 93 preq12d i = N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 = P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1
95 94 eleq1d i = N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1 Edg G
96 91 95 ralsn i N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G P ++ ⟨“ P 0 ”⟩ N 1 P ++ ⟨“ P 0 ”⟩ N - 1 + 1 Edg G
97 90 96 sylibr N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G i N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
98 75 76 76 addsubd N N + 1 - 1 = N - 1 + 1
99 98 oveq2d N 0 ..^ N + 1 - 1 = 0 ..^ N - 1 + 1
100 nnm1nn0 N N 1 0
101 elnn0uz N 1 0 N 1 0
102 100 101 sylib N N 1 0
103 fzosplitsn N 1 0 0 ..^ N - 1 + 1 = 0 ..^ N 1 N 1
104 102 103 syl N 0 ..^ N - 1 + 1 = 0 ..^ N 1 N 1
105 99 104 eqtrd N 0 ..^ N + 1 - 1 = 0 ..^ N 1 N 1
106 105 raleqdv N i 0 ..^ N + 1 - 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i 0 ..^ N 1 N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
107 ralunb i 0 ..^ N 1 N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
108 106 107 bitrdi N i 0 ..^ N + 1 - 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
109 108 3ad2ant1 N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G i 0 ..^ N + 1 - 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i 0 ..^ N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i N 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
110 60 97 109 mpbir2and N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G i 0 ..^ N + 1 - 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
111 ccatlen P Word Vtx G ⟨“ P 0 ”⟩ Word Vtx G P ++ ⟨“ P 0 ”⟩ = P + ⟨“ P 0 ”⟩
112 5 7 111 syl2anc N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ = P + ⟨“ P 0 ”⟩
113 id P = N P = N
114 s1len ⟨“ P 0 ”⟩ = 1
115 114 a1i P = N ⟨“ P 0 ”⟩ = 1
116 113 115 oveq12d P = N P + ⟨“ P 0 ”⟩ = N + 1
117 116 ad2antll N P Word Vtx G P = N P + ⟨“ P 0 ”⟩ = N + 1
118 112 117 eqtrd N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ = N + 1
119 118 3adant3 N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ = N + 1
120 119 oveq1d N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ 1 = N + 1 - 1
121 120 oveq2d N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 = 0 ..^ N + 1 - 1
122 121 raleqdv N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G i 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G i 0 ..^ N + 1 - 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
123 110 122 mpbird N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G i 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
124 4 10 123 3jca N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ P ++ ⟨“ P 0 ”⟩ Word Vtx G i 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
125 nnnn0 N N 0
126 iswwlksn N 0 P ++ ⟨“ P 0 ”⟩ N WWalksN G P ++ ⟨“ P 0 ”⟩ WWalks G P ++ ⟨“ P 0 ”⟩ = N + 1
127 125 126 syl N P ++ ⟨“ P 0 ”⟩ N WWalksN G P ++ ⟨“ P 0 ”⟩ WWalks G P ++ ⟨“ P 0 ”⟩ = N + 1
128 eqid Vtx G = Vtx G
129 eqid Edg G = Edg G
130 128 129 iswwlks P ++ ⟨“ P 0 ”⟩ WWalks G P ++ ⟨“ P 0 ”⟩ P ++ ⟨“ P 0 ”⟩ Word Vtx G i 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G
131 130 anbi1i P ++ ⟨“ P 0 ”⟩ WWalks G P ++ ⟨“ P 0 ”⟩ = N + 1 P ++ ⟨“ P 0 ”⟩ P ++ ⟨“ P 0 ”⟩ Word Vtx G i 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G P ++ ⟨“ P 0 ”⟩ = N + 1
132 127 131 bitrdi N P ++ ⟨“ P 0 ”⟩ N WWalksN G P ++ ⟨“ P 0 ”⟩ P ++ ⟨“ P 0 ”⟩ Word Vtx G i 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G P ++ ⟨“ P 0 ”⟩ = N + 1
133 132 3ad2ant1 N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ N WWalksN G P ++ ⟨“ P 0 ”⟩ P ++ ⟨“ P 0 ”⟩ Word Vtx G i 0 ..^ P ++ ⟨“ P 0 ”⟩ 1 P ++ ⟨“ P 0 ”⟩ i P ++ ⟨“ P 0 ”⟩ i + 1 Edg G P ++ ⟨“ P 0 ”⟩ = N + 1
134 124 119 133 mpbir2and N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ N WWalksN G
135 lswccats1 P Word Vtx G P 0 Vtx G lastS P ++ ⟨“ P 0 ”⟩ = P 0
136 5 6 135 syl2anc N P Word Vtx G P = N lastS P ++ ⟨“ P 0 ”⟩ = P 0
137 lbfzo0 0 0 ..^ N N
138 137 biimpri N 0 0 ..^ N
139 40 eleq2d P = N 0 0 ..^ P 0 0 ..^ N
140 139 adantl P Word Vtx G P = N 0 0 ..^ P 0 0 ..^ N
141 138 140 syl5ibrcom N P Word Vtx G P = N 0 0 ..^ P
142 141 imp N P Word Vtx G P = N 0 0 ..^ P
143 ccatval1 P Word Vtx G ⟨“ P 0 ”⟩ Word Vtx G 0 0 ..^ P P ++ ⟨“ P 0 ”⟩ 0 = P 0
144 5 7 142 143 syl3anc N P Word Vtx G P = N P ++ ⟨“ P 0 ”⟩ 0 = P 0
145 136 144 eqtr4d N P Word Vtx G P = N lastS P ++ ⟨“ P 0 ”⟩ = P ++ ⟨“ P 0 ”⟩ 0
146 145 3adant3 N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G lastS P ++ ⟨“ P 0 ”⟩ = P ++ ⟨“ P 0 ”⟩ 0
147 fveq2 w = P ++ ⟨“ P 0 ”⟩ lastS w = lastS P ++ ⟨“ P 0 ”⟩
148 fveq1 w = P ++ ⟨“ P 0 ”⟩ w 0 = P ++ ⟨“ P 0 ”⟩ 0
149 147 148 eqeq12d w = P ++ ⟨“ P 0 ”⟩ lastS w = w 0 lastS P ++ ⟨“ P 0 ”⟩ = P ++ ⟨“ P 0 ”⟩ 0
150 149 1 elrab2 P ++ ⟨“ P 0 ”⟩ D P ++ ⟨“ P 0 ”⟩ N WWalksN G lastS P ++ ⟨“ P 0 ”⟩ = P ++ ⟨“ P 0 ”⟩ 0
151 134 146 150 sylanbrc N P Word Vtx G P = N i 0 ..^ N 1 P i P i + 1 Edg G lastS P P 0 Edg G P ++ ⟨“ P 0 ”⟩ D