Metamath Proof Explorer


Theorem wwlksext2clwwlk

Description: If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-Apr-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypotheses clwwlkext2edg.v V = Vtx G
clwwlkext2edg.e E = Edg G
Assertion wwlksext2clwwlk W N WWalksN G Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwwlkext2edg.v V = Vtx G
2 clwwlkext2edg.e E = Edg G
3 wwlknbp1 W N WWalksN G N 0 W Word Vtx G W = N + 1
4 1 wrdeqi Word V = Word Vtx G
5 4 eleq2i W Word V W Word Vtx G
6 5 biimpri W Word Vtx G W Word V
7 6 3ad2ant2 N 0 W Word Vtx G W = N + 1 W Word V
8 7 ad2antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V W Word V
9 s1cl Z V ⟨“ Z ”⟩ Word V
10 9 adantl W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V ⟨“ Z ”⟩ Word V
11 ccatcl W Word V ⟨“ Z ”⟩ Word V W ++ ⟨“ Z ”⟩ Word V
12 8 10 11 syl2anc W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V W ++ ⟨“ Z ”⟩ Word V
13 12 adantr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ Word V
14 1 2 wwlknp W N WWalksN G W Word V W = N + 1 i 0 ..^ N W i W i + 1 E
15 simplll W Word V W = N + 1 Z V N 0 i 0 ..^ N W Word V
16 9 adantr Z V N 0 ⟨“ Z ”⟩ Word V
17 16 ad2antlr W Word V W = N + 1 Z V N 0 i 0 ..^ N ⟨“ Z ”⟩ Word V
18 elfzo0 i 0 ..^ N i 0 N i < N
19 simp1 i 0 N i < N i 0
20 peano2nn N N + 1
21 20 3ad2ant2 i 0 N i < N N + 1
22 nn0re i 0 i
23 22 3ad2ant1 i 0 N i < N i
24 nnre N N
25 24 3ad2ant2 i 0 N i < N N
26 peano2re N N + 1
27 24 26 syl N N + 1
28 27 3ad2ant2 i 0 N i < N N + 1
29 simp3 i 0 N i < N i < N
30 24 ltp1d N N < N + 1
31 30 3ad2ant2 i 0 N i < N N < N + 1
32 23 25 28 29 31 lttrd i 0 N i < N i < N + 1
33 elfzo0 i 0 ..^ N + 1 i 0 N + 1 i < N + 1
34 19 21 32 33 syl3anbrc i 0 N i < N i 0 ..^ N + 1
35 18 34 sylbi i 0 ..^ N i 0 ..^ N + 1
36 35 adantl W Word V W = N + 1 Z V N 0 i 0 ..^ N i 0 ..^ N + 1
37 oveq2 W = N + 1 0 ..^ W = 0 ..^ N + 1
38 37 adantl W Word V W = N + 1 0 ..^ W = 0 ..^ N + 1
39 38 eleq2d W Word V W = N + 1 i 0 ..^ W i 0 ..^ N + 1
40 39 ad2antrr W Word V W = N + 1 Z V N 0 i 0 ..^ N i 0 ..^ W i 0 ..^ N + 1
41 36 40 mpbird W Word V W = N + 1 Z V N 0 i 0 ..^ N i 0 ..^ W
42 ccatval1 W Word V ⟨“ Z ”⟩ Word V i 0 ..^ W W ++ ⟨“ Z ”⟩ i = W i
43 15 17 41 42 syl3anc W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i = W i
44 fzonn0p1p1 i 0 ..^ N i + 1 0 ..^ N + 1
45 44 adantl W Word V W = N + 1 Z V N 0 i 0 ..^ N i + 1 0 ..^ N + 1
46 37 eleq2d W = N + 1 i + 1 0 ..^ W i + 1 0 ..^ N + 1
47 46 ad3antlr W Word V W = N + 1 Z V N 0 i 0 ..^ N i + 1 0 ..^ W i + 1 0 ..^ N + 1
48 45 47 mpbird W Word V W = N + 1 Z V N 0 i 0 ..^ N i + 1 0 ..^ W
49 ccatval1 W Word V ⟨“ Z ”⟩ Word V i + 1 0 ..^ W W ++ ⟨“ Z ”⟩ i + 1 = W i + 1
50 15 17 48 49 syl3anc W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i + 1 = W i + 1
51 43 50 preq12d W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
52 51 ex W Word V W = N + 1 Z V N 0 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
53 52 expcom Z V N 0 W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
54 53 expcom N 0 Z V W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
55 54 3ad2ant1 N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
56 55 imp N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
57 56 expdcom W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
58 57 3imp1 W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W i W i + 1
59 58 eleq1d W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W i W i + 1 E
60 59 ralbidva W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i 0 ..^ N W i W i + 1 E
61 60 biimprd W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W i W i + 1 E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
62 61 3exp W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W i W i + 1 E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
63 62 com34 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
64 63 3imp1 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
65 64 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
66 simpll W Word V W = N + 1 Z V N 0 W Word V
67 9 ad2antrl W Word V W = N + 1 Z V N 0 ⟨“ Z ”⟩ Word V
68 nn0p1gt0 N 0 0 < N + 1
69 68 ad2antll W Word V W = N + 1 Z V N 0 0 < N + 1
70 breq2 W = N + 1 0 < W 0 < N + 1
71 70 ad2antlr W Word V W = N + 1 Z V N 0 0 < W 0 < N + 1
72 69 71 mpbird W Word V W = N + 1 Z V N 0 0 < W
73 hashneq0 W Word V 0 < W W
74 73 ad2antrr W Word V W = N + 1 Z V N 0 0 < W W
75 72 74 mpbid W Word V W = N + 1 Z V N 0 W
76 ccatval1lsw W Word V ⟨“ Z ”⟩ Word V W W ++ ⟨“ Z ”⟩ W 1 = lastS W
77 66 67 75 76 syl3anc W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W 1 = lastS W
78 oveq1 W = N + 1 W 1 = N + 1 - 1
79 78 ad2antlr W Word V W = N + 1 Z V N 0 W 1 = N + 1 - 1
80 nn0cn N 0 N
81 80 ad2antll W Word V W = N + 1 Z V N 0 N
82 pncan1 N N + 1 - 1 = N
83 81 82 syl W Word V W = N + 1 Z V N 0 N + 1 - 1 = N
84 79 83 eqtrd W Word V W = N + 1 Z V N 0 W 1 = N
85 84 fveq2d W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W 1 = W ++ ⟨“ Z ”⟩ N
86 77 85 eqtr3d W Word V W = N + 1 Z V N 0 lastS W = W ++ ⟨“ Z ”⟩ N
87 ccatws1ls W Word V Z V W ++ ⟨“ Z ”⟩ W = Z
88 87 ad2ant2r W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W = Z
89 fveq2 W = N + 1 W ++ ⟨“ Z ”⟩ W = W ++ ⟨“ Z ”⟩ N + 1
90 89 ad2antlr W Word V W = N + 1 Z V N 0 W ++ ⟨“ Z ”⟩ W = W ++ ⟨“ Z ”⟩ N + 1
91 88 90 eqtr3d W Word V W = N + 1 Z V N 0 Z = W ++ ⟨“ Z ”⟩ N + 1
92 86 91 preq12d W Word V W = N + 1 Z V N 0 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
93 92 expcom Z V N 0 W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
94 93 expcom N 0 Z V W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
95 94 3ad2ant1 N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
96 95 imp N 0 W Word Vtx G W = N + 1 Z V W Word V W = N + 1 lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
97 96 com12 W Word V W = N + 1 N 0 W Word Vtx G W = N + 1 Z V lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
98 97 3adant3 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
99 98 imp W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
100 99 eleq1d W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
101 100 biimpa W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
102 simprl1 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V N 0
103 102 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E N 0
104 fveq2 i = N W ++ ⟨“ Z ”⟩ i = W ++ ⟨“ Z ”⟩ N
105 fvoveq1 i = N W ++ ⟨“ Z ”⟩ i + 1 = W ++ ⟨“ Z ”⟩ N + 1
106 104 105 preq12d i = N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 = W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1
107 106 eleq1d i = N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
108 107 ralsng N 0 i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
109 103 108 syl W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E W ++ ⟨“ Z ”⟩ N W ++ ⟨“ Z ”⟩ N + 1 E
110 101 109 mpbird W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
111 ralunb i 0 ..^ N N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i 0 ..^ N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
112 65 110 111 sylanbrc W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ N N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
113 elnn0uz N 0 N 0
114 102 113 sylib W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V N 0
115 114 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E N 0
116 fzosplitsn N 0 0 ..^ N + 1 = 0 ..^ N N
117 115 116 syl W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E 0 ..^ N + 1 = 0 ..^ N N
118 117 raleqdv W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ N + 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i 0 ..^ N N W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
119 112 118 mpbird W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ N + 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
120 ccatws1len W Word V W ++ ⟨“ Z ”⟩ = W + 1
121 120 3ad2ant1 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E W ++ ⟨“ Z ”⟩ = W + 1
122 121 ad2antrr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ = W + 1
123 122 oveq1d W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ 1 = W + 1 - 1
124 oveq1 W = N + 1 W + 1 = N + 1 + 1
125 124 oveq1d W = N + 1 W + 1 - 1 = N + 1 + 1 - 1
126 1cnd N 0 1
127 80 126 addcld N 0 N + 1
128 127 126 pncand N 0 N + 1 + 1 - 1 = N + 1
129 128 3ad2ant1 N 0 W Word Vtx G W = N + 1 N + 1 + 1 - 1 = N + 1
130 129 adantr N 0 W Word Vtx G W = N + 1 Z V N + 1 + 1 - 1 = N + 1
131 125 130 sylan9eq W = N + 1 N 0 W Word Vtx G W = N + 1 Z V W + 1 - 1 = N + 1
132 131 3ad2antl2 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V W + 1 - 1 = N + 1
133 132 adantr W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W + 1 - 1 = N + 1
134 123 133 eqtrd W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E W ++ ⟨“ Z ”⟩ 1 = N + 1
135 134 oveq2d W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E 0 ..^ W ++ ⟨“ Z ”⟩ 1 = 0 ..^ N + 1
136 135 raleqdv W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E i 0 ..^ N + 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
137 119 136 mpbird W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
138 137 exp42 W Word V W = N + 1 i 0 ..^ N W i W i + 1 E N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
139 14 138 syl W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
140 139 imp41 W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
141 140 adantrr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E
142 lswccats1 W Word V Z V lastS W ++ ⟨“ Z ”⟩ = Z
143 8 142 sylancom W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ = Z
144 68 3ad2ant1 N 0 W Word Vtx G W = N + 1 0 < N + 1
145 70 3ad2ant3 N 0 W Word Vtx G W = N + 1 0 < W 0 < N + 1
146 144 145 mpbird N 0 W Word Vtx G W = N + 1 0 < W
147 146 ad2antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V 0 < W
148 ccatfv0 W Word V ⟨“ Z ”⟩ Word V 0 < W W ++ ⟨“ Z ”⟩ 0 = W 0
149 8 10 147 148 syl3anc W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V W ++ ⟨“ Z ”⟩ 0 = W 0
150 143 149 preq12d W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 = Z W 0
151 150 eleq1d W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E Z W 0 E
152 151 biimprcd Z W 0 E W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
153 152 adantl lastS W Z E Z W 0 E W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
154 153 impcom W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
155 13 141 154 3jca W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E
156 ccatws1len W Word Vtx G W ++ ⟨“ Z ”⟩ = W + 1
157 156 3ad2ant2 N 0 W Word Vtx G W = N + 1 W ++ ⟨“ Z ”⟩ = W + 1
158 124 3ad2ant3 N 0 W Word Vtx G W = N + 1 W + 1 = N + 1 + 1
159 80 126 126 addassd N 0 N + 1 + 1 = N + 1 + 1
160 1p1e2 1 + 1 = 2
161 160 oveq2i N + 1 + 1 = N + 2
162 159 161 eqtrdi N 0 N + 1 + 1 = N + 2
163 162 3ad2ant1 N 0 W Word Vtx G W = N + 1 N + 1 + 1 = N + 2
164 157 158 163 3eqtrd N 0 W Word Vtx G W = N + 1 W ++ ⟨“ Z ”⟩ = N + 2
165 164 ad3antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ = N + 2
166 2nn 2
167 nn0nnaddcl N 0 2 N + 2
168 166 167 mpan2 N 0 N + 2
169 168 3ad2ant1 N 0 W Word Vtx G W = N + 1 N + 2
170 1 2 isclwwlknx N + 2 W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E W ++ ⟨“ Z ”⟩ = N + 2
171 169 170 syl N 0 W Word Vtx G W = N + 1 W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E W ++ ⟨“ Z ”⟩ = N + 2
172 171 ad3antlr W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G W ++ ⟨“ Z ”⟩ Word V i 0 ..^ W ++ ⟨“ Z ”⟩ 1 W ++ ⟨“ Z ”⟩ i W ++ ⟨“ Z ”⟩ i + 1 E lastS W ++ ⟨“ Z ”⟩ W ++ ⟨“ Z ”⟩ 0 E W ++ ⟨“ Z ”⟩ = N + 2
173 155 165 172 mpbir2and W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G
174 173 exp31 W N WWalksN G N 0 W Word Vtx G W = N + 1 Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G
175 3 174 mpdan W N WWalksN G Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G
176 175 imp W N WWalksN G Z V lastS W Z E Z W 0 E W ++ ⟨“ Z ”⟩ N + 2 ClWWalksN G