Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β πΊ β USPGraph) |
2 | | wrdsymb1 14450 |
. . . . . 6
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (πβ0) β π) |
3 | 2 | s1cld 14500 |
. . . . 5
β’ ((π β Word π β§ 1 β€ (β―βπ)) β β¨β(πβ0)ββ© β
Word π) |
4 | | ccatcl 14471 |
. . . . 5
β’ ((π β Word π β§ β¨β(πβ0)ββ© β Word π) β (π ++ β¨β(πβ0)ββ©) β Word π) |
5 | 3, 4 | syldan 592 |
. . . 4
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (π ++ β¨β(πβ0)ββ©) β Word π) |
6 | 5 | 3adant1 1131 |
. . 3
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (π ++ β¨β(πβ0)ββ©) β Word π) |
7 | | lencl 14430 |
. . . . . . . 8
β’ (π β Word π β (β―βπ) β
β0) |
8 | | 1e2m1 12288 |
. . . . . . . . . 10
β’ 1 = (2
β 1) |
9 | 8 | breq1i 5116 |
. . . . . . . . 9
β’ (1 β€
(β―βπ) β (2
β 1) β€ (β―βπ)) |
10 | | 2re 12235 |
. . . . . . . . . . 11
β’ 2 β
β |
11 | 10 | a1i 11 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β 2 β β) |
12 | | 1red 11164 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β 1 β β) |
13 | | nn0re 12430 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β (β―βπ) β β) |
14 | 11, 12, 13 | lesubaddd 11760 |
. . . . . . . . 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 478 |
. . . . . 6
β’ ((π β Word π β§ 1 β€ (β―βπ)) β 2 β€
((β―βπ) +
1)) |
18 | | s1len 14503 |
. . . . . . 7
β’
(β―ββ¨β(πβ0)ββ©) = 1 |
19 | 18 | oveq2i 7372 |
. . . . . 6
β’
((β―βπ) +
(β―ββ¨β(πβ0)ββ©)) =
((β―βπ) +
1) |
20 | 17, 19 | breqtrrdi 5151 |
. . . . 5
β’ ((π β Word π β§ 1 β€ (β―βπ)) β 2 β€
((β―βπ) +
(β―ββ¨β(πβ0)ββ©))) |
21 | | ccatlen 14472 |
. . . . . 6
β’ ((π β Word π β§ β¨β(πβ0)ββ© β Word π) β (β―β(π ++ β¨β(πβ0)ββ©)) =
((β―βπ) +
(β―ββ¨β(πβ0)ββ©))) |
22 | 3, 21 | syldan 592 |
. . . . 5
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (β―β(π ++ β¨β(πβ0)ββ©)) =
((β―βπ) +
(β―ββ¨β(πβ0)ββ©))) |
23 | 20, 22 | breqtrrd 5137 |
. . . 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 28995 |
. . 3
β’ ((πΊ β USPGraph β§ (π ++ β¨β(πβ0)ββ©) β
Word π β§ 2 β€
(β―β(π ++
β¨β(πβ0)ββ©))) β
(βπ π(ClWalksβπΊ)(π ++ β¨β(πβ0)ββ©) β
((lastSβ(π ++
β¨β(πβ0)ββ©)) = ((π ++ β¨β(πβ0)ββ©)β0)
β§ ((π ++
β¨β(πβ0)ββ©) prefix
((β―β(π ++
β¨β(πβ0)ββ©)) β 1)) β
(ClWWalksβπΊ)))) |
28 | 1, 6, 24, 27 | syl3anc 1372 |
. 2
β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (βπ π(ClWalksβπΊ)(π ++ β¨β(πβ0)ββ©) β
((lastSβ(π ++
β¨β(πβ0)ββ©)) = ((π ++ β¨β(πβ0)ββ©)β0)
β§ ((π ++
β¨β(πβ0)ββ©) prefix
((β―β(π ++
β¨β(πβ0)ββ©)) β 1)) β
(ClWWalksβπΊ)))) |
29 | | wrdlenccats1lenm1 14519 |
. . . . . . . 8
β’ (π β Word π β ((β―β(π ++ β¨β(πβ0)ββ©)) β 1) =
(β―βπ)) |
30 | 29 | oveq2d 7377 |
. . . . . . 7
β’ (π β Word π β ((π ++ β¨β(πβ0)ββ©) prefix
((β―β(π ++
β¨β(πβ0)ββ©)) β 1)) =
((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ))) |
31 | 30 | adantr 482 |
. . . . . 6
β’ ((π β Word π β§ 1 β€ (β―βπ)) β ((π ++ β¨β(πβ0)ββ©) prefix
((β―β(π ++
β¨β(πβ0)ββ©)) β 1)) =
((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ))) |
32 | | simpl 484 |
. . . . . . 7
β’ ((π β Word π β§ 1 β€ (β―βπ)) β π β Word π) |
33 | | eqidd 2734 |
. . . . . . 7
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (β―βπ) = (β―βπ)) |
34 | | pfxccatid 14638 |
. . . . . . 7
β’ ((π β Word π β§ β¨β(πβ0)ββ© β Word π β§ (β―βπ) = (β―βπ)) β ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ)) = π) |
35 | 32, 3, 33, 34 | syl3anc 1372 |
. . . . . 6
β’ ((π β Word π β§ 1 β€ (β―βπ)) β ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ)) = π) |
36 | 31, 35 | eqtr2d 2774 |
. . . . 5
β’ ((π β Word π β§ 1 β€ (β―βπ)) β π = ((π ++ β¨β(πβ0)ββ©) prefix
((β―β(π ++
β¨β(πβ0)ββ©)) β
1))) |
37 | 36 | eleq1d 2819 |
. . . 4
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (π β (ClWWalksβπΊ) β ((π ++ β¨β(πβ0)ββ©) prefix
((β―β(π ++
β¨β(πβ0)ββ©)) β 1)) β
(ClWWalksβπΊ))) |
38 | | lswccats1fst 14532 |
. . . . 5
β’ ((π β Word π β§ 1 β€ (β―βπ)) β (lastSβ(π ++ β¨β(πβ0)ββ©)) =
((π ++ β¨β(πβ0)ββ©)β0)) |
39 | 38 | biantrurd 534 |
. . . 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βπΊ))) |