Step | Hyp | Ref
| Expression |
1 | | fstwrdne 14256 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉) |
2 | 1 | s1cld 14306 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 〈“(𝑊‘0)”〉 ∈
Word 𝑉) |
3 | | ccatlen 14276 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉) → (♯‘(𝑊 ++ 〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
(♯‘〈“(𝑊‘0)”〉))) |
4 | 2, 3 | syldan 591 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 ++ 〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
(♯‘〈“(𝑊‘0)”〉))) |
5 | | s1len 14309 |
. . . . . . . . 9
⊢
(♯‘〈“(𝑊‘0)”〉) = 1 |
6 | 5 | oveq2i 7282 |
. . . . . . . 8
⊢
((♯‘𝑊) +
(♯‘〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
1) |
7 | 4, 6 | eqtrdi 2796 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘(𝑊 ++ 〈“(𝑊‘0)”〉)) =
((♯‘𝑊) +
1)) |
8 | 7 | oveq1d 7286 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘(𝑊 ++ 〈“(𝑊‘0)”〉)) −
1) = (((♯‘𝑊) +
1) − 1)) |
9 | | lencl 14234 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
10 | 9 | nn0cnd 12295 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℂ) |
11 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℂ) |
12 | | 1cnd 10971 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 1 ∈
ℂ) |
13 | 11, 12, 12 | addsubd 11353 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (((♯‘𝑊) + 1) − 1) =
(((♯‘𝑊) −
1) + 1)) |
14 | 8, 13 | eqtrd 2780 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘(𝑊 ++ 〈“(𝑊‘0)”〉)) −
1) = (((♯‘𝑊)
− 1) + 1)) |
15 | 14 | oveq2d 7287 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) →
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)) =
(0..^(((♯‘𝑊)
− 1) + 1))) |
16 | 15 | raleqdv 3347 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈
(0..^(((♯‘𝑊)
− 1) + 1)){((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
17 | | lennncl 14235 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
18 | | nnm1nn0 12274 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
ℕ0) |
20 | | elnn0uz 12622 |
. . . . . . 7
⊢
(((♯‘𝑊)
− 1) ∈ ℕ0 ↔ ((♯‘𝑊) − 1) ∈
(ℤ≥‘0)) |
21 | 19, 20 | sylib 217 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
(ℤ≥‘0)) |
22 | | fzosplitsn 13493 |
. . . . . 6
⊢
(((♯‘𝑊)
− 1) ∈ (ℤ≥‘0) →
(0..^(((♯‘𝑊)
− 1) + 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)})) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) →
(0..^(((♯‘𝑊)
− 1) + 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1)})) |
24 | 23 | raleqdv 3347 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈
(0..^(((♯‘𝑊)
− 1) + 1)){((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈
((0..^((♯‘𝑊)
− 1)) ∪ {((♯‘𝑊) − 1)}){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
25 | | ralunb 4130 |
. . . 4
⊢
(∀𝑖 ∈
((0..^((♯‘𝑊)
− 1)) ∪ {((♯‘𝑊) − 1)}){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
26 | 24, 25 | bitrdi 287 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈
(0..^(((♯‘𝑊)
− 1) + 1)){((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
27 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 𝑊 ∈ Word 𝑉) |
28 | 9 | nn0zd 12423 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ) |
29 | 28 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℤ) |
30 | | elfzom1elfzo 13453 |
. . . . . . . . 9
⊢
(((♯‘𝑊)
∈ ℤ ∧ 𝑖
∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈ (0..^(♯‘𝑊))) |
31 | 29, 30 | sylan 580 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → 𝑖 ∈
(0..^(♯‘𝑊))) |
32 | | ccats1val1 14330 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖) = (𝑊‘𝑖)) |
33 | 27, 31, 32 | syl2an2r 682 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖) = (𝑊‘𝑖)) |
34 | | elfzom1elp1fzo 13452 |
. . . . . . . . 9
⊢
(((♯‘𝑊)
∈ ℤ ∧ 𝑖
∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈ (0..^(♯‘𝑊))) |
35 | 29, 34 | sylan 580 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → (𝑖 + 1) ∈
(0..^(♯‘𝑊))) |
36 | | ccats1val1 14330 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
37 | 27, 35, 36 | syl2an2r 682 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
38 | 33, 37 | preq12d 4683 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → {((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}) |
39 | 38 | eleq1d 2825 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ 𝑖 ∈ (0..^((♯‘𝑊) − 1))) → ({((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
40 | 39 | ralbidva 3122 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
41 | | ovex 7304 |
. . . . . 6
⊢
((♯‘𝑊)
− 1) ∈ V |
42 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑖 = ((♯‘𝑊) − 1) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖) = ((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1))) |
43 | | fvoveq1 7294 |
. . . . . . . 8
⊢ (𝑖 = ((♯‘𝑊) − 1) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1)) = ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1))) |
44 | 42, 43 | preq12d 4683 |
. . . . . . 7
⊢ (𝑖 = ((♯‘𝑊) − 1) → {((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} = {((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1))}) |
45 | 44 | eleq1d 2825 |
. . . . . 6
⊢ (𝑖 = ((♯‘𝑊) − 1) → ({((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1))} ∈
(Edg‘𝐺))) |
46 | 41, 45 | ralsn 4623 |
. . . . 5
⊢
(∀𝑖 ∈
{((♯‘𝑊) −
1)} {((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1))} ∈
(Edg‘𝐺)) |
47 | | fzo0end 13477 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
(0..^(♯‘𝑊))) |
48 | 17, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((♯‘𝑊) − 1) ∈
(0..^(♯‘𝑊))) |
49 | | ccats1val1 14330 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 ++
〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1))) |
50 | 48, 49 | syldan 591 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)) = (𝑊‘((♯‘𝑊) − 1))) |
51 | | lsw 14265 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
52 | 51 | adantr 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
53 | 50, 52 | eqtr4d 2783 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)) = (lastS‘𝑊)) |
54 | | npcan1 11400 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℂ → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊)) |
55 | 10, 54 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (((♯‘𝑊) − 1) + 1) = (♯‘𝑊)) |
56 | 55 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (((♯‘𝑊) − 1) + 1) =
(♯‘𝑊)) |
57 | 56 | fveq2d 6775 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1)) = ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(♯‘𝑊))) |
58 | | eqidd 2741 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) = (♯‘𝑊)) |
59 | | ccats1val2 14332 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ (♯‘𝑊) = (♯‘𝑊)) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(♯‘𝑊)) = (𝑊‘0)) |
60 | 27, 1, 58, 59 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(♯‘𝑊)) = (𝑊‘0)) |
61 | 57, 60 | eqtrd 2780 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1)) = (𝑊‘0)) |
62 | 53, 61 | preq12d 4683 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → {((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1))} =
{(lastS‘𝑊), (𝑊‘0)}) |
63 | 62 | eleq1d 2825 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ({((𝑊 ++ 〈“(𝑊‘0)”〉)‘((♯‘𝑊) − 1)), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(((♯‘𝑊) − 1) + 1))} ∈
(Edg‘𝐺) ↔
{(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
64 | 46, 63 | syl5bb 283 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
65 | 40, 64 | anbi12d 631 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){((𝑊 ++
〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ ∀𝑖 ∈ {((♯‘𝑊) − 1)} {((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
66 | 16, 26, 65 | 3bitrd 305 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
67 | 27, 2 | jca 512 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉)) |
68 | | ccat0 14278 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉) → ((𝑊 ++ 〈“(𝑊‘0)”〉) = ∅ ↔
(𝑊 = ∅ ∧
〈“(𝑊‘0)”〉 =
∅))) |
69 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑊 = ∅ ∧
〈“(𝑊‘0)”〉 = ∅) →
𝑊 =
∅) |
70 | 68, 69 | syl6bi 252 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉) → ((𝑊 ++ 〈“(𝑊‘0)”〉) = ∅ →
𝑊 =
∅)) |
71 | 70 | necon3d 2966 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉) → (𝑊 ≠ ∅ → (𝑊 ++ 〈“(𝑊‘0)”〉) ≠
∅)) |
72 | 71 | adantld 491 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ++ 〈“(𝑊‘0)”〉) ≠
∅)) |
73 | 67, 72 | mpcom 38 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ++ 〈“(𝑊‘0)”〉) ≠
∅) |
74 | | wrdv 14230 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V) |
75 | | s1cli 14308 |
. . . . . . 7
⊢
〈“(𝑊‘0)”〉 ∈ Word
V |
76 | | ccatalpha 14296 |
. . . . . . 7
⊢ ((𝑊 ∈ Word V ∧
〈“(𝑊‘0)”〉 ∈ Word V) →
((𝑊 ++ 〈“(𝑊‘0)”〉) ∈
Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉))) |
77 | 74, 75, 76 | sylancl 586 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ 〈“(𝑊‘0)”〉) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉))) |
78 | 77 | adantr 481 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉) ∈ Word 𝑉 ↔ (𝑊 ∈ Word 𝑉 ∧ 〈“(𝑊‘0)”〉 ∈ Word 𝑉))) |
79 | 27, 2, 78 | mpbir2and 710 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ++ 〈“(𝑊‘0)”〉) ∈ Word 𝑉) |
80 | 73, 79 | jca 512 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉) ≠ ∅ ∧
(𝑊 ++ 〈“(𝑊‘0)”〉) ∈
Word 𝑉)) |
81 | | clwwlkwwlksb.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
82 | | eqid 2740 |
. . . . . 6
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
83 | 81, 82 | iswwlks 28197 |
. . . . 5
⊢ ((𝑊 ++ 〈“(𝑊‘0)”〉) ∈
(WWalks‘𝐺) ↔
((𝑊 ++ 〈“(𝑊‘0)”〉) ≠
∅ ∧ (𝑊 ++
〈“(𝑊‘0)”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
84 | | df-3an 1088 |
. . . . 5
⊢ (((𝑊 ++ 〈“(𝑊‘0)”〉) ≠
∅ ∧ (𝑊 ++
〈“(𝑊‘0)”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (((𝑊 ++ 〈“(𝑊‘0)”〉) ≠ ∅ ∧
(𝑊 ++ 〈“(𝑊‘0)”〉) ∈
Word 𝑉) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
85 | 83, 84 | bitri 274 |
. . . 4
⊢ ((𝑊 ++ 〈“(𝑊‘0)”〉) ∈
(WWalks‘𝐺) ↔
(((𝑊 ++ 〈“(𝑊‘0)”〉) ≠
∅ ∧ (𝑊 ++
〈“(𝑊‘0)”〉) ∈ Word 𝑉) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
86 | 85 | a1i 11 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉) ∈
(WWalks‘𝐺) ↔
(((𝑊 ++ 〈“(𝑊‘0)”〉) ≠
∅ ∧ (𝑊 ++
〈“(𝑊‘0)”〉) ∈ Word 𝑉) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
87 | 80, 86 | mpbirand 704 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“(𝑊‘0)”〉) ∈
(WWalks‘𝐺) ↔
∀𝑖 ∈
(0..^((♯‘(𝑊 ++
〈“(𝑊‘0)”〉)) − 1)){((𝑊 ++ 〈“(𝑊‘0)”〉)‘𝑖), ((𝑊 ++ 〈“(𝑊‘0)”〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
88 | 81, 82 | isclwwlk 28344 |
. . . 4
⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺))) |
89 | | 3anass 1094 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
90 | 88, 89 | bitri 274 |
. . 3
⊢ (𝑊 ∈ (ClWWalks‘𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) ∧ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
91 | 90 | baib 536 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ (Edg‘𝐺)))) |
92 | 66, 87, 91 | 3bitr4rd 312 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (𝑊 ++ 〈“(𝑊‘0)”〉) ∈
(WWalks‘𝐺))) |