MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  clwwlkwwlksb Structured version   Visualization version   GIF version

Theorem clwwlkwwlksb 27837
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.)
Hypothesis
Ref Expression
clwwlkwwlksb.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
clwwlkwwlksb ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺)))

Proof of Theorem clwwlkwwlksb
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 fstwrdne 13898 . . . . . . . . . 10 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉)
21s1cld 13948 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)
3 ccatlen 13918 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → (♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + (♯‘⟨“(𝑊‘0)”⟩)))
42, 3syldan 594 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + (♯‘⟨“(𝑊‘0)”⟩)))
5 s1len 13951 . . . . . . . . 9 (♯‘⟨“(𝑊‘0)”⟩) = 1
65oveq2i 7151 . . . . . . . 8 ((♯‘𝑊) + (♯‘⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + 1)
74, 6syl6eq 2873 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) = ((♯‘𝑊) + 1))
87oveq1d 7155 . . . . . 6 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1) = (((♯‘𝑊) + 1) − 1))
9 lencl 13876 . . . . . . . . 9 (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ0)
109nn0cnd 11945 . . . . . . . 8 (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ)
1110adantr 484 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℂ)
12 1cnd 10625 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → 1 ∈ ℂ)
1311, 12, 12addsubd 11007 . . . . . 6 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (((♯‘𝑊) + 1) − 1) = (((♯‘𝑊) − 1) + 1))
148, 13eqtrd 2857 . . . . 5 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1) = (((♯‘𝑊) − 1) + 1))
1514oveq2d 7156 . . . 4 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)) = (0..^(((♯‘𝑊) − 1) + 1)))
1615raleqdv 3392 . . 3 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(((♯‘𝑊) − 1) + 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
17 lennncl 13877 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)
18 nnm1nn0 11926 . . . . . . . 8 ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) − 1) ∈ ℕ0)
1917, 18syl 17 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈ ℕ0)
20 elnn0uz 12271 . . . . . . 7 (((♯‘𝑊) − 1) ∈ ℕ0 ↔ ((♯‘𝑊) − 1) ∈ (ℤ‘0))
2119, 20sylib 221 . . . . . 6 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈ (ℤ‘0))
22 fzosplitsn 13140 . . . . . 6 (((♯‘𝑊) − 1) ∈ (ℤ‘0) → (0..^(((♯‘𝑊) − 1) + 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}))
2321, 22syl 17 . . . . 5 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (0..^(((♯‘𝑊) − 1) + 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}))
2423raleqdv 3392 . . . 4 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^(((♯‘𝑊) − 1) + 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
25 ralunb 4142 . . . 4 (∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)}){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
2624, 25syl6bb 290 . . 3 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^(((♯‘𝑊) − 1) + 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
27 simpl 486 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → 𝑊 ∈ Word 𝑉)
289nn0zd 12073 . . . . . . . . . 10 (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ)
2928adantr 484 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℤ)
30 elfzom1elfzo 13100 . . . . . . . . 9 (((♯‘𝑊) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈ (0..^(♯‘𝑊)))
3129, 30sylan 583 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈ (0..^(♯‘𝑊)))
32 ccats1val1 13972 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖) = (𝑊𝑖))
3327, 31, 32syl2an2r 684 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖) = (𝑊𝑖))
34 elfzom1elp1fzo 13099 . . . . . . . . 9 (((♯‘𝑊) ∈ ℤ ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝑊)))
3529, 34sylan 583 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝑊)))
36 ccats1val1 13972 . . . . . . . 8 ((𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
3727, 35, 36syl2an2r 684 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
3833, 37preq12d 4651 . . . . . 6 (((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} = {(𝑊𝑖), (𝑊‘(𝑖 + 1))})
3938eleq1d 2898 . . . . 5 (((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ({((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
4039ralbidva 3186 . . . 4 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
41 ovex 7173 . . . . . 6 ((♯‘𝑊) − 1) ∈ V
42 fveq2 6652 . . . . . . . 8 (𝑖 = ((♯‘𝑊) − 1) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖) = ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)))
43 fvoveq1 7163 . . . . . . . 8 (𝑖 = ((♯‘𝑊) − 1) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1)))
4442, 43preq12d 4651 . . . . . . 7 (𝑖 = ((♯‘𝑊) − 1) → {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))})
4544eleq1d 2898 . . . . . 6 (𝑖 = ((♯‘𝑊) − 1) → ({((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ (Edg‘𝐺)))
4641, 45ralsn 4593 . . . . 5 (∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ (Edg‘𝐺))
47 fzo0end 13124 . . . . . . . . . 10 ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊)))
4817, 47syl 17 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊)))
49 ccats1val1 13972 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
5048, 49syldan 594 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
51 lsw 13907 . . . . . . . . 9 (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
5251adantr 484 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
5350, 52eqtr4d 2860 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
54 npcan1 11054 . . . . . . . . . . 11 ((♯‘𝑊) ∈ ℂ → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
5510, 54syl 17 . . . . . . . . . 10 (𝑊 ∈ Word 𝑉 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
5655adantr 484 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊))
5756fveq2d 6656 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1)) = ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(♯‘𝑊)))
58 eqidd 2823 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (♯‘𝑊) = (♯‘𝑊))
59 ccats1val2 13974 . . . . . . . . 9 ((𝑊 ∈ Word 𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(♯‘𝑊)) = (𝑊‘0))
6027, 1, 58, 59syl3anc 1368 . . . . . . . 8 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(♯‘𝑊)) = (𝑊‘0))
6157, 60eqtrd 2857 . . . . . . 7 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1)) = (𝑊‘0))
6253, 61preq12d 4651 . . . . . 6 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} = {(lastS‘𝑊), (𝑊‘0)})
6362eleq1d 2898 . . . . 5 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ({((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘((♯‘𝑊) − 1)), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(((♯‘𝑊) − 1) + 1))} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))
6446, 63syl5bb 286 . . . 4 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))
6540, 64anbi12d 633 . . 3 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
6616, 26, 653bitrd 308 . 2 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
6727, 2jca 515 . . . . 5 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉))
68 ccat0 13920 . . . . . . . 8 ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) = ∅ ↔ (𝑊 = ∅ ∧ ⟨“(𝑊‘0)”⟩ = ∅)))
69 simpl 486 . . . . . . . 8 ((𝑊 = ∅ ∧ ⟨“(𝑊‘0)”⟩ = ∅) → 𝑊 = ∅)
7068, 69syl6bi 256 . . . . . . 7 ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) = ∅ → 𝑊 = ∅))
7170necon3d 3032 . . . . . 6 ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → (𝑊 ≠ ∅ → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅))
7271adantld 494 . . . . 5 ((𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅))
7367, 72mpcom 38 . . . 4 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅)
74 wrdv 13872 . . . . . . 7 (𝑊 ∈ Word 𝑉𝑊 ∈ Word V)
75 s1cli 13950 . . . . . . 7 ⟨“(𝑊‘0)”⟩ ∈ Word V
76 ccatalpha 13938 . . . . . . 7 ((𝑊 ∈ Word V ∧ ⟨“(𝑊‘0)”⟩ ∈ Word V) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)))
7774, 75, 76sylancl 589 . . . . . 6 (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)))
7877adantr 484 . . . . 5 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ ⟨“(𝑊‘0)”⟩ ∈ Word 𝑉)))
7927, 2, 78mpbir2and 712 . . . 4 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉)
8073, 79jca 515 . . 3 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉))
81 clwwlkwwlksb.v . . . . . 6 𝑉 = (Vtx‘𝐺)
82 eqid 2822 . . . . . 6 (Edg‘𝐺) = (Edg‘𝐺)
8381, 82iswwlks 27620 . . . . 5 ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
84 df-3an 1086 . . . . 5 (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
8583, 84bitri 278 . . . 4 ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
8685a1i 11 . . 3 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ (((𝑊 ++ ⟨“(𝑊‘0)”⟩) ≠ ∅ ∧ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ Word 𝑉) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
8780, 86mpbirand 706 . 2 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → ((𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“(𝑊‘0)”⟩)) − 1)){((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘𝑖), ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
8881, 82isclwwlk 27767 . . . 4 (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))
89 3anass 1092 . . . 4 (((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
9088, 89bitri 278 . . 3 (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) ∧ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
9190baib 539 . 2 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))))
9266, 87, 913bitr4rd 315 1 ((𝑊 ∈ Word 𝑉𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (𝑊 ++ ⟨“(𝑊‘0)”⟩) ∈ (WWalks‘𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  wne 3011  wral 3130  Vcvv 3469  cun 3906  c0 4265  {csn 4539  {cpr 4541  cfv 6334  (class class class)co 7140  cc 10524  0cc0 10526  1c1 10527   + caddc 10529  cmin 10859  cn 11625  0cn0 11885  cz 11969  cuz 12231  ..^cfzo 13028  chash 13686  Word cword 13857  lastSclsw 13905   ++ cconcat 13913  ⟨“cs1 13940  Vtxcvtx 26787  Edgcedg 26838  WWalkscwwlks 27609  ClWWalkscclwwlk 27764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-dju 9318  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-2 11688  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-hash 13687  df-word 13858  df-lsw 13906  df-concat 13914  df-s1 13941  df-wwlks 27614  df-clwwlk 27765
This theorem is referenced by:  clwwlknwwlksnb  27838
  Copyright terms: Public domain W3C validator