Step | Hyp | Ref
| Expression |
1 | | wwlksnext.v |
. . . . 5
β’ π = (VtxβπΊ) |
2 | | wwlksnext.e |
. . . . 5
β’ πΈ = (EdgβπΊ) |
3 | 1, 2 | wwlknp 29361 |
. . . 4
β’ (π β ((π + 1) WWalksN πΊ) β (π β Word π β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ)) |
4 | | wwlksnred 29410 |
. . . . . . . 8
β’ (π β β0
β (π β ((π + 1) WWalksN πΊ) β (π prefix (π + 1)) β (π WWalksN πΊ))) |
5 | 4 | ad2antrr 723 |
. . . . . . 7
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β (π β ((π + 1) WWalksN πΊ) β (π prefix (π + 1)) β (π WWalksN πΊ))) |
6 | | fveqeq2 6901 |
. . . . . . . . . . . . . . . 16
β’ (π = (π ++ β¨βπββ©) β ((β―βπ) = ((π + 1) + 1) β (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1))) |
7 | 6 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . 15
β’ ((π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ) β ((β―βπ) = ((π + 1) + 1) β (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1))) |
8 | 7 | adantl 481 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β ((β―βπ) = ((π + 1) + 1) β (β―β(π ++ β¨βπββ©)) = ((π + 1) + 1))) |
9 | | s1cl 14557 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β¨βπββ© β Word π) |
10 | 9 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β0
β§ π β π) β β¨βπββ© β Word π) |
11 | 10 | anim1ci 615 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β0
β§ π β π) β§ π β Word π) β (π β Word π β§ β¨βπββ© β Word π)) |
12 | | ccatlen 14530 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ β¨βπββ© β Word π) β (β―β(π ++ β¨βπββ©)) = ((β―βπ) +
(β―ββ¨βπββ©))) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β π) β§ π β Word π) β (β―β(π ++ β¨βπββ©)) = ((β―βπ) +
(β―ββ¨βπββ©))) |
14 | 13 | eqeq1d 2733 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ π β π) β§ π β Word π) β ((β―β(π ++ β¨βπββ©)) = ((π + 1) + 1) β ((β―βπ) +
(β―ββ¨βπββ©)) = ((π + 1) + 1))) |
15 | | s1len 14561 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β―ββ¨βπββ©) = 1 |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β0
β§ π β π) β§ π β Word π) β (β―ββ¨βπββ©) =
1) |
17 | 16 | oveq2d 7428 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β π) β§ π β Word π) β ((β―βπ) + (β―ββ¨βπββ©)) =
((β―βπ) +
1)) |
18 | 17 | eqeq1d 2733 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ π β π) β§ π β Word π) β (((β―βπ) + (β―ββ¨βπββ©)) = ((π + 1) + 1) β
((β―βπ) + 1) =
((π + 1) +
1))) |
19 | | lencl 14488 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Word π β (β―βπ) β
β0) |
20 | 19 | nn0cnd 12539 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Word π β (β―βπ) β β) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β π) β§ π β Word π) β (β―βπ) β β) |
22 | | peano2nn0 12517 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (π + 1) β
β0) |
23 | 22 | nn0cnd 12539 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (π + 1) β
β) |
24 | 23 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β π) β§ π β Word π) β (π + 1) β β) |
25 | | 1cnd 11214 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β π) β§ π β Word π) β 1 β β) |
26 | 21, 24, 25 | addcan2d 11423 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ π β π) β§ π β Word π) β (((β―βπ) + 1) = ((π + 1) + 1) β (β―βπ) = (π + 1))) |
27 | 14, 18, 26 | 3bitrd 304 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ π β π) β§ π β Word π) β ((β―β(π ++ β¨βπββ©)) = ((π + 1) + 1) β (β―βπ) = (π + 1))) |
28 | | oveq2 7420 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) = (β―βπ) β ((π ++ β¨βπββ©) prefix (π + 1)) = ((π ++ β¨βπββ©) prefix (β―βπ))) |
29 | 28 | eqcoms 2739 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ) =
(π + 1) β ((π ++ β¨βπββ©) prefix (π + 1)) = ((π ++ β¨βπββ©) prefix (β―βπ))) |
30 | | pfxccat1 14657 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Word π β§ β¨βπββ© β Word π) β ((π ++ β¨βπββ©) prefix (β―βπ)) = π) |
31 | 11, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ π β π) β§ π β Word π) β ((π ++ β¨βπββ©) prefix (β―βπ)) = π) |
32 | 29, 31 | sylan9eqr 2793 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β β0
β§ π β π) β§ π β Word π) β§ (β―βπ) = (π + 1)) β ((π ++ β¨βπββ©) prefix (π + 1)) = π) |
33 | 32 | ex 412 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ π β π) β§ π β Word π) β ((β―βπ) = (π + 1) β ((π ++ β¨βπββ©) prefix (π + 1)) = π)) |
34 | 27, 33 | sylbid 239 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ π β π) β§ π β Word π) β ((β―β(π ++ β¨βπββ©)) = ((π + 1) + 1) β ((π ++ β¨βπββ©) prefix (π + 1)) = π)) |
35 | 34 | 3ad2antr1 1187 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β ((β―β(π ++ β¨βπββ©)) = ((π + 1) + 1) β ((π ++ β¨βπββ©) prefix (π + 1)) = π)) |
36 | 8, 35 | sylbid 239 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β ((β―βπ) = ((π + 1) + 1) β ((π ++ β¨βπββ©) prefix (π + 1)) = π)) |
37 | 36 | imp 406 |
. . . . . . . . . . . 12
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β§ (β―βπ) = ((π + 1) + 1)) β ((π ++ β¨βπββ©) prefix (π + 1)) = π) |
38 | | oveq1 7419 |
. . . . . . . . . . . . . . 15
β’ (π = (π ++ β¨βπββ©) β (π prefix (π + 1)) = ((π ++ β¨βπββ©) prefix (π + 1))) |
39 | 38 | eqeq1d 2733 |
. . . . . . . . . . . . . 14
β’ (π = (π ++ β¨βπββ©) β ((π prefix (π + 1)) = π β ((π ++ β¨βπββ©) prefix (π + 1)) = π)) |
40 | 39 | 3ad2ant2 1133 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ) β ((π prefix (π + 1)) = π β ((π ++ β¨βπββ©) prefix (π + 1)) = π)) |
41 | 40 | ad2antlr 724 |
. . . . . . . . . . . 12
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β§ (β―βπ) = ((π + 1) + 1)) β ((π prefix (π + 1)) = π β ((π ++ β¨βπββ©) prefix (π + 1)) = π)) |
42 | 37, 41 | mpbird 256 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β§ (β―βπ) = ((π + 1) + 1)) β (π prefix (π + 1)) = π) |
43 | 42 | eleq1d 2817 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β§ (β―βπ) = ((π + 1) + 1)) β ((π prefix (π + 1)) β (π WWalksN πΊ) β π β (π WWalksN πΊ))) |
44 | 43 | biimpd 228 |
. . . . . . . . 9
β’ ((((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β§ (β―βπ) = ((π + 1) + 1)) β ((π prefix (π + 1)) β (π WWalksN πΊ) β π β (π WWalksN πΊ))) |
45 | 44 | ex 412 |
. . . . . . . 8
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β ((β―βπ) = ((π + 1) + 1) β ((π prefix (π + 1)) β (π WWalksN πΊ) β π β (π WWalksN πΊ)))) |
46 | 45 | com23 86 |
. . . . . . 7
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β ((π prefix (π + 1)) β (π WWalksN πΊ) β ((β―βπ) = ((π + 1) + 1) β π β (π WWalksN πΊ)))) |
47 | 5, 46 | syld 47 |
. . . . . 6
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β (π β ((π + 1) WWalksN πΊ) β ((β―βπ) = ((π + 1) + 1) β π β (π WWalksN πΊ)))) |
48 | 47 | com13 88 |
. . . . 5
β’
((β―βπ) =
((π + 1) + 1) β (π β ((π + 1) WWalksN πΊ) β (((π β β0 β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β π β (π WWalksN πΊ)))) |
49 | 48 | 3ad2ant2 1133 |
. . . 4
β’ ((π β Word π β§ (β―βπ) = ((π + 1) + 1) β§ βπ β (0..^(π + 1)){(πβπ), (πβ(π + 1))} β πΈ) β (π β ((π + 1) WWalksN πΊ) β (((π β β0 β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β π β (π WWalksN πΊ)))) |
50 | 3, 49 | mpcom 38 |
. . 3
β’ (π β ((π + 1) WWalksN πΊ) β (((π β β0 β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β π β (π WWalksN πΊ))) |
51 | 50 | com12 32 |
. 2
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β (π β ((π + 1) WWalksN πΊ) β π β (π WWalksN πΊ))) |
52 | 1, 2 | wwlksnext 29411 |
. . . . . . . . . . 11
β’ ((π β (π WWalksN πΊ) β§ π β π β§ {(lastSβπ), π} β πΈ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ)) |
53 | | eleq1 2820 |
. . . . . . . . . . 11
β’ (π = (π ++ β¨βπββ©) β (π β ((π + 1) WWalksN πΊ) β (π ++ β¨βπββ©) β ((π + 1) WWalksN πΊ))) |
54 | 52, 53 | syl5ibrcom 246 |
. . . . . . . . . 10
β’ ((π β (π WWalksN πΊ) β§ π β π β§ {(lastSβπ), π} β πΈ) β (π = (π ++ β¨βπββ©) β π β ((π + 1) WWalksN πΊ))) |
55 | 54 | 3exp 1118 |
. . . . . . . . 9
β’ (π β (π WWalksN πΊ) β (π β π β ({(lastSβπ), π} β πΈ β (π = (π ++ β¨βπββ©) β π β ((π + 1) WWalksN πΊ))))) |
56 | 55 | com23 86 |
. . . . . . . 8
β’ (π β (π WWalksN πΊ) β ({(lastSβπ), π} β πΈ β (π β π β (π = (π ++ β¨βπββ©) β π β ((π + 1) WWalksN πΊ))))) |
57 | 56 | com14 96 |
. . . . . . 7
β’ (π = (π ++ β¨βπββ©) β ({(lastSβπ), π} β πΈ β (π β π β (π β (π WWalksN πΊ) β π β ((π + 1) WWalksN πΊ))))) |
58 | 57 | imp 406 |
. . . . . 6
β’ ((π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ) β (π β π β (π β (π WWalksN πΊ) β π β ((π + 1) WWalksN πΊ)))) |
59 | 58 | 3adant1 1129 |
. . . . 5
β’ ((π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ) β (π β π β (π β (π WWalksN πΊ) β π β ((π + 1) WWalksN πΊ)))) |
60 | 59 | com12 32 |
. . . 4
β’ (π β π β ((π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ) β (π β (π WWalksN πΊ) β π β ((π + 1) WWalksN πΊ)))) |
61 | 60 | adantl 481 |
. . 3
β’ ((π β β0
β§ π β π) β ((π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ) β (π β (π WWalksN πΊ) β π β ((π + 1) WWalksN πΊ)))) |
62 | 61 | imp 406 |
. 2
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β (π β (π WWalksN πΊ) β π β ((π + 1) WWalksN πΊ))) |
63 | 51, 62 | impbid 211 |
1
β’ (((π β β0
β§ π β π) β§ (π β Word π β§ π = (π ++ β¨βπββ©) β§ {(lastSβπ), π} β πΈ)) β (π β ((π + 1) WWalksN πΊ) β π β (π WWalksN πΊ))) |