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∈NWWalksNG|lastS⁡w=w⁡0
Assertion clwwlkel ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩∈D

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d ⊢D=w∈NWWalksNG|lastS⁡w=w⁡0
2 ccatws1n0 ⊢P∈WordVtx⁡G→P++⟨“P⁡0”⟩≠∅
3 2 adantr ⊢P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩≠∅
4 3 3ad2ant2 ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩≠∅
5 simprl ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P∈WordVtx⁡G
6 fstwrdne0 ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P⁡0∈Vtx⁡G
7 6 s1cld ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→⟨“P⁡0”⟩∈WordVtx⁡G
8 ccatcl ⊢P∈WordVtx⁡G∧⟨“P⁡0”⟩∈WordVtx⁡G→P++⟨“P⁡0”⟩∈WordVtx⁡G
9 5 7 8 syl2anc ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩∈WordVtx⁡G
10 9 3adant3 ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩∈WordVtx⁡G
11 5 adantr ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→P∈WordVtx⁡G
12 7 adantr ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→⟨“P⁡0”⟩∈WordVtx⁡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∈WordVtx⁡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∈WordVtx⁡G∧P=N→i∈0..^P↔i∈0..^N
43 42 adantr ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→i∈0..^P↔i∈0..^N
44 39 43 mpbird ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→i∈0..^P
45 ccatval1 ⊢P∈WordVtx⁡G∧⟨“P⁡0”⟩∈WordVtx⁡G∧i∈0..^P→P++⟨“P⁡0”⟩⁡i=P⁡i
46 11 12 44 45 syl3anc ⊢N∈ℕ∧P∈WordVtx⁡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∈WordVtx⁡G∧P=N∧i∈0..^N−1→i+1∈0..^N
49 40 ad2antll ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→0..^P=0..^N
50 49 adantr ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→0..^P=0..^N
51 48 50 eleqtrrd ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→i+1∈0..^P
52 ccatval1 ⊢P∈WordVtx⁡G∧⟨“P⁡0”⟩∈WordVtx⁡G∧i+1∈0..^P→P++⟨“P⁡0”⟩⁡i+1=P⁡i+1
53 11 12 51 52 syl3anc ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→P++⟨“P⁡0”⟩⁡i+1=P⁡i+1
54 46 53 preq12d ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1=P⁡iP⁡i+1
55 54 eleq1d ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧i∈0..^N−1→P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔P⁡iP⁡i+1∈Edg⁡G
56 55 ralbidva ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G
57 56 biimprcd ⊢∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G→N∈ℕ∧P∈WordVtx⁡G∧P=N→∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
58 57 adantr ⊢∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→N∈ℕ∧P∈WordVtx⁡G∧P=N→∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
59 58 expdcom ⊢N∈ℕ→P∈WordVtx⁡G∧P=N→∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
60 59 3imp ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“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∈WordVtx⁡G∧P=N→N−1∈0..^P↔N−1∈0..^N
64 61 63 syl5ibrcom ⊢N∈ℕ→P∈WordVtx⁡G∧P=N→N−1∈0..^P
65 64 imp ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→N−1∈0..^P
66 ccatval1 ⊢P∈WordVtx⁡G∧⟨“P⁡0”⟩∈WordVtx⁡G∧N−1∈0..^P→P++⟨“P⁡0”⟩⁡N−1=P⁡N−1
67 5 7 65 66 syl3anc ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩⁡N−1=P⁡N−1
68 lsw ⊢P∈WordVtx⁡G→lastS⁡P=P⁡P−1
69 68 adantr ⊢P∈WordVtx⁡G∧P=N→lastS⁡P=P⁡P−1
70 fvoveq1 ⊢P=N→P⁡P−1=P⁡N−1
71 70 adantl ⊢P∈WordVtx⁡G∧P=N→P⁡P−1=P⁡N−1
72 69 71 eqtr2d ⊢P∈WordVtx⁡G∧P=N→P⁡N−1=lastS⁡P
73 72 adantl ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P⁡N−1=lastS⁡P
74 67 73 eqtr2d ⊢N∈ℕ∧P∈WordVtx⁡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∈WordVtx⁡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∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩⁡P=P++⟨“P⁡0”⟩⁡N
82 ccatws1ls ⊢P∈WordVtx⁡G∧P⁡0∈Vtx⁡G→P++⟨“P⁡0”⟩⁡P=P⁡0
83 5 6 82 syl2anc ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩⁡P=P⁡0
84 79 81 83 3eqtr2rd ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P⁡0=P++⟨“P⁡0”⟩⁡N-1+1
85 74 84 preq12d ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→lastS⁡PP⁡0=P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1
86 85 eleq1d ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→lastS⁡PP⁡0∈Edg⁡G↔P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1∈Edg⁡G
87 86 biimpcd ⊢lastS⁡PP⁡0∈Edg⁡G→N∈ℕ∧P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1∈Edg⁡G
88 87 adantl ⊢∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→N∈ℕ∧P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1∈Edg⁡G
89 88 expdcom ⊢N∈ℕ→P∈WordVtx⁡G∧P=N→∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1∈Edg⁡G
90 89 3imp ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩⁡N−1P++⟨“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”⟩⁡iP++⟨“P⁡0”⟩⁡i+1=P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1
95 94 eleq1d ⊢i=N−1→P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1∈Edg⁡G
96 91 95 ralsn ⊢∀i∈N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔P++⟨“P⁡0”⟩⁡N−1P++⟨“P⁡0”⟩⁡N-1+1∈Edg⁡G
97 90 96 sylibr ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→∀i∈N−1P++⟨“P⁡0”⟩⁡iP++⟨“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-1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^N−1∪N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
107 ralunb ⊢∀i∈0..^N−1∪N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G∧∀i∈N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
108 106 107 bitrdi ⊢N∈ℕ→∀i∈0..^N+1-1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G∧∀i∈N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
109 108 3ad2ant1 ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→∀i∈0..^N+1-1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G∧∀i∈N−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
110 60 97 109 mpbir2and ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→∀i∈0..^N+1-1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
111 ccatlen ⊢P∈WordVtx⁡G∧⟨“P⁡0”⟩∈WordVtx⁡G→P++⟨“P⁡0”⟩=P+⟨“P⁡0”⟩
112 5 7 111 syl2anc ⊢N∈ℕ∧P∈WordVtx⁡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∈WordVtx⁡G∧P=N→P+⟨“P⁡0”⟩=N+1
118 112 117 eqtrd ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩=N+1
119 118 3adant3 ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩=N+1
120 119 oveq1d ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩−1=N+1-1
121 120 oveq2d ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→0..^P++⟨“P⁡0”⟩−1=0..^N+1-1
122 121 raleqdv ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→∀i∈0..^P++⟨“P⁡0”⟩−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^N+1-1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
123 110 122 mpbird ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→∀i∈0..^P++⟨“P⁡0”⟩−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
124 4 10 123 3jca ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩≠∅∧P++⟨“P⁡0”⟩∈WordVtx⁡G∧∀i∈0..^P++⟨“P⁡0”⟩−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G
125 nnnn0 ⊢N∈ℕ→N∈ℕ0
126 iswwlksn ⊢N∈ℕ0→P++⟨“P⁡0”⟩∈NWWalksNG↔P++⟨“P⁡0”⟩∈WWalks⁡G∧P++⟨“P⁡0”⟩=N+1
127 125 126 syl ⊢N∈ℕ→P++⟨“P⁡0”⟩∈NWWalksNG↔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”⟩∈WordVtx⁡G∧∀i∈0..^P++⟨“P⁡0”⟩−1P++⟨“P⁡0”⟩⁡iP++⟨“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”⟩∈WordVtx⁡G∧∀i∈0..^P++⟨“P⁡0”⟩−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G∧P++⟨“P⁡0”⟩=N+1
132 127 131 bitrdi ⊢N∈ℕ→P++⟨“P⁡0”⟩∈NWWalksNG↔P++⟨“P⁡0”⟩≠∅∧P++⟨“P⁡0”⟩∈WordVtx⁡G∧∀i∈0..^P++⟨“P⁡0”⟩−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G∧P++⟨“P⁡0”⟩=N+1
133 132 3ad2ant1 ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩∈NWWalksNG↔P++⟨“P⁡0”⟩≠∅∧P++⟨“P⁡0”⟩∈WordVtx⁡G∧∀i∈0..^P++⟨“P⁡0”⟩−1P++⟨“P⁡0”⟩⁡iP++⟨“P⁡0”⟩⁡i+1∈Edg⁡G∧P++⟨“P⁡0”⟩=N+1
134 124 119 133 mpbir2and ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩∈NWWalksNG
135 lswccats1 ⊢P∈WordVtx⁡G∧P⁡0∈Vtx⁡G→lastS⁡P++⟨“P⁡0”⟩=P⁡0
136 5 6 135 syl2anc ⊢N∈ℕ∧P∈WordVtx⁡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∈WordVtx⁡G∧P=N→0∈0..^P↔0∈0..^N
141 138 140 syl5ibrcom ⊢N∈ℕ→P∈WordVtx⁡G∧P=N→0∈0..^P
142 141 imp ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→0∈0..^P
143 ccatval1 ⊢P∈WordVtx⁡G∧⟨“P⁡0”⟩∈WordVtx⁡G∧0∈0..^P→P++⟨“P⁡0”⟩⁡0=P⁡0
144 5 7 142 143 syl3anc ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→P++⟨“P⁡0”⟩⁡0=P⁡0
145 136 144 eqtr4d ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N→lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0
146 145 3adant3 ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡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”⟩∈NWWalksNG∧lastS⁡P++⟨“P⁡0”⟩=P++⟨“P⁡0”⟩⁡0
151 134 146 150 sylanbrc ⊢N∈ℕ∧P∈WordVtx⁡G∧P=N∧∀i∈0..^N−1P⁡iP⁡i+1∈Edg⁡G∧lastS⁡PP⁡0∈Edg⁡G→P++⟨“P⁡0”⟩∈D