| Step | Hyp | Ref
| Expression |
|---|
| 1 | | clwwlknonel.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
| 2 | | clwwlknonel.e |
. . . . . . 7
β’ πΈ = (EdgβπΊ) |
| 3 | 1, 2 | isclwwlk 29746 |
. . . . . 6
β’ (π β (ClWWalksβπΊ) β ((π β Word π β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)) |
| 4 | | simpl 482 |
. . . . . . . . . . . . 13
β’
(((β―βπ)
= π β§ π = β
) β (β―βπ) = π) |
| 5 | | fveq2 6885 |
. . . . . . . . . . . . . . 15
β’ (π = β
β
(β―βπ) =
(β―ββ
)) |
| 6 | | hash0 14332 |
. . . . . . . . . . . . . . 15
β’
(β―ββ
) = 0 |
| 7 | 5, 6 | eqtrdi 2782 |
. . . . . . . . . . . . . 14
β’ (π = β
β
(β―βπ) =
0) |
| 8 | 7 | adantl 481 |
. . . . . . . . . . . . 13
β’
(((β―βπ)
= π β§ π = β
) β (β―βπ) = 0) |
| 9 | 4, 8 | eqtr3d 2768 |
. . . . . . . . . . . 12
β’
(((β―βπ)
= π β§ π = β
) β π = 0) |
| 10 | 9 | ex 412 |
. . . . . . . . . . 11
β’
((β―βπ) =
π β (π = β
β π = 0)) |
| 11 | 10 | necon3d 2955 |
. . . . . . . . . 10
β’
((β―βπ) =
π β (π β 0 β π β β
)) |
| 12 | 11 | impcom 407 |
. . . . . . . . 9
β’ ((π β 0 β§
(β―βπ) = π) β π β β
) |
| 13 | 12 | biantrud 531 |
. . . . . . . 8
β’ ((π β 0 β§
(β―βπ) = π) β (π β Word π β (π β Word π β§ π β β
))) |
| 14 | 13 | bicomd 222 |
. . . . . . 7
β’ ((π β 0 β§
(β―βπ) = π) β ((π β Word π β§ π β β
) β π β Word π)) |
| 15 | 14 | 3anbi1d 1436 |
. . . . . 6
β’ ((π β 0 β§
(β―βπ) = π) β (((π β Word π β§ π β β
) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β (π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
| 16 | 3, 15 | bitrid 283 |
. . . . 5
β’ ((π β 0 β§
(β―βπ) = π) β (π β (ClWWalksβπΊ) β (π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ))) |
| 17 | 16 | a1d 25 |
. . . 4
β’ ((π β 0 β§
(β―βπ) = π) β ((πβ0) = π β (π β (ClWWalksβπΊ) β (π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)))) |
| 18 | 17 | expimpd 453 |
. . 3
β’ (π β 0 β
(((β―βπ) = π β§ (πβ0) = π) β (π β (ClWWalksβπΊ) β (π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ)))) |
| 19 | 18 | pm5.32rd 577 |
. 2
β’ (π β 0 β ((π β (ClWWalksβπΊ) β§ ((β―βπ) = π β§ (πβ0) = π)) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ ((β―βπ) = π β§ (πβ0) = π)))) |
| 20 | | isclwwlknon 29853 |
. . 3
β’ (π β (π(ClWWalksNOnβπΊ)π) β (π β (π ClWWalksN πΊ) β§ (πβ0) = π)) |
| 21 | | isclwwlkn 29789 |
. . . 4
β’ (π β (π ClWWalksN πΊ) β (π β (ClWWalksβπΊ) β§ (β―βπ) = π)) |
| 22 | 21 | anbi1i 623 |
. . 3
β’ ((π β (π ClWWalksN πΊ) β§ (πβ0) = π) β ((π β (ClWWalksβπΊ) β§ (β―βπ) = π) β§ (πβ0) = π)) |
| 23 | | anass 468 |
. . 3
β’ (((π β (ClWWalksβπΊ) β§ (β―βπ) = π) β§ (πβ0) = π) β (π β (ClWWalksβπΊ) β§ ((β―βπ) = π β§ (πβ0) = π))) |
| 24 | 20, 22, 23 | 3bitri 297 |
. 2
β’ (π β (π(ClWWalksNOnβπΊ)π) β (π β (ClWWalksβπΊ) β§ ((β―βπ) = π β§ (πβ0) = π))) |
| 25 | | 3anass 1092 |
. 2
β’ (((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π β§ (πβ0) = π) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ ((β―βπ) = π β§ (πβ0) = π))) |
| 26 | 19, 24, 25 | 3bitr4g 314 |
1
β’ (π β 0 β (π β (π(ClWWalksNOnβπΊ)π) β ((π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ {(lastSβπ), (πβ0)} β πΈ) β§ (β―βπ) = π β§ (πβ0) = π))) |
