Step | Hyp | Ref
| Expression |
1 | | nnnn0 12428 |
. . . . 5
β’ (π β β β π β
β0) |
2 | | ccatws1lenp1b 14518 |
. . . . 5
β’ ((π β Word π β§ π β β0) β
((β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1) β
(β―βπ) = π)) |
3 | 1, 2 | sylan2 594 |
. . . 4
β’ ((π β Word π β§ π β β) β
((β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1) β
(β―βπ) = π)) |
4 | 3 | anbi2d 630 |
. . 3
β’ ((π β Word π β§ π β β) β (((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1)) β ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―βπ) = π))) |
5 | | simpl 484 |
. . . . . . 7
β’ ((π β Word π β§ π β β) β π β Word π) |
6 | | eleq1 2822 |
. . . . . . . . . 10
β’
((β―βπ) =
π β
((β―βπ) β
β β π β
β)) |
7 | | len0nnbi 14448 |
. . . . . . . . . . 11
β’ (π β Word π β (π β β
β (β―βπ) β
β)) |
8 | 7 | biimprcd 250 |
. . . . . . . . . 10
β’
((β―βπ)
β β β (π
β Word π β π β β
)) |
9 | 6, 8 | syl6bir 254 |
. . . . . . . . 9
β’
((β―βπ) =
π β (π β β β (π β Word π β π β β
))) |
10 | 9 | com13 88 |
. . . . . . . 8
β’ (π β Word π β (π β β β ((β―βπ) = π β π β β
))) |
11 | 10 | imp31 419 |
. . . . . . 7
β’ (((π β Word π β§ π β β) β§ (β―βπ) = π) β π β β
) |
12 | | clwwlkwwlksb.v |
. . . . . . . 8
β’ π = (VtxβπΊ) |
13 | 12 | clwwlkwwlksb 29047 |
. . . . . . 7
β’ ((π β Word π β§ π β β
) β (π β (ClWWalksβπΊ) β (π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ))) |
14 | 5, 11, 13 | syl2an2r 684 |
. . . . . 6
β’ (((π β Word π β§ π β β) β§ (β―βπ) = π) β (π β (ClWWalksβπΊ) β (π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ))) |
15 | 14 | bicomd 222 |
. . . . 5
β’ (((π β Word π β§ π β β) β§ (β―βπ) = π) β ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β
π β
(ClWWalksβπΊ))) |
16 | 15 | ex 414 |
. . . 4
β’ ((π β Word π β§ π β β) β
((β―βπ) = π β ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β
π β
(ClWWalksβπΊ)))) |
17 | 16 | pm5.32rd 579 |
. . 3
β’ ((π β Word π β§ π β β) β (((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―βπ) = π) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π))) |
18 | 4, 17 | bitrd 279 |
. 2
β’ ((π β Word π β§ π β β) β (((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1)) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π))) |
19 | 1 | adantl 483 |
. . 3
β’ ((π β Word π β§ π β β) β π β
β0) |
20 | | iswwlksn 28832 |
. . 3
β’ (π β β0
β ((π ++
β¨β(πβ0)ββ©) β (π WWalksN πΊ) β ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1)))) |
21 | 19, 20 | syl 17 |
. 2
β’ ((π β Word π β§ π β β) β ((π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ) β ((π ++ β¨β(πβ0)ββ©) β
(WWalksβπΊ) β§
(β―β(π ++
β¨β(πβ0)ββ©)) = (π + 1)))) |
22 | | isclwwlkn 29020 |
. . 3
β’ (π β (π ClWWalksN πΊ) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π)) |
23 | 22 | a1i 11 |
. 2
β’ ((π β Word π β§ π β β) β (π β (π ClWWalksN πΊ) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π))) |
24 | 18, 21, 23 | 3bitr4rd 312 |
1
β’ ((π β Word π β§ π β β) β (π β (π ClWWalksN πΊ) β (π ++ β¨β(πβ0)ββ©) β (π WWalksN πΊ))) |