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=VtxG
wwlksnext.e E=EdgG
Assertion wwlksnext TNWWalksNGSVlastSTSET++⟨“S”⟩N+1WWalksNG

Proof

Step Hyp Ref Expression
1 wwlksnext.v V=VtxG
2 wwlksnext.e E=EdgG
3 1 wwlknbp TNWWalksNGGVN0TWordV
4 1 2 wwlknp TNWWalksNGTWordVT=N+1i0..^NTiTi+1E
5 simp1 TWordVT=N+1i0..^NTiTi+1ETWordV
6 simprl N0SVlastSTSESV
7 cats1un TWordVSVT++⟨“S”⟩=TTS
8 5 6 7 syl2an TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩=TTS
9 opex TSV
10 9 snnz TS
11 10 neii ¬TS=
12 11 intnan ¬T=TS=
13 df-ne TTS¬TTS=
14 un00 T=TS=TTS=
15 13 14 xchbinxr TTS¬T=TS=
16 12 15 mpbir TTS
17 16 a1i TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSETTS
18 8 17 eqnetrd TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩
19 s1cl SV⟨“S”⟩WordV
20 19 ad2antrl N0SVlastSTSE⟨“S”⟩WordV
21 ccatcl TWordV⟨“S”⟩WordVT++⟨“S”⟩WordV
22 5 20 21 syl2an TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩WordV
23 simplrl N0SVTWordVT=N+1i0..^NTWordV
24 fzossfzop1 N00..^N0..^N+1
25 24 ad2antrr N0SVTWordVT=N+10..^N0..^N+1
26 25 sselda N0SVTWordVT=N+1i0..^Ni0..^N+1
27 oveq2 T=N+10..^T=0..^N+1
28 27 eleq2d T=N+1i0..^Ti0..^N+1
29 28 adantl TWordVT=N+1i0..^Ti0..^N+1
30 29 ad2antlr N0SVTWordVT=N+1i0..^Ni0..^Ti0..^N+1
31 26 30 mpbird N0SVTWordVT=N+1i0..^Ni0..^T
32 ccats1val1 TWordVi0..^TT++⟨“S”⟩i=Ti
33 23 31 32 syl2anc N0SVTWordVT=N+1i0..^NT++⟨“S”⟩i=Ti
34 fzonn0p1p1 i0..^Ni+10..^N+1
35 34 adantl N0SVTWordVT=N+1i0..^Ni+10..^N+1
36 27 adantl TWordVT=N+10..^T=0..^N+1
37 36 ad2antlr N0SVTWordVT=N+1i0..^N0..^T=0..^N+1
38 35 37 eleqtrrd N0SVTWordVT=N+1i0..^Ni+10..^T
39 ccats1val1 TWordVi+10..^TT++⟨“S”⟩i+1=Ti+1
40 23 38 39 syl2anc N0SVTWordVT=N+1i0..^NT++⟨“S”⟩i+1=Ti+1
41 33 40 preq12d N0SVTWordVT=N+1i0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1=TiTi+1
42 41 exp31 N0SVTWordVT=N+1i0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1=TiTi+1
43 42 adantrr N0SVlastSTSETWordVT=N+1i0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1=TiTi+1
44 43 impcom TWordVT=N+1N0SVlastSTSEi0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1=TiTi+1
45 44 imp TWordVT=N+1N0SVlastSTSEi0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1=TiTi+1
46 45 eleq1d TWordVT=N+1N0SVlastSTSEi0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1ETiTi+1E
47 46 ralbidva TWordVT=N+1N0SVlastSTSEi0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1Ei0..^NTiTi+1E
48 47 exbiri TWordVT=N+1N0SVlastSTSEi0..^NTiTi+1Ei0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1E
49 48 com23 TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1E
50 49 3impia TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1E
51 50 imp TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1E
52 oveq1 T=N+1T1=N+1-1
53 52 adantl TWordVT=N+1T1=N+1-1
54 nn0cn N0N
55 1cnd N01
56 54 55 pncand N0N+1-1=N
57 56 adantl SVN0N+1-1=N
58 53 57 sylan9eqr SVN0TWordVT=N+1T1=N
59 58 fveq2d SVN0TWordVT=N+1TT1=TN
60 lsw TWordVlastST=TT1
61 60 ad2antrl SVN0TWordVT=N+1lastST=TT1
62 simprl SVN0TWordVT=N+1TWordV
63 fzonn0p1 N0N0..^N+1
64 63 ad2antlr SVN0TWordVT=N+1N0..^N+1
65 27 eleq2d T=N+1N0..^TN0..^N+1
66 65 ad2antll SVN0TWordVT=N+1N0..^TN0..^N+1
67 64 66 mpbird SVN0TWordVT=N+1N0..^T
68 ccats1val1 TWordVN0..^TT++⟨“S”⟩N=TN
69 62 67 68 syl2anc SVN0TWordVT=N+1T++⟨“S”⟩N=TN
70 59 61 69 3eqtr4d SVN0TWordVT=N+1lastST=T++⟨“S”⟩N
71 simpll SVN0TWordVT=N+1SV
72 simprr SVN0TWordVT=N+1T=N+1
73 72 eqcomd SVN0TWordVT=N+1N+1=T
74 ccats1val2 TWordVSVN+1=TT++⟨“S”⟩N+1=S
75 74 eqcomd TWordVSVN+1=TS=T++⟨“S”⟩N+1
76 62 71 73 75 syl3anc SVN0TWordVT=N+1S=T++⟨“S”⟩N+1
77 70 76 preq12d SVN0TWordVT=N+1lastSTS=T++⟨“S”⟩NT++⟨“S”⟩N+1
78 77 eleq1d SVN0TWordVT=N+1lastSTSET++⟨“S”⟩NT++⟨“S”⟩N+1E
79 78 biimpcd lastSTSESVN0TWordVT=N+1T++⟨“S”⟩NT++⟨“S”⟩N+1E
80 79 exp4c lastSTSESVN0TWordVT=N+1T++⟨“S”⟩NT++⟨“S”⟩N+1E
81 80 impcom SVlastSTSEN0TWordVT=N+1T++⟨“S”⟩NT++⟨“S”⟩N+1E
82 81 impcom N0SVlastSTSETWordVT=N+1T++⟨“S”⟩NT++⟨“S”⟩N+1E
83 82 impcom TWordVT=N+1N0SVlastSTSET++⟨“S”⟩NT++⟨“S”⟩N+1E
84 83 3adantl3 TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩NT++⟨“S”⟩N+1E
85 fveq2 i=NT++⟨“S”⟩i=T++⟨“S”⟩N
86 fvoveq1 i=NT++⟨“S”⟩i+1=T++⟨“S”⟩N+1
87 85 86 preq12d i=NT++⟨“S”⟩iT++⟨“S”⟩i+1=T++⟨“S”⟩NT++⟨“S”⟩N+1
88 87 eleq1d i=NT++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩NT++⟨“S”⟩N+1E
89 88 ralsng N0iNT++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩NT++⟨“S”⟩N+1E
90 89 ad2antrl TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEiNT++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩NT++⟨“S”⟩N+1E
91 84 90 mpbird TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEiNT++⟨“S”⟩iT++⟨“S”⟩i+1E
92 ralunb i0..^NNT++⟨“S”⟩iT++⟨“S”⟩i+1Ei0..^NT++⟨“S”⟩iT++⟨“S”⟩i+1EiNT++⟨“S”⟩iT++⟨“S”⟩i+1E
93 51 91 92 sylanbrc TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^NNT++⟨“S”⟩iT++⟨“S”⟩i+1E
94 elnn0uz N0N0
95 eluzfz2 N0N0N
96 94 95 sylbi N0N0N
97 fzelp1 N0NN0N+1
98 fzosplit N0N+10..^N+1=0..^NN..^N+1
99 96 97 98 3syl N00..^N+1=0..^NN..^N+1
100 nn0z N0N
101 fzosn NN..^N+1=N
102 100 101 syl N0N..^N+1=N
103 102 uneq2d N00..^NN..^N+1=0..^NN
104 99 103 eqtrd N00..^N+1=0..^NN
105 104 ad2antrl TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSE0..^N+1=0..^NN
106 105 raleqdv TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^N+1T++⟨“S”⟩iT++⟨“S”⟩i+1Ei0..^NNT++⟨“S”⟩iT++⟨“S”⟩i+1E
107 93 106 mpbird TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^N+1T++⟨“S”⟩iT++⟨“S”⟩i+1E
108 ccatlen TWordV⟨“S”⟩WordVT++⟨“S”⟩=T+⟨“S”⟩
109 5 20 108 syl2an TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩=T+⟨“S”⟩
110 109 oveq1d TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩1=T+⟨“S”⟩-1
111 simpl2 TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET=N+1
112 s1len ⟨“S”⟩=1
113 112 a1i TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSE⟨“S”⟩=1
114 111 113 oveq12d TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET+⟨“S”⟩=N+1+1
115 114 oveq1d TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET+⟨“S”⟩-1=N+1+1-1
116 peano2nn0 N0N+10
117 116 nn0cnd N0N+1
118 117 55 pncand N0N+1+1-1=N+1
119 118 ad2antrl TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEN+1+1-1=N+1
120 110 115 119 3eqtrd TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩1=N+1
121 120 oveq2d TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSE0..^T++⟨“S”⟩1=0..^N+1
122 121 raleqdv TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1Ei0..^N+1T++⟨“S”⟩iT++⟨“S”⟩i+1E
123 107 122 mpbird TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSEi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1E
124 18 22 123 3jca TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1E
125 109 114 eqtrd TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩=N+1+1
126 124 125 jca TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
127 126 ex TWordVT=N+1i0..^NTiTi+1EN0SVlastSTSET++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
128 4 127 syl TNWWalksNGN0SVlastSTSET++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
129 128 expd TNWWalksNGN0SVlastSTSET++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
130 129 impcom N0TNWWalksNGSVlastSTSET++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
131 130 adantll GVN0TNWWalksNGSVlastSTSET++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
132 iswwlksn N+10T++⟨“S”⟩N+1WWalksNGT++⟨“S”⟩WWalksGT++⟨“S”⟩=N+1+1
133 116 132 syl N0T++⟨“S”⟩N+1WWalksNGT++⟨“S”⟩WWalksGT++⟨“S”⟩=N+1+1
134 133 adantl GVN0T++⟨“S”⟩N+1WWalksNGT++⟨“S”⟩WWalksGT++⟨“S”⟩=N+1+1
135 1 2 iswwlks T++⟨“S”⟩WWalksGT++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1E
136 135 anbi1i T++⟨“S”⟩WWalksGT++⟨“S”⟩=N+1+1T++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
137 134 136 bitrdi GVN0T++⟨“S”⟩N+1WWalksNGT++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
138 137 adantr GVN0TNWWalksNGT++⟨“S”⟩N+1WWalksNGT++⟨“S”⟩T++⟨“S”⟩WordVi0..^T++⟨“S”⟩1T++⟨“S”⟩iT++⟨“S”⟩i+1ET++⟨“S”⟩=N+1+1
139 131 138 sylibrd GVN0TNWWalksNGSVlastSTSET++⟨“S”⟩N+1WWalksNG
140 139 ex GVN0TNWWalksNGSVlastSTSET++⟨“S”⟩N+1WWalksNG
141 140 3adant3 GVN0TWordVTNWWalksNGSVlastSTSET++⟨“S”⟩N+1WWalksNG
142 3 141 mpcom TNWWalksNGSVlastSTSET++⟨“S”⟩N+1WWalksNG
143 142 3impib TNWWalksNGSVlastSTSET++⟨“S”⟩N+1WWalksNG