Proof of Theorem clwlkclwwlk2
| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝐺 ∈ USPGraph) |
| 2 | | wrdsymb1 14591 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃‘0) ∈ 𝑉) |
| 3 | 2 | s1cld 14641 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 〈“(𝑃‘0)”〉 ∈
Word 𝑉) |
| 4 | | ccatcl 14612 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word 𝑉) |
| 5 | 3, 4 | syldan 591 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word 𝑉) |
| 6 | 5 | 3adant1 1131 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word 𝑉) |
| 7 | | lencl 14571 |
. . . . . . . 8
⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈
ℕ0) |
| 8 | | 1e2m1 12393 |
. . . . . . . . . 10
⊢ 1 = (2
− 1) |
| 9 | 8 | breq1i 5150 |
. . . . . . . . 9
⊢ (1 ≤
(♯‘𝑃) ↔ (2
− 1) ≤ (♯‘𝑃)) |
| 10 | | 2re 12340 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
| 11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢
((♯‘𝑃)
∈ ℕ0 → 2 ∈ ℝ) |
| 12 | | 1red 11262 |
. . . . . . . . . 10
⊢
((♯‘𝑃)
∈ ℕ0 → 1 ∈ ℝ) |
| 13 | | nn0re 12535 |
. . . . . . . . . 10
⊢
((♯‘𝑃)
∈ ℕ0 → (♯‘𝑃) ∈ ℝ) |
| 14 | 11, 12, 13 | lesubaddd 11860 |
. . . . . . . . 9
⊢
((♯‘𝑃)
∈ ℕ0 → ((2 − 1) ≤ (♯‘𝑃) ↔ 2 ≤
((♯‘𝑃) +
1))) |
| 15 | 9, 14 | bitrid 283 |
. . . . . . . 8
⊢
((♯‘𝑃)
∈ ℕ0 → (1 ≤ (♯‘𝑃) ↔ 2 ≤ ((♯‘𝑃) + 1))) |
| 16 | 7, 15 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (1 ≤ (♯‘𝑃) ↔ 2 ≤
((♯‘𝑃) +
1))) |
| 17 | 16 | biimpa 476 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
((♯‘𝑃) +
1)) |
| 18 | | s1len 14644 |
. . . . . . 7
⊢
(♯‘〈“(𝑃‘0)”〉) = 1 |
| 19 | 18 | oveq2i 7442 |
. . . . . 6
⊢
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉)) =
((♯‘𝑃) +
1) |
| 20 | 17, 19 | breqtrrdi 5185 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉))) |
| 21 | | ccatlen 14613 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉) → (♯‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉))) |
| 22 | 3, 21 | syldan 591 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉))) |
| 23 | 20, 22 | breqtrrd 5171 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
(♯‘(𝑃 ++
〈“(𝑃‘0)”〉))) |
| 24 | 23 | 3adant1 1131 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
(♯‘(𝑃 ++
〈“(𝑃‘0)”〉))) |
| 25 | | clwlkclwwlk.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 26 | | clwlkclwwlk.e |
. . . 4
⊢ 𝐸 = (iEdg‘𝐺) |
| 27 | 25, 26 | clwlkclwwlk 30021 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ (𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word 𝑉 ∧ 2 ≤
(♯‘(𝑃 ++
〈“(𝑃‘0)”〉))) →
(∃𝑓 𝑓(ClWalks‘𝐺)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔
((lastS‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)))) |
| 28 | 1, 6, 24, 27 | syl3anc 1373 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔
((lastS‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)))) |
| 29 | | wrdlenccats1lenm1 14660 |
. . . . . . . 8
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘(𝑃 ++ 〈“(𝑃‘0)”〉)) − 1) =
(♯‘𝑃)) |
| 30 | 29 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) =
((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
(♯‘𝑃))) |
| 31 | 30 | adantr 480 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) =
((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
(♯‘𝑃))) |
| 32 | | simpl 482 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃 ∈ Word 𝑉) |
| 33 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘𝑃) = (♯‘𝑃)) |
| 34 | | pfxccatid 14779 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉 ∧ (♯‘𝑃) = (♯‘𝑃)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
(♯‘𝑃)) = 𝑃) |
| 35 | 32, 3, 33, 34 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
(♯‘𝑃)) = 𝑃) |
| 36 | 31, 35 | eqtr2d 2778 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃 = ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) −
1))) |
| 37 | 36 | eleq1d 2826 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃 ∈ (ClWWalks‘𝐺) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺))) |
| 38 | | lswccats1fst 14673 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (lastS‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
| 39 | 38 | biantrurd 532 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺) ↔
((lastS‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)))) |
| 40 | 37, 39 | bitr2d 280 |
. . 3
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (((lastS‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)) ↔
𝑃 ∈
(ClWWalks‘𝐺))) |
| 41 | 40 | 3adant1 1131 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (((lastS‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)) ↔
𝑃 ∈
(ClWWalks‘𝐺))) |
| 42 | 28, 41 | bitrd 279 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔ 𝑃 ∈ (ClWWalks‘𝐺))) |