Step | Hyp | Ref
| Expression |
1 | | clwlkwlk 28765 |
. . 3
β’ (πΆ β (ClWalksβπΊ) β πΆ β (WalksβπΊ)) |
2 | | wlkcpr 28619 |
. . . 4
β’ (πΆ β (WalksβπΊ) β (1st
βπΆ)(WalksβπΊ)(2nd βπΆ)) |
3 | | eqid 2737 |
. . . . . . . 8
β’
(VtxβπΊ) =
(VtxβπΊ) |
4 | 3 | wlkpwrd 28607 |
. . . . . . 7
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β (2nd βπΆ) β Word (VtxβπΊ)) |
5 | | lencl 14428 |
. . . . . . . . 9
β’
((2nd βπΆ) β Word (VtxβπΊ) β (β―β(2nd
βπΆ)) β
β0) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β (β―β(2nd
βπΆ)) β
β0) |
7 | | wlklenvm1 28612 |
. . . . . . . . . . 11
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β (β―β(1st
βπΆ)) =
((β―β(2nd βπΆ)) β 1)) |
8 | 7 | breq2d 5122 |
. . . . . . . . . 10
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β (1 β€
(β―β(1st βπΆ)) β 1 β€
((β―β(2nd βπΆ)) β 1))) |
9 | | 1red 11163 |
. . . . . . . . . . . . 13
β’
((β―β(2nd βπΆ)) β β0 β 1
β β) |
10 | | nn0re 12429 |
. . . . . . . . . . . . 13
β’
((β―β(2nd βπΆ)) β β0 β
(β―β(2nd βπΆ)) β β) |
11 | 9, 9, 10 | leaddsub2d 11764 |
. . . . . . . . . . . 12
β’
((β―β(2nd βπΆ)) β β0 β ((1 +
1) β€ (β―β(2nd βπΆ)) β 1 β€
((β―β(2nd βπΆ)) β 1))) |
12 | | 1p1e2 12285 |
. . . . . . . . . . . . . 14
β’ (1 + 1) =
2 |
13 | 12 | breq1i 5117 |
. . . . . . . . . . . . 13
β’ ((1 + 1)
β€ (β―β(2nd βπΆ)) β 2 β€
(β―β(2nd βπΆ))) |
14 | 13 | biimpi 215 |
. . . . . . . . . . . 12
β’ ((1 + 1)
β€ (β―β(2nd βπΆ)) β 2 β€
(β―β(2nd βπΆ))) |
15 | 11, 14 | syl6bir 254 |
. . . . . . . . . . 11
β’
((β―β(2nd βπΆ)) β β0 β (1 β€
((β―β(2nd βπΆ)) β 1) β 2 β€
(β―β(2nd βπΆ)))) |
16 | 4, 5, 15 | 3syl 18 |
. . . . . . . . . 10
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β (1 β€
((β―β(2nd βπΆ)) β 1) β 2 β€
(β―β(2nd βπΆ)))) |
17 | 8, 16 | sylbid 239 |
. . . . . . . . 9
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β (1 β€
(β―β(1st βπΆ)) β 2 β€
(β―β(2nd βπΆ)))) |
18 | 17 | imp 408 |
. . . . . . . 8
β’
(((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β§ 1 β€
(β―β(1st βπΆ))) β 2 β€
(β―β(2nd βπΆ))) |
19 | | ige2m1fz 13538 |
. . . . . . . 8
β’
(((β―β(2nd βπΆ)) β β0 β§ 2 β€
(β―β(2nd βπΆ))) β ((β―β(2nd
βπΆ)) β 1)
β (0...(β―β(2nd βπΆ)))) |
20 | 6, 18, 19 | syl2an2r 684 |
. . . . . . 7
β’
(((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β§ 1 β€
(β―β(1st βπΆ))) β ((β―β(2nd
βπΆ)) β 1)
β (0...(β―β(2nd βπΆ)))) |
21 | | pfxlen 14578 |
. . . . . . 7
β’
(((2nd βπΆ) β Word (VtxβπΊ) β§ ((β―β(2nd
βπΆ)) β 1)
β (0...(β―β(2nd βπΆ)))) β (β―β((2nd
βπΆ) prefix
((β―β(2nd βπΆ)) β 1))) =
((β―β(2nd βπΆ)) β 1)) |
22 | 4, 20, 21 | syl2an2r 684 |
. . . . . 6
β’
(((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β§ 1 β€
(β―β(1st βπΆ))) β (β―β((2nd
βπΆ) prefix
((β―β(2nd βπΆ)) β 1))) =
((β―β(2nd βπΆ)) β 1)) |
23 | 7 | eqcomd 2743 |
. . . . . . 7
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β ((β―β(2nd
βπΆ)) β 1) =
(β―β(1st βπΆ))) |
24 | 23 | adantr 482 |
. . . . . 6
β’
(((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β§ 1 β€
(β―β(1st βπΆ))) β ((β―β(2nd
βπΆ)) β 1) =
(β―β(1st βπΆ))) |
25 | 22, 24 | eqtrd 2777 |
. . . . 5
β’
(((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β§ 1 β€
(β―β(1st βπΆ))) β (β―β((2nd
βπΆ) prefix
((β―β(2nd βπΆ)) β 1))) =
(β―β(1st βπΆ))) |
26 | 25 | ex 414 |
. . . 4
β’
((1st βπΆ)(WalksβπΊ)(2nd βπΆ) β (1 β€
(β―β(1st βπΆ)) β (β―β((2nd
βπΆ) prefix
((β―β(2nd βπΆ)) β 1))) =
(β―β(1st βπΆ)))) |
27 | 2, 26 | sylbi 216 |
. . 3
β’ (πΆ β (WalksβπΊ) β (1 β€
(β―β(1st βπΆ)) β (β―β((2nd
βπΆ) prefix
((β―β(2nd βπΆ)) β 1))) =
(β―β(1st βπΆ)))) |
28 | 1, 27 | syl 17 |
. 2
β’ (πΆ β (ClWalksβπΊ) β (1 β€
(β―β(1st βπΆ)) β (β―β((2nd
βπΆ) prefix
((β―β(2nd βπΆ)) β 1))) =
(β―β(1st βπΆ)))) |
29 | 28 | imp 408 |
1
β’ ((πΆ β (ClWalksβπΊ) β§ 1 β€
(β―β(1st βπΆ))) β (β―β((2nd
βπΆ) prefix
((β―β(2nd βπΆ)) β 1))) =
(β―β(1st βπΆ))) |