Metamath Proof Explorer


Theorem wwlksnext

Description: Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021)

Ref Expression
Hypotheses wwlksnext.v V = Vtx G
wwlksnext.e E = Edg G
Assertion wwlksnext T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ N + 1 WWalksN G

Proof

Step Hyp Ref Expression
1 wwlksnext.v V = Vtx G
2 wwlksnext.e E = Edg G
3 1 wwlknbp T N WWalksN G G V N 0 T Word V
4 1 2 wwlknp T N WWalksN G T Word V T = N + 1 i 0 ..^ N T i T i + 1 E
5 simp1 T Word V T = N + 1 i 0 ..^ N T i T i + 1 E T Word V
6 simprl N 0 S V lastS T S E S V
7 cats1un T Word V S V T ++ ⟨“ S ”⟩ = T T S
8 5 6 7 syl2an T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ = T T S
9 opex T S V
10 9 snnz T S
11 10 neii ¬ T S =
12 11 intnan ¬ T = T S =
13 df-ne T T S ¬ T T S =
14 un00 T = T S = T T S =
15 13 14 xchbinxr T T S ¬ T = T S =
16 12 15 mpbir T T S
17 16 a1i T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T T S
18 8 17 eqnetrd T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩
19 s1cl S V ⟨“ S ”⟩ Word V
20 19 ad2antrl N 0 S V lastS T S E ⟨“ S ”⟩ Word V
21 ccatcl T Word V ⟨“ S ”⟩ Word V T ++ ⟨“ S ”⟩ Word V
22 5 20 21 syl2an T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ Word V
23 simplrl N 0 S V T Word V T = N + 1 i 0 ..^ N T Word V
24 fzossfzop1 N 0 0 ..^ N 0 ..^ N + 1
25 24 ad2antrr N 0 S V T Word V T = N + 1 0 ..^ N 0 ..^ N + 1
26 25 sselda N 0 S V T Word V T = N + 1 i 0 ..^ N i 0 ..^ N + 1
27 oveq2 T = N + 1 0 ..^ T = 0 ..^ N + 1
28 27 eleq2d T = N + 1 i 0 ..^ T i 0 ..^ N + 1
29 28 adantl T Word V T = N + 1 i 0 ..^ T i 0 ..^ N + 1
30 29 ad2antlr N 0 S V T Word V T = N + 1 i 0 ..^ N i 0 ..^ T i 0 ..^ N + 1
31 26 30 mpbird N 0 S V T Word V T = N + 1 i 0 ..^ N i 0 ..^ T
32 ccats1val1 T Word V i 0 ..^ T T ++ ⟨“ S ”⟩ i = T i
33 23 31 32 syl2anc N 0 S V T Word V T = N + 1 i 0 ..^ N T ++ ⟨“ S ”⟩ i = T i
34 fzonn0p1p1 i 0 ..^ N i + 1 0 ..^ N + 1
35 34 adantl N 0 S V T Word V T = N + 1 i 0 ..^ N i + 1 0 ..^ N + 1
36 27 adantl T Word V T = N + 1 0 ..^ T = 0 ..^ N + 1
37 36 ad2antlr N 0 S V T Word V T = N + 1 i 0 ..^ N 0 ..^ T = 0 ..^ N + 1
38 35 37 eleqtrrd N 0 S V T Word V T = N + 1 i 0 ..^ N i + 1 0 ..^ T
39 ccats1val1 T Word V i + 1 0 ..^ T T ++ ⟨“ S ”⟩ i + 1 = T i + 1
40 23 38 39 syl2anc N 0 S V T Word V T = N + 1 i 0 ..^ N T ++ ⟨“ S ”⟩ i + 1 = T i + 1
41 33 40 preq12d N 0 S V T Word V T = N + 1 i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 = T i T i + 1
42 41 exp31 N 0 S V T Word V T = N + 1 i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 = T i T i + 1
43 42 adantrr N 0 S V lastS T S E T Word V T = N + 1 i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 = T i T i + 1
44 43 impcom T Word V T = N + 1 N 0 S V lastS T S E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 = T i T i + 1
45 44 imp T Word V T = N + 1 N 0 S V lastS T S E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 = T i T i + 1
46 45 eleq1d T Word V T = N + 1 N 0 S V lastS T S E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T i T i + 1 E
47 46 ralbidva T Word V T = N + 1 N 0 S V lastS T S E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E i 0 ..^ N T i T i + 1 E
48 47 exbiri T Word V T = N + 1 N 0 S V lastS T S E i 0 ..^ N T i T i + 1 E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
49 48 com23 T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
50 49 3impia T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
51 50 imp T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
52 oveq1 T = N + 1 T 1 = N + 1 - 1
53 52 adantl T Word V T = N + 1 T 1 = N + 1 - 1
54 nn0cn N 0 N
55 1cnd N 0 1
56 54 55 pncand N 0 N + 1 - 1 = N
57 56 adantl S V N 0 N + 1 - 1 = N
58 53 57 sylan9eqr S V N 0 T Word V T = N + 1 T 1 = N
59 58 fveq2d S V N 0 T Word V T = N + 1 T T 1 = T N
60 lsw T Word V lastS T = T T 1
61 60 ad2antrl S V N 0 T Word V T = N + 1 lastS T = T T 1
62 simprl S V N 0 T Word V T = N + 1 T Word V
63 fzonn0p1 N 0 N 0 ..^ N + 1
64 63 ad2antlr S V N 0 T Word V T = N + 1 N 0 ..^ N + 1
65 27 eleq2d T = N + 1 N 0 ..^ T N 0 ..^ N + 1
66 65 ad2antll S V N 0 T Word V T = N + 1 N 0 ..^ T N 0 ..^ N + 1
67 64 66 mpbird S V N 0 T Word V T = N + 1 N 0 ..^ T
68 ccats1val1 T Word V N 0 ..^ T T ++ ⟨“ S ”⟩ N = T N
69 62 67 68 syl2anc S V N 0 T Word V T = N + 1 T ++ ⟨“ S ”⟩ N = T N
70 59 61 69 3eqtr4d S V N 0 T Word V T = N + 1 lastS T = T ++ ⟨“ S ”⟩ N
71 simpll S V N 0 T Word V T = N + 1 S V
72 simprr S V N 0 T Word V T = N + 1 T = N + 1
73 72 eqcomd S V N 0 T Word V T = N + 1 N + 1 = T
74 ccats1val2 T Word V S V N + 1 = T T ++ ⟨“ S ”⟩ N + 1 = S
75 74 eqcomd T Word V S V N + 1 = T S = T ++ ⟨“ S ”⟩ N + 1
76 62 71 73 75 syl3anc S V N 0 T Word V T = N + 1 S = T ++ ⟨“ S ”⟩ N + 1
77 70 76 preq12d S V N 0 T Word V T = N + 1 lastS T S = T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1
78 77 eleq1d S V N 0 T Word V T = N + 1 lastS T S E T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
79 78 biimpcd lastS T S E S V N 0 T Word V T = N + 1 T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
80 79 exp4c lastS T S E S V N 0 T Word V T = N + 1 T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
81 80 impcom S V lastS T S E N 0 T Word V T = N + 1 T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
82 81 impcom N 0 S V lastS T S E T Word V T = N + 1 T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
83 82 impcom T Word V T = N + 1 N 0 S V lastS T S E T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
84 83 3adantl3 T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
85 fveq2 i = N T ++ ⟨“ S ”⟩ i = T ++ ⟨“ S ”⟩ N
86 fvoveq1 i = N T ++ ⟨“ S ”⟩ i + 1 = T ++ ⟨“ S ”⟩ N + 1
87 85 86 preq12d i = N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 = T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1
88 87 eleq1d i = N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
89 88 ralsng N 0 i N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
90 89 ad2antrl T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ N T ++ ⟨“ S ”⟩ N + 1 E
91 84 90 mpbird T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
92 ralunb i 0 ..^ N N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E i 0 ..^ N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E i N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
93 51 91 92 sylanbrc T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ N N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
94 elnn0uz N 0 N 0
95 eluzfz2 N 0 N 0 N
96 94 95 sylbi N 0 N 0 N
97 fzelp1 N 0 N N 0 N + 1
98 fzosplit N 0 N + 1 0 ..^ N + 1 = 0 ..^ N N ..^ N + 1
99 96 97 98 3syl N 0 0 ..^ N + 1 = 0 ..^ N N ..^ N + 1
100 nn0z N 0 N
101 fzosn N N ..^ N + 1 = N
102 100 101 syl N 0 N ..^ N + 1 = N
103 102 uneq2d N 0 0 ..^ N N ..^ N + 1 = 0 ..^ N N
104 99 103 eqtrd N 0 0 ..^ N + 1 = 0 ..^ N N
105 104 ad2antrl T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E 0 ..^ N + 1 = 0 ..^ N N
106 105 raleqdv T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ N + 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E i 0 ..^ N N T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
107 93 106 mpbird T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ N + 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
108 ccatlen T Word V ⟨“ S ”⟩ Word V T ++ ⟨“ S ”⟩ = T + ⟨“ S ”⟩
109 5 20 108 syl2an T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ = T + ⟨“ S ”⟩
110 109 oveq1d T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ 1 = T + ⟨“ S ”⟩ - 1
111 simpl2 T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T = N + 1
112 s1len ⟨“ S ”⟩ = 1
113 112 a1i T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E ⟨“ S ”⟩ = 1
114 111 113 oveq12d T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T + ⟨“ S ”⟩ = N + 1 + 1
115 114 oveq1d T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T + ⟨“ S ”⟩ - 1 = N + 1 + 1 - 1
116 peano2nn0 N 0 N + 1 0
117 116 nn0cnd N 0 N + 1
118 117 55 pncand N 0 N + 1 + 1 - 1 = N + 1
119 118 ad2antrl T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E N + 1 + 1 - 1 = N + 1
120 110 115 119 3eqtrd T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ 1 = N + 1
121 120 oveq2d T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E 0 ..^ T ++ ⟨“ S ”⟩ 1 = 0 ..^ N + 1
122 121 raleqdv T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E i 0 ..^ N + 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
123 107 122 mpbird T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
124 18 22 123 3jca T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
125 109 114 eqtrd T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ = N + 1 + 1
126 124 125 jca T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
127 126 ex T Word V T = N + 1 i 0 ..^ N T i T i + 1 E N 0 S V lastS T S E T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
128 4 127 syl T N WWalksN G N 0 S V lastS T S E T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
129 128 expd T N WWalksN G N 0 S V lastS T S E T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
130 129 impcom N 0 T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
131 130 adantll G V N 0 T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
132 iswwlksn N + 1 0 T ++ ⟨“ S ”⟩ N + 1 WWalksN G T ++ ⟨“ S ”⟩ WWalks G T ++ ⟨“ S ”⟩ = N + 1 + 1
133 116 132 syl N 0 T ++ ⟨“ S ”⟩ N + 1 WWalksN G T ++ ⟨“ S ”⟩ WWalks G T ++ ⟨“ S ”⟩ = N + 1 + 1
134 133 adantl G V N 0 T ++ ⟨“ S ”⟩ N + 1 WWalksN G T ++ ⟨“ S ”⟩ WWalks G T ++ ⟨“ S ”⟩ = N + 1 + 1
135 1 2 iswwlks T ++ ⟨“ S ”⟩ WWalks G T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E
136 135 anbi1i T ++ ⟨“ S ”⟩ WWalks G T ++ ⟨“ S ”⟩ = N + 1 + 1 T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
137 134 136 bitrdi G V N 0 T ++ ⟨“ S ”⟩ N + 1 WWalksN G T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
138 137 adantr G V N 0 T N WWalksN G T ++ ⟨“ S ”⟩ N + 1 WWalksN G T ++ ⟨“ S ”⟩ T ++ ⟨“ S ”⟩ Word V i 0 ..^ T ++ ⟨“ S ”⟩ 1 T ++ ⟨“ S ”⟩ i T ++ ⟨“ S ”⟩ i + 1 E T ++ ⟨“ S ”⟩ = N + 1 + 1
139 131 138 sylibrd G V N 0 T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ N + 1 WWalksN G
140 139 ex G V N 0 T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ N + 1 WWalksN G
141 140 3adant3 G V N 0 T Word V T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ N + 1 WWalksN G
142 3 141 mpcom T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ N + 1 WWalksN G
143 142 3impib T N WWalksN G S V lastS T S E T ++ ⟨“ S ”⟩ N + 1 WWalksN G