Proof of Theorem clwlkclwwlk2
Step | Hyp | Ref
| Expression |
1 | | lswccats1fst 13833 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (lastS‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
2 | 1 | 3adant1 1123 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (lastS‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)) |
3 | 2 | biantrurd 533 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺) ↔
((lastS‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)))) |
4 | | wrdlenccats1lenm1 13820 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → ((♯‘(𝑃 ++ 〈“(𝑃‘0)”〉)) − 1) =
(♯‘𝑃)) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → ((♯‘(𝑃 ++ 〈“(𝑃‘0)”〉)) −
1) = (♯‘𝑃)) |
6 | 5 | oveq2d 7032 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) =
((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
(♯‘𝑃))) |
7 | | simpl 483 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃 ∈ Word 𝑉) |
8 | | wrdsymb1 13751 |
. . . . . . 7
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃‘0) ∈ 𝑉) |
9 | 8 | s1cld 13801 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 〈“(𝑃‘0)”〉 ∈
Word 𝑉) |
10 | | eqidd 2796 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘𝑃) = (♯‘𝑃)) |
11 | | pfxccatid 13939 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉 ∧ (♯‘𝑃) = (♯‘𝑃)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
(♯‘𝑃)) = 𝑃) |
12 | 7, 9, 10, 11 | syl3anc 1364 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
(♯‘𝑃)) = 𝑃) |
13 | 6, 12 | eqtr2d 2832 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃 = ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) −
1))) |
14 | 13 | 3adant1 1123 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃 = ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) −
1))) |
15 | 14 | eleq1d 2867 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃 ∈ (ClWWalks‘𝐺) ↔ ((𝑃 ++ 〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺))) |
16 | | simp1 1129 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝐺 ∈ USPGraph) |
17 | | simp2 1130 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 𝑃 ∈ Word 𝑉) |
18 | 9 | 3adant1 1123 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 〈“(𝑃‘0)”〉 ∈
Word 𝑉) |
19 | | ccatcl 13772 |
. . . 4
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word 𝑉) |
20 | 17, 18, 19 | syl2anc 584 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ Word 𝑉) |
21 | | lencl 13729 |
. . . . . . . 8
⊢ (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈
ℕ0) |
22 | | 1e2m1 11612 |
. . . . . . . . . . 11
⊢ 1 = (2
− 1) |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢
((♯‘𝑃)
∈ ℕ0 → 1 = (2 − 1)) |
24 | 23 | breq1d 4972 |
. . . . . . . . 9
⊢
((♯‘𝑃)
∈ ℕ0 → (1 ≤ (♯‘𝑃) ↔ (2 − 1) ≤
(♯‘𝑃))) |
25 | | 2re 11559 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢
((♯‘𝑃)
∈ ℕ0 → 2 ∈ ℝ) |
27 | | 1red 10488 |
. . . . . . . . . 10
⊢
((♯‘𝑃)
∈ ℕ0 → 1 ∈ ℝ) |
28 | | nn0re 11754 |
. . . . . . . . . 10
⊢
((♯‘𝑃)
∈ ℕ0 → (♯‘𝑃) ∈ ℝ) |
29 | 26, 27, 28 | lesubaddd 11085 |
. . . . . . . . 9
⊢
((♯‘𝑃)
∈ ℕ0 → ((2 − 1) ≤ (♯‘𝑃) ↔ 2 ≤
((♯‘𝑃) +
1))) |
30 | 24, 29 | bitrd 280 |
. . . . . . . 8
⊢
((♯‘𝑃)
∈ ℕ0 → (1 ≤ (♯‘𝑃) ↔ 2 ≤ ((♯‘𝑃) + 1))) |
31 | 21, 30 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ Word 𝑉 → (1 ≤ (♯‘𝑃) ↔ 2 ≤
((♯‘𝑃) +
1))) |
32 | 31 | biimpa 477 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
((♯‘𝑃) +
1)) |
33 | | s1len 13804 |
. . . . . . 7
⊢
(♯‘〈“(𝑃‘0)”〉) = 1 |
34 | 33 | oveq2i 7027 |
. . . . . 6
⊢
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉)) =
((♯‘𝑃) +
1) |
35 | 32, 34 | syl6breqr 5004 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉))) |
36 | 35 | 3adant1 1123 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉))) |
37 | 7, 9 | jca 512 |
. . . . . 6
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉)) |
38 | 37 | 3adant1 1123 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉)) |
39 | | ccatlen 13773 |
. . . . 5
⊢ ((𝑃 ∈ Word 𝑉 ∧ 〈“(𝑃‘0)”〉 ∈ Word 𝑉) → (♯‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉))) |
40 | 38, 39 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (♯‘(𝑃 ++ 〈“(𝑃‘0)”〉)) =
((♯‘𝑃) +
(♯‘〈“(𝑃‘0)”〉))) |
41 | 36, 40 | breqtrrd 4990 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → 2 ≤
(♯‘(𝑃 ++
〈“(𝑃‘0)”〉))) |
42 | | clwlkclwwlk.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
43 | | clwlkclwwlk.e |
. . . 4
⊢ 𝐸 = (iEdg‘𝐺) |
44 | 42, 43 | clwlkclwwlk 27467 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ (𝑃 ++ 〈“(𝑃‘0)”〉) ∈
Word 𝑉 ∧ 2 ≤
(♯‘(𝑃 ++
〈“(𝑃‘0)”〉))) →
(∃𝑓 𝑓(ClWalks‘𝐺)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔
((lastS‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)))) |
45 | 16, 20, 41, 44 | syl3anc 1364 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔
((lastS‘(𝑃 ++
〈“(𝑃‘0)”〉)) = ((𝑃 ++ 〈“(𝑃‘0)”〉)‘0)
∧ ((𝑃 ++
〈“(𝑃‘0)”〉) prefix
((♯‘(𝑃 ++
〈“(𝑃‘0)”〉)) − 1)) ∈
(ClWWalks‘𝐺)))) |
46 | 3, 15, 45 | 3bitr4rd 313 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔ 𝑃 ∈ (ClWWalks‘𝐺))) |