Step | Hyp | Ref
| Expression |
1 | | clwlkclwwlkf.c |
. . . . 5
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€
(β―β(1st βπ€))} |
2 | | eqid 2733 |
. . . . 5
β’
(1st βπ) = (1st βπ) |
3 | | eqid 2733 |
. . . . 5
β’
(2nd βπ) = (2nd βπ) |
4 | 1, 2, 3 | clwlkclwwlkflem 28997 |
. . . 4
β’ (π β πΆ β ((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β)) |
5 | | isclwlk 28770 |
. . . . . . . 8
β’
((1st βπ)(ClWalksβπΊ)(2nd βπ) β ((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))))) |
6 | | fvex 6859 |
. . . . . . . . 9
β’
(1st βπ) β V |
7 | | breq1 5112 |
. . . . . . . . 9
β’ (π = (1st βπ) β (π(ClWalksβπΊ)(2nd βπ) β (1st βπ)(ClWalksβπΊ)(2nd βπ))) |
8 | 6, 7 | spcev 3567 |
. . . . . . . 8
β’
((1st βπ)(ClWalksβπΊ)(2nd βπ) β βπ π(ClWalksβπΊ)(2nd βπ)) |
9 | 5, 8 | sylbir 234 |
. . . . . . 7
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ)))) β
βπ π(ClWalksβπΊ)(2nd βπ)) |
10 | 9 | 3adant3 1133 |
. . . . . 6
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β) β βπ π(ClWalksβπΊ)(2nd βπ)) |
11 | 10 | adantl 483 |
. . . . 5
β’ ((πΊ β USPGraph β§
((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β)) β βπ π(ClWalksβπΊ)(2nd βπ)) |
12 | | simpl 484 |
. . . . . 6
β’ ((πΊ β USPGraph β§
((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β)) β πΊ β USPGraph) |
13 | | eqid 2733 |
. . . . . . . . 9
β’
(VtxβπΊ) =
(VtxβπΊ) |
14 | 13 | wlkpwrd 28614 |
. . . . . . . 8
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (2nd βπ) β Word (VtxβπΊ)) |
15 | 14 | 3ad2ant1 1134 |
. . . . . . 7
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β) β (2nd
βπ) β Word
(VtxβπΊ)) |
16 | 15 | adantl 483 |
. . . . . 6
β’ ((πΊ β USPGraph β§
((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β)) β (2nd
βπ) β Word
(VtxβπΊ)) |
17 | | elnnnn0c 12466 |
. . . . . . . . . 10
β’
((β―β(1st βπ)) β β β
((β―β(1st βπ)) β β0 β§ 1 β€
(β―β(1st βπ)))) |
18 | | nn0re 12430 |
. . . . . . . . . . . . . 14
β’
((β―β(1st βπ)) β β0 β
(β―β(1st βπ)) β β) |
19 | | 1e2m1 12288 |
. . . . . . . . . . . . . . . . 17
β’ 1 = (2
β 1) |
20 | 19 | breq1i 5116 |
. . . . . . . . . . . . . . . 16
β’ (1 β€
(β―β(1st βπ)) β (2 β 1) β€
(β―β(1st βπ))) |
21 | 20 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ (1 β€
(β―β(1st βπ)) β (2 β 1) β€
(β―β(1st βπ))) |
22 | | 2re 12235 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
23 | | 1re 11163 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
24 | | lesubadd 11635 |
. . . . . . . . . . . . . . . 16
β’ ((2
β β β§ 1 β β β§ (β―β(1st
βπ)) β β)
β ((2 β 1) β€ (β―β(1st βπ)) β 2 β€
((β―β(1st βπ)) + 1))) |
25 | 22, 23, 24 | mp3an12 1452 |
. . . . . . . . . . . . . . 15
β’
((β―β(1st βπ)) β β β ((2 β 1) β€
(β―β(1st βπ)) β 2 β€
((β―β(1st βπ)) + 1))) |
26 | 21, 25 | imbitrid 243 |
. . . . . . . . . . . . . 14
β’
((β―β(1st βπ)) β β β (1 β€
(β―β(1st βπ)) β 2 β€
((β―β(1st βπ)) + 1))) |
27 | 18, 26 | syl 17 |
. . . . . . . . . . . . 13
β’
((β―β(1st βπ)) β β0 β (1 β€
(β―β(1st βπ)) β 2 β€
((β―β(1st βπ)) + 1))) |
28 | 27 | adantl 483 |
. . . . . . . . . . . 12
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) β
β0) β (1 β€ (β―β(1st βπ)) β 2 β€
((β―β(1st βπ)) + 1))) |
29 | | wlklenvp1 28615 |
. . . . . . . . . . . . . 14
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (β―β(2nd
βπ)) =
((β―β(1st βπ)) + 1)) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) β
β0) β (β―β(2nd βπ)) =
((β―β(1st βπ)) + 1)) |
31 | 30 | breq2d 5121 |
. . . . . . . . . . . 12
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) β
β0) β (2 β€ (β―β(2nd βπ)) β 2 β€
((β―β(1st βπ)) + 1))) |
32 | 28, 31 | sylibrd 259 |
. . . . . . . . . . 11
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) β
β0) β (1 β€ (β―β(1st βπ)) β 2 β€
(β―β(2nd βπ)))) |
33 | 32 | expimpd 455 |
. . . . . . . . . 10
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (((β―β(1st
βπ)) β
β0 β§ 1 β€ (β―β(1st βπ))) β 2 β€
(β―β(2nd βπ)))) |
34 | 17, 33 | biimtrid 241 |
. . . . . . . . 9
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β ((β―β(1st
βπ)) β β
β 2 β€ (β―β(2nd βπ)))) |
35 | 34 | a1d 25 |
. . . . . . . 8
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β
((β―β(1st βπ)) β β β 2 β€
(β―β(2nd βπ))))) |
36 | 35 | 3imp 1112 |
. . . . . . 7
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β) β 2 β€
(β―β(2nd βπ))) |
37 | 36 | adantl 483 |
. . . . . 6
β’ ((πΊ β USPGraph β§
((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β)) β 2 β€
(β―β(2nd βπ))) |
38 | | eqid 2733 |
. . . . . . 7
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
39 | 13, 38 | clwlkclwwlk 28995 |
. . . . . 6
β’ ((πΊ β USPGraph β§
(2nd βπ)
β Word (VtxβπΊ)
β§ 2 β€ (β―β(2nd βπ))) β (βπ π(ClWalksβπΊ)(2nd βπ) β ((lastSβ(2nd
βπ)) =
((2nd βπ)β0) β§ ((2nd
βπ) prefix
((β―β(2nd βπ)) β 1)) β (ClWWalksβπΊ)))) |
40 | 12, 16, 37, 39 | syl3anc 1372 |
. . . . 5
β’ ((πΊ β USPGraph β§
((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β)) β (βπ π(ClWalksβπΊ)(2nd βπ) β ((lastSβ(2nd
βπ)) =
((2nd βπ)β0) β§ ((2nd
βπ) prefix
((β―β(2nd βπ)) β 1)) β (ClWWalksβπΊ)))) |
41 | 11, 40 | mpbid 231 |
. . . 4
β’ ((πΊ β USPGraph β§
((1st βπ)(WalksβπΊ)(2nd βπ) β§ ((2nd βπ)β0) = ((2nd
βπ)β(β―β(1st
βπ))) β§
(β―β(1st βπ)) β β)) β
((lastSβ(2nd βπ)) = ((2nd βπ)β0) β§
((2nd βπ)
prefix ((β―β(2nd βπ)) β 1)) β (ClWWalksβπΊ))) |
42 | 4, 41 | sylan2 594 |
. . 3
β’ ((πΊ β USPGraph β§ π β πΆ) β ((lastSβ(2nd
βπ)) =
((2nd βπ)β0) β§ ((2nd
βπ) prefix
((β―β(2nd βπ)) β 1)) β (ClWWalksβπΊ))) |
43 | 42 | simprd 497 |
. 2
β’ ((πΊ β USPGraph β§ π β πΆ) β ((2nd βπ) prefix
((β―β(2nd βπ)) β 1)) β (ClWWalksβπΊ)) |
44 | | clwlkclwwlkf.f |
. 2
β’ πΉ = (π β πΆ β¦ ((2nd βπ) prefix
((β―β(2nd βπ)) β 1))) |
45 | 43, 44 | fmptd 7066 |
1
β’ (πΊ β USPGraph β πΉ:πΆβΆ(ClWWalksβπΊ)) |