Metamath Proof Explorer

Theorem clwwlkwwlksb

Description: A nonempty word over vertices represents a closed walk iff the word concatenated with its first symbol represents a walk. (Contributed by AV, 4-Mar-2022)

Ref Expression
Hypothesis clwwlkwwlksb.v ⊢V=Vtx⁡G
Assertion clwwlkwwlksb ⊢W∈WordV∧W≠∅→W∈ClWWalks⁡G↔W++⟨“W⁡0”⟩∈WWalks⁡G

Proof

Step Hyp Ref Expression
1 clwwlkwwlksb.v ⊢V=Vtx⁡G
2 fstwrdne ⊢W∈WordV∧W≠∅→W⁡0∈V
3 2 s1cld ⊢W∈WordV∧W≠∅→⟨“W⁡0”⟩∈WordV
4 ccatlen ⊢W∈WordV∧⟨“W⁡0”⟩∈WordV→W++⟨“W⁡0”⟩=W+⟨“W⁡0”⟩
5 3 4 syldan ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩=W+⟨“W⁡0”⟩
6 s1len ⊢⟨“W⁡0”⟩=1
7 6 oveq2i ⊢W+⟨“W⁡0”⟩=W+1
8 5 7 eqtrdi ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩=W+1
9 8 oveq1d ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩−1=W+1-1
10 lencl ⊢W∈WordV→W∈ℕ0
11 10 nn0cnd ⊢W∈WordV→W∈ℂ
12 11 adantr ⊢W∈WordV∧W≠∅→W∈ℂ
13 1cnd ⊢W∈WordV∧W≠∅→1∈ℂ
14 12 13 13 addsubd ⊢W∈WordV∧W≠∅→W+1-1=W-1+1
15 9 14 eqtrd ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩−1=W-1+1
16 15 oveq2d ⊢W∈WordV∧W≠∅→0..^W++⟨“W⁡0”⟩−1=0..^W-1+1
17 16 raleqdv ⊢W∈WordV∧W≠∅→∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^W-1+1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
18 lennncl ⊢W∈WordV∧W≠∅→W∈ℕ
19 nnm1nn0 ⊢W∈ℕ→W−1∈ℕ0
20 18 19 syl ⊢W∈WordV∧W≠∅→W−1∈ℕ0
21 elnn0uz ⊢W−1∈ℕ0↔W−1∈ℤ≥0
22 20 21 sylib ⊢W∈WordV∧W≠∅→W−1∈ℤ≥0
23 fzosplitsn ⊢W−1∈ℤ≥0→0..^W-1+1=0..^W−1∪W−1
24 22 23 syl ⊢W∈WordV∧W≠∅→0..^W-1+1=0..^W−1∪W−1
25 24 raleqdv ⊢W∈WordV∧W≠∅→∀i∈0..^W-1+1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^W−1∪W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
26 ralunb ⊢∀i∈0..^W−1∪W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G∧∀i∈W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
27 25 26 bitrdi ⊢W∈WordV∧W≠∅→∀i∈0..^W-1+1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G∧∀i∈W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
28 simpl ⊢W∈WordV∧W≠∅→W∈WordV
29 10 nn0zd ⊢W∈WordV→W∈ℤ
30 29 adantr ⊢W∈WordV∧W≠∅→W∈ℤ
31 elfzom1elfzo ⊢W∈ℤ∧i∈0..^W−1→i∈0..^W
32 30 31 sylan ⊢W∈WordV∧W≠∅∧i∈0..^W−1→i∈0..^W
33 ccats1val1 ⊢W∈WordV∧i∈0..^W→W++⟨“W⁡0”⟩⁡i=W⁡i
34 28 32 33 syl2an2r ⊢W∈WordV∧W≠∅∧i∈0..^W−1→W++⟨“W⁡0”⟩⁡i=W⁡i
35 elfzom1elp1fzo ⊢W∈ℤ∧i∈0..^W−1→i+1∈0..^W
36 30 35 sylan ⊢W∈WordV∧W≠∅∧i∈0..^W−1→i+1∈0..^W
37 ccats1val1 ⊢W∈WordV∧i+1∈0..^W→W++⟨“W⁡0”⟩⁡i+1=W⁡i+1
38 28 36 37 syl2an2r ⊢W∈WordV∧W≠∅∧i∈0..^W−1→W++⟨“W⁡0”⟩⁡i+1=W⁡i+1
39 34 38 preq12d ⊢W∈WordV∧W≠∅∧i∈0..^W−1→W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1=W⁡iW⁡i+1
40 39 eleq1d ⊢W∈WordV∧W≠∅∧i∈0..^W−1→W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔W⁡iW⁡i+1∈Edg⁡G
41 40 ralbidva ⊢W∈WordV∧W≠∅→∀i∈0..^W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G
42 ovex ⊢W−1∈V
43 fveq2 ⊢i=W−1→W++⟨“W⁡0”⟩⁡i=W++⟨“W⁡0”⟩⁡W−1
44 fvoveq1 ⊢i=W−1→W++⟨“W⁡0”⟩⁡i+1=W++⟨“W⁡0”⟩⁡W-1+1
45 43 44 preq12d ⊢i=W−1→W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1=W++⟨“W⁡0”⟩⁡W−1W++⟨“W⁡0”⟩⁡W-1+1
46 45 eleq1d ⊢i=W−1→W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔W++⟨“W⁡0”⟩⁡W−1W++⟨“W⁡0”⟩⁡W-1+1∈Edg⁡G
47 42 46 ralsn ⊢∀i∈W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔W++⟨“W⁡0”⟩⁡W−1W++⟨“W⁡0”⟩⁡W-1+1∈Edg⁡G
48 fzo0end ⊢W∈ℕ→W−1∈0..^W
49 18 48 syl ⊢W∈WordV∧W≠∅→W−1∈0..^W
50 ccats1val1 ⊢W∈WordV∧W−1∈0..^W→W++⟨“W⁡0”⟩⁡W−1=W⁡W−1
51 49 50 syldan ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩⁡W−1=W⁡W−1
52 lsw ⊢W∈WordV→lastS⁡W=W⁡W−1
53 52 adantr ⊢W∈WordV∧W≠∅→lastS⁡W=W⁡W−1
54 51 53 eqtr4d ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩⁡W−1=lastS⁡W
55 npcan1 ⊢W∈ℂ→W-1+1=W
56 11 55 syl ⊢W∈WordV→W-1+1=W
57 56 adantr ⊢W∈WordV∧W≠∅→W-1+1=W
58 57 fveq2d ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩⁡W-1+1=W++⟨“W⁡0”⟩⁡W
59 eqidd ⊢W∈WordV∧W≠∅→W=W
60 ccats1val2 ⊢W∈WordV∧W⁡0∈V∧W=W→W++⟨“W⁡0”⟩⁡W=W⁡0
61 28 2 59 60 syl3anc ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩⁡W=W⁡0
62 58 61 eqtrd ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩⁡W-1+1=W⁡0
63 54 62 preq12d ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩⁡W−1W++⟨“W⁡0”⟩⁡W-1+1=lastS⁡WW⁡0
64 63 eleq1d ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩⁡W−1W++⟨“W⁡0”⟩⁡W-1+1∈Edg⁡G↔lastS⁡WW⁡0∈Edg⁡G
65 47 64 bitrid ⊢W∈WordV∧W≠∅→∀i∈W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔lastS⁡WW⁡0∈Edg⁡G
66 41 65 anbi12d ⊢W∈WordV∧W≠∅→∀i∈0..^W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G∧∀i∈W−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
67 17 27 66 3bitrd ⊢W∈WordV∧W≠∅→∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
68 28 3 jca ⊢W∈WordV∧W≠∅→W∈WordV∧⟨“W⁡0”⟩∈WordV
69 ccat0 ⊢W∈WordV∧⟨“W⁡0”⟩∈WordV→W++⟨“W⁡0”⟩=∅↔W=∅∧⟨“W⁡0”⟩=∅
70 simpl ⊢W=∅∧⟨“W⁡0”⟩=∅→W=∅
71 69 70 syl6bi ⊢W∈WordV∧⟨“W⁡0”⟩∈WordV→W++⟨“W⁡0”⟩=∅→W=∅
72 71 necon3d ⊢W∈WordV∧⟨“W⁡0”⟩∈WordV→W≠∅→W++⟨“W⁡0”⟩≠∅
73 72 adantld ⊢W∈WordV∧⟨“W⁡0”⟩∈WordV→W∈WordV∧W≠∅→W++⟨“W⁡0”⟩≠∅
74 68 73 mpcom ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩≠∅
75 wrdv ⊢W∈WordV→W∈WordV
76 s1cli ⊢⟨“W⁡0”⟩∈WordV
77 ccatalpha ⊢W∈WordV∧⟨“W⁡0”⟩∈WordV→W++⟨“W⁡0”⟩∈WordV↔W∈WordV∧⟨“W⁡0”⟩∈WordV
78 75 76 77 sylancl ⊢W∈WordV→W++⟨“W⁡0”⟩∈WordV↔W∈WordV∧⟨“W⁡0”⟩∈WordV
79 78 adantr ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩∈WordV↔W∈WordV∧⟨“W⁡0”⟩∈WordV
80 28 3 79 mpbir2and ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩∈WordV
81 74 80 jca ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩≠∅∧W++⟨“W⁡0”⟩∈WordV
82 eqid ⊢Edg⁡G=Edg⁡G
83 1 82 iswwlks ⊢W++⟨“W⁡0”⟩∈WWalks⁡G↔W++⟨“W⁡0”⟩≠∅∧W++⟨“W⁡0”⟩∈WordV∧∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
84 df-3an ⊢W++⟨“W⁡0”⟩≠∅∧W++⟨“W⁡0”⟩∈WordV∧∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G↔W++⟨“W⁡0”⟩≠∅∧W++⟨“W⁡0”⟩∈WordV∧∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
85 83 84 bitri ⊢W++⟨“W⁡0”⟩∈WWalks⁡G↔W++⟨“W⁡0”⟩≠∅∧W++⟨“W⁡0”⟩∈WordV∧∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
86 85 a1i ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩∈WWalks⁡G↔W++⟨“W⁡0”⟩≠∅∧W++⟨“W⁡0”⟩∈WordV∧∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
87 81 86 mpbirand ⊢W∈WordV∧W≠∅→W++⟨“W⁡0”⟩∈WWalks⁡G↔∀i∈0..^W++⟨“W⁡0”⟩−1W++⟨“W⁡0”⟩⁡iW++⟨“W⁡0”⟩⁡i+1∈Edg⁡G
88 1 82 isclwwlk ⊢W∈ClWWalks⁡G↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
89 3anass ⊢W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
90 88 89 bitri ⊢W∈ClWWalks⁡G↔W∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
91 90 baib ⊢W∈WordV∧W≠∅→W∈ClWWalks⁡G↔∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
92 67 87 91 3bitr4rd ⊢W∈WordV∧W≠∅→W∈ClWWalks⁡G↔W++⟨“W⁡0”⟩∈WWalks⁡G