Step | Hyp | Ref
| Expression |
1 | | clwwlkf1o.d |
. . 3
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} |
2 | | clwwlkf1o.f |
. . 3
β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) |
3 | 1, 2 | clwwlkf 29040 |
. 2
β’ (π β β β πΉ:π·βΆ(π ClWWalksN πΊ)) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(VtxβπΊ) =
(VtxβπΊ) |
5 | | eqid 2733 |
. . . . . . . 8
β’
(EdgβπΊ) =
(EdgβπΊ) |
6 | 4, 5 | clwwlknp 29030 |
. . . . . . 7
β’ (π β (π ClWWalksN πΊ) β ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) |
7 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β π β β) |
8 | | simpl1 1192 |
. . . . . . . . . 10
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β (π β Word (VtxβπΊ) β§ (β―βπ) = π)) |
9 | | 3simpc 1151 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) |
10 | 9 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) |
11 | 1 | clwwlkel 29039 |
. . . . . . . . . 10
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ (βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (π ++ β¨β(πβ0)ββ©) β π·) |
12 | 7, 8, 10, 11 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β (π ++ β¨β(πβ0)ββ©) β π·) |
13 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π = (β―βπ) β ((π ++ β¨β(πβ0)ββ©) prefix π) = ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ))) |
14 | 13 | eqcoms 2741 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
π β ((π ++ β¨β(πβ0)ββ©) prefix
π) = ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ))) |
15 | 14 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = π) β ((π ++ β¨β(πβ0)ββ©) prefix π) = ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ))) |
16 | 15 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β ((π ++ β¨β(πβ0)ββ©) prefix π) = ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ))) |
17 | 16 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β ((π ++ β¨β(πβ0)ββ©) prefix π) = ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ))) |
18 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ π β β) β π β Word (VtxβπΊ)) |
19 | | fstwrdne0 14453 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ (π β Word (VtxβπΊ) β§ (β―βπ) = π)) β (πβ0) β (VtxβπΊ)) |
20 | 19 | ancoms 460 |
. . . . . . . . . . . . . 14
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ π β β) β (πβ0) β (VtxβπΊ)) |
21 | 20 | s1cld 14500 |
. . . . . . . . . . . . 13
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ π β β) β β¨β(πβ0)ββ© β
Word (VtxβπΊ)) |
22 | 18, 21 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ π β β) β (π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β Word
(VtxβπΊ))) |
23 | 22 | 3ad2antl1 1186 |
. . . . . . . . . . 11
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β (π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β Word
(VtxβπΊ))) |
24 | | pfxccat1 14599 |
. . . . . . . . . . 11
β’ ((π β Word (VtxβπΊ) β§ β¨β(πβ0)ββ© β
Word (VtxβπΊ)) β
((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ)) = π) |
25 | 23, 24 | syl 17 |
. . . . . . . . . 10
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β ((π ++ β¨β(πβ0)ββ©) prefix
(β―βπ)) = π) |
26 | 17, 25 | eqtr2d 2774 |
. . . . . . . . 9
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β π = ((π ++ β¨β(πβ0)ββ©) prefix π)) |
27 | 12, 26 | jca 513 |
. . . . . . . 8
β’ ((((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ π β β) β ((π ++ β¨β(πβ0)ββ©) β π· β§ π = ((π ++ β¨β(πβ0)ββ©) prefix π))) |
28 | 27 | ex 414 |
. . . . . . 7
β’ (((π β Word (VtxβπΊ) β§ (β―βπ) = π) β§ βπ β (0..^(π β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β (π β β β ((π ++ β¨β(πβ0)ββ©) β π· β§ π = ((π ++ β¨β(πβ0)ββ©) prefix π)))) |
29 | 6, 28 | syl 17 |
. . . . . 6
β’ (π β (π ClWWalksN πΊ) β (π β β β ((π ++ β¨β(πβ0)ββ©) β π· β§ π = ((π ++ β¨β(πβ0)ββ©) prefix π)))) |
30 | 29 | impcom 409 |
. . . . 5
β’ ((π β β β§ π β (π ClWWalksN πΊ)) β ((π ++ β¨β(πβ0)ββ©) β π· β§ π = ((π ++ β¨β(πβ0)ββ©) prefix π))) |
31 | | oveq1 7368 |
. . . . . 6
β’ (π₯ = (π ++ β¨β(πβ0)ββ©) β (π₯ prefix π) = ((π ++ β¨β(πβ0)ββ©) prefix π)) |
32 | 31 | rspceeqv 3599 |
. . . . 5
β’ (((π ++ β¨β(πβ0)ββ©) β
π· β§ π = ((π ++ β¨β(πβ0)ββ©) prefix π)) β βπ₯ β π· π = (π₯ prefix π)) |
33 | 30, 32 | syl 17 |
. . . 4
β’ ((π β β β§ π β (π ClWWalksN πΊ)) β βπ₯ β π· π = (π₯ prefix π)) |
34 | 1, 2 | clwwlkfv 29041 |
. . . . . . 7
β’ (π₯ β π· β (πΉβπ₯) = (π₯ prefix π)) |
35 | 34 | eqeq2d 2744 |
. . . . . 6
β’ (π₯ β π· β (π = (πΉβπ₯) β π = (π₯ prefix π))) |
36 | 35 | adantl 483 |
. . . . 5
β’ (((π β β β§ π β (π ClWWalksN πΊ)) β§ π₯ β π·) β (π = (πΉβπ₯) β π = (π₯ prefix π))) |
37 | 36 | rexbidva 3170 |
. . . 4
β’ ((π β β β§ π β (π ClWWalksN πΊ)) β (βπ₯ β π· π = (πΉβπ₯) β βπ₯ β π· π = (π₯ prefix π))) |
38 | 33, 37 | mpbird 257 |
. . 3
β’ ((π β β β§ π β (π ClWWalksN πΊ)) β βπ₯ β π· π = (πΉβπ₯)) |
39 | 38 | ralrimiva 3140 |
. 2
β’ (π β β β
βπ β (π ClWWalksN πΊ)βπ₯ β π· π = (πΉβπ₯)) |
40 | | dffo3 7056 |
. 2
β’ (πΉ:π·βontoβ(π ClWWalksN πΊ) β (πΉ:π·βΆ(π ClWWalksN πΊ) β§ βπ β (π ClWWalksN πΊ)βπ₯ β π· π = (πΉβπ₯))) |
41 | 3, 39, 40 | sylanbrc 584 |
1
β’ (π β β β πΉ:π·βontoβ(π ClWWalksN πΊ)) |