| Step | Hyp | Ref
| Expression |
| 1 | | wwlksnext.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | 1 | wwlknbp 29862 |
. . 3
⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉)) |
| 3 | | wwlksnext.e |
. . . . . . . . . . 11
⊢ 𝐸 = (Edg‘𝐺) |
| 4 | 1, 3 | wwlknp 29863 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸)) |
| 5 | | simp1 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → 𝑇 ∈ Word 𝑉) |
| 6 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → 𝑆 ∈ 𝑉) |
| 7 | | cats1un 14759 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑇 ++ 〈“𝑆”〉) = (𝑇 ∪ {〈(♯‘𝑇), 𝑆〉})) |
| 8 | 5, 6, 7 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ 〈“𝑆”〉) = (𝑇 ∪ {〈(♯‘𝑇), 𝑆〉})) |
| 9 | | opex 5469 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈(♯‘𝑇), 𝑆〉 ∈ V |
| 10 | 9 | snnz 4776 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈(♯‘𝑇), 𝑆〉} ≠ ∅ |
| 11 | 10 | neii 2942 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
{〈(♯‘𝑇),
𝑆〉} =
∅ |
| 12 | 11 | intnan 486 |
. . . . . . . . . . . . . . . 16
⊢ ¬
(𝑇 = ∅ ∧
{〈(♯‘𝑇),
𝑆〉} =
∅) |
| 13 | | df-ne 2941 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∪
{〈(♯‘𝑇),
𝑆〉}) ≠ ∅
↔ ¬ (𝑇 ∪
{〈(♯‘𝑇),
𝑆〉}) =
∅) |
| 14 | | un00 4445 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 = ∅ ∧
{〈(♯‘𝑇),
𝑆〉} = ∅) ↔
(𝑇 ∪
{〈(♯‘𝑇),
𝑆〉}) =
∅) |
| 15 | 13, 14 | xchbinxr 335 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∪
{〈(♯‘𝑇),
𝑆〉}) ≠ ∅
↔ ¬ (𝑇 = ∅
∧ {〈(♯‘𝑇), 𝑆〉} = ∅)) |
| 16 | 12, 15 | mpbir 231 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∪
{〈(♯‘𝑇),
𝑆〉}) ≠
∅ |
| 17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ∪ {〈(♯‘𝑇), 𝑆〉}) ≠ ∅) |
| 18 | 8, 17 | eqnetrd 3008 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ 〈“𝑆”〉) ≠
∅) |
| 19 | | s1cl 14640 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ 𝑉 → 〈“𝑆”〉 ∈ Word 𝑉) |
| 20 | 19 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → 〈“𝑆”〉 ∈ Word 𝑉) |
| 21 | | ccatcl 14612 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ Word 𝑉 ∧ 〈“𝑆”〉 ∈ Word 𝑉) → (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉) |
| 22 | 5, 20, 21 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉) |
| 23 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑇 ∈ Word 𝑉) |
| 24 | | fzossfzop1 13782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
| 25 | 24 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
| 26 | 25 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) |
| 27 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((♯‘𝑇) =
(𝑁 + 1) →
(0..^(♯‘𝑇)) =
(0..^(𝑁 +
1))) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝑇) =
(𝑁 + 1) → (𝑖 ∈
(0..^(♯‘𝑇))
↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
| 30 | 29 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) |
| 31 | 26, 30 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(♯‘𝑇))) |
| 32 | | ccats1val1 14664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ 〈“𝑆”〉)‘𝑖) = (𝑇‘𝑖)) |
| 33 | 23, 31, 32 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ 〈“𝑆”〉)‘𝑖) = (𝑇‘𝑖)) |
| 34 | | fzonn0p1p1 13783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
| 36 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1))) |
| 37 | 36 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1))) |
| 38 | 35, 37 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(♯‘𝑇))) |
| 39 | | ccats1val1 14664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1))) |
| 40 | 23, 38, 39 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1))) |
| 41 | 33, 40 | preq12d 4741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))}) |
| 42 | 41 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℕ0
∧ 𝑆 ∈ 𝑉) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))}))) |
| 43 | 42 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))}))) |
| 44 | 43 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})) |
| 45 | 44 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))}) |
| 46 | 45 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸)) |
| 47 | 46 | ralbidva 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸)) |
| 48 | 47 | exbiri 811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
| 49 | 48 | com23 86 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸 → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸))) |
| 50 | 49 | 3impia 1118 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
| 51 | 50 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) |
| 52 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝑇) =
(𝑁 + 1) →
((♯‘𝑇) −
1) = ((𝑁 + 1) −
1)) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → ((♯‘𝑇) − 1) = ((𝑁 + 1) −
1)) |
| 54 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 55 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
| 56 | 54, 55 | pncand 11621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
| 57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) − 1) = 𝑁) |
| 58 | 53, 57 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ((♯‘𝑇) − 1) = 𝑁) |
| 59 | 58 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑇‘((♯‘𝑇) − 1)) = (𝑇‘𝑁)) |
| 60 | | lsw 14602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑇 ∈ Word 𝑉 → (lastS‘𝑇) = (𝑇‘((♯‘𝑇) − 1))) |
| 61 | 60 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (lastS‘𝑇) = (𝑇‘((♯‘𝑇) − 1))) |
| 62 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑇 ∈ Word 𝑉) |
| 63 | | fzonn0p1 13781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0..^(𝑁 + 1))) |
| 64 | 63 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1))) |
| 65 | 27 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝑇) =
(𝑁 + 1) → (𝑁 ∈
(0..^(♯‘𝑇))
↔ 𝑁 ∈ (0..^(𝑁 + 1)))) |
| 66 | 65 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑁 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(𝑁 + 1)))) |
| 67 | 64, 66 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(♯‘𝑇))) |
| 68 | | ccats1val1 14664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ 〈“𝑆”〉)‘𝑁) = (𝑇‘𝑁)) |
| 69 | 62, 67, 68 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ((𝑇 ++ 〈“𝑆”〉)‘𝑁) = (𝑇‘𝑁)) |
| 70 | 59, 61, 69 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (lastS‘𝑇) = ((𝑇 ++ 〈“𝑆”〉)‘𝑁)) |
| 71 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑆 ∈ 𝑉) |
| 72 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (♯‘𝑇) = (𝑁 + 1)) |
| 73 | 72 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑁 + 1) = (♯‘𝑇)) |
| 74 | | ccats1val2 14665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑁 + 1) = (♯‘𝑇)) → ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1)) = 𝑆) |
| 75 | 74 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑁 + 1) = (♯‘𝑇)) → 𝑆 = ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))) |
| 76 | 62, 71, 73, 75 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑆 = ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))) |
| 77 | 70, 76 | preq12d 4741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → {(lastS‘𝑇), 𝑆} = {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))}) |
| 78 | 77 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ({(lastS‘𝑇), 𝑆} ∈ 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
| 79 | 78 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({(lastS‘𝑇),
𝑆} ∈ 𝐸 → (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
| 80 | 79 | exp4c 432 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({(lastS‘𝑇),
𝑆} ∈ 𝐸 → (𝑆 ∈ 𝑉 → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸)))) |
| 81 | 80 | impcom 407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸))) |
| 82 | 81 | impcom 407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
| 83 | 82 | impcom 407 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸) |
| 84 | 83 | 3adantl3 1169 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸) |
| 85 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑁 → ((𝑇 ++ 〈“𝑆”〉)‘𝑖) = ((𝑇 ++ 〈“𝑆”〉)‘𝑁)) |
| 86 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑁 → ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1)) = ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))) |
| 87 | 85, 86 | preq12d 4741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑁 → {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} = {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))}) |
| 88 | 87 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑁 → ({((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
| 89 | 88 | ralsng 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (∀𝑖 ∈
{𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
| 90 | 89 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (∀𝑖 ∈ {𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ 〈“𝑆”〉)‘𝑁), ((𝑇 ++ 〈“𝑆”〉)‘(𝑁 + 1))} ∈ 𝐸)) |
| 91 | 84, 90 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ {𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) |
| 92 | | ralunb 4197 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑖 ∈
((0..^𝑁) ∪ {𝑁}){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
| 93 | 51, 91, 92 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) |
| 94 | | elnn0uz 12923 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
| 95 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
| 96 | 94, 95 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...𝑁)) |
| 97 | | fzelp1 13616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (0...𝑁) → 𝑁 ∈ (0...(𝑁 + 1))) |
| 98 | | fzosplit 13732 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (0...(𝑁 + 1)) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1)))) |
| 99 | 96, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (0..^(𝑁 + 1)) =
((0..^𝑁) ∪ (𝑁..^(𝑁 + 1)))) |
| 100 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 101 | | fzosn 13775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → (𝑁..^(𝑁 + 1)) = {𝑁}) |
| 102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (𝑁..^(𝑁 + 1)) = {𝑁}) |
| 103 | 102 | uneq2d 4168 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ ((0..^𝑁) ∪
(𝑁..^(𝑁 + 1))) = ((0..^𝑁) ∪ {𝑁})) |
| 104 | 99, 103 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (0..^(𝑁 + 1)) =
((0..^𝑁) ∪ {𝑁})) |
| 105 | 104 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
| 106 | 93, 105 | raleqtrrdv 3330 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) |
| 107 | | ccatlen 14613 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ Word 𝑉 ∧ 〈“𝑆”〉 ∈ Word 𝑉) → (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((♯‘𝑇) +
(♯‘〈“𝑆”〉))) |
| 108 | 5, 20, 107 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((♯‘𝑇) +
(♯‘〈“𝑆”〉))) |
| 109 | 108 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘(𝑇 ++ 〈“𝑆”〉)) − 1) =
(((♯‘𝑇) +
(♯‘〈“𝑆”〉)) − 1)) |
| 110 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘𝑇) = (𝑁 + 1)) |
| 111 | | s1len 14644 |
. . . . . . . . . . . . . . . . . . 19
⊢
(♯‘〈“𝑆”〉) = 1 |
| 112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘〈“𝑆”〉) =
1) |
| 113 | 110, 112 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘𝑇) + (♯‘〈“𝑆”〉)) = ((𝑁 + 1) + 1)) |
| 114 | 113 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((♯‘𝑇) +
(♯‘〈“𝑆”〉)) − 1) = (((𝑁 + 1) + 1) −
1)) |
| 115 | | peano2nn0 12566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
| 116 | 115 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
| 117 | 116, 55 | pncand 11621 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
| 118 | 117 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1)) |
| 119 | 109, 114,
118 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘(𝑇 ++ 〈“𝑆”〉)) − 1) =
(𝑁 + 1)) |
| 120 | 119 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (0..^((♯‘(𝑇 ++ 〈“𝑆”〉)) − 1)) =
(0..^(𝑁 +
1))) |
| 121 | 106, 120 | raleqtrrdv 3330 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) |
| 122 | 18, 22, 121 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
| 123 | 108, 113 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)) |
| 124 | 122, 123 | jca 511 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1))) |
| 125 | 124 | ex 412 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 126 | 4, 125 | syl 17 |
. . . . . . . . 9
⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 127 | 126 | expd 415 |
. . . . . . . 8
⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1))))) |
| 128 | 127 | impcom 407 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 129 | 128 | adantll 714 |
. . . . . 6
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 130 | | iswwlksn 29858 |
. . . . . . . . . 10
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑇 ++
〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ 〈“𝑆”〉) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 131 | 115, 130 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((𝑇 ++
〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ 〈“𝑆”〉) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 132 | 131 | adantl 481 |
. . . . . . . 8
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑇 ++
〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ 〈“𝑆”〉) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 133 | 1, 3 | iswwlks 29856 |
. . . . . . . . 9
⊢ ((𝑇 ++ 〈“𝑆”〉) ∈
(WWalks‘𝐺) ↔
((𝑇 ++ 〈“𝑆”〉) ≠ ∅
∧ (𝑇 ++
〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ 〈“𝑆”〉)) −
1)){((𝑇 ++
〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸)) |
| 134 | 133 | anbi1i 624 |
. . . . . . . 8
⊢ (((𝑇 ++ 〈“𝑆”〉) ∈
(WWalks‘𝐺) ∧
(♯‘(𝑇 ++
〈“𝑆”〉)) = ((𝑁 + 1) + 1)) ↔ (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1))) |
| 135 | 132, 134 | bitrdi 287 |
. . . . . . 7
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝑇 ++
〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 136 | 135 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (((𝑇 ++ 〈“𝑆”〉) ≠ ∅ ∧ (𝑇 ++ 〈“𝑆”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈
(0..^((♯‘(𝑇 ++
〈“𝑆”〉)) − 1)){((𝑇 ++ 〈“𝑆”〉)‘𝑖), ((𝑇 ++ 〈“𝑆”〉)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ 〈“𝑆”〉)) = ((𝑁 + 1) + 1)))) |
| 137 | 129, 136 | sylibrd 259 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺))) |
| 138 | 137 | ex 412 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0)
→ (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)))) |
| 139 | 138 | 3adant3 1133 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0
∧ 𝑇 ∈ Word 𝑉) → (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)))) |
| 140 | 2, 139 | mpcom 38 |
. 2
⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺))) |
| 141 | 140 | 3impib 1117 |
1
⊢ ((𝑇 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalksN 𝐺)) |