Step | Hyp | Ref
| Expression |
1 | | 1nn 12172 |
. . 3
β’ 1 β
β |
2 | | eqid 2733 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
3 | | eqid 2733 |
. . . 4
β’
(EdgβπΊ) =
(EdgβπΊ) |
4 | 2, 3 | isclwwlknx 29029 |
. . 3
β’ (1 β
β β (π β (1
ClWWalksN πΊ) β ((π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = 1))) |
5 | 1, 4 | ax-mp 5 |
. 2
β’ (π β (1 ClWWalksN πΊ) β ((π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = 1)) |
6 | | 3anass 1096 |
. . . 4
β’ ((π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β (π β Word (VtxβπΊ) β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)))) |
7 | | ral0 4474 |
. . . . . . . 8
β’
βπ β
β
{(πβπ), (πβ(π + 1))} β (EdgβπΊ) |
8 | | oveq1 7368 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
1 β ((β―βπ)
β 1) = (1 β 1)) |
9 | | 1m1e0 12233 |
. . . . . . . . . . . . 13
β’ (1
β 1) = 0 |
10 | 8, 9 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’
((β―βπ) =
1 β ((β―βπ)
β 1) = 0) |
11 | 10 | oveq2d 7377 |
. . . . . . . . . . 11
β’
((β―βπ) =
1 β (0..^((β―βπ) β 1)) = (0..^0)) |
12 | | fzo0 13605 |
. . . . . . . . . . 11
β’ (0..^0) =
β
|
13 | 11, 12 | eqtrdi 2789 |
. . . . . . . . . 10
β’
((β―βπ) =
1 β (0..^((β―βπ) β 1)) = β
) |
14 | 13 | raleqdv 3312 |
. . . . . . . . 9
β’
((β―βπ) =
1 β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β β
{(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β β
{(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
16 | 7, 15 | mpbiri 258 |
. . . . . . 7
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) |
17 | 16 | biantrurd 534 |
. . . . . 6
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
({(lastSβπ), (πβ0)} β
(EdgβπΊ) β
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)))) |
18 | | lsw1 14464 |
. . . . . . . . . 10
β’ ((π β Word (VtxβπΊ) β§ (β―βπ) = 1) β (lastSβπ) = (πβ0)) |
19 | 18 | ancoms 460 |
. . . . . . . . 9
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
(lastSβπ) = (πβ0)) |
20 | 19 | preq1d 4704 |
. . . . . . . 8
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
{(lastSβπ), (πβ0)} = {(πβ0), (πβ0)}) |
21 | | dfsn2 4603 |
. . . . . . . 8
β’ {(πβ0)} = {(πβ0), (πβ0)} |
22 | 20, 21 | eqtr4di 2791 |
. . . . . . 7
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
{(lastSβπ), (πβ0)} = {(πβ0)}) |
23 | 22 | eleq1d 2819 |
. . . . . 6
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
({(lastSβπ), (πβ0)} β
(EdgβπΊ) β
{(πβ0)} β
(EdgβπΊ))) |
24 | 17, 23 | bitr3d 281 |
. . . . 5
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ)) β
((βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β {(πβ0)} β (EdgβπΊ))) |
25 | 24 | pm5.32da 580 |
. . . 4
β’
((β―βπ) =
1 β ((π β Word
(VtxβπΊ) β§
(βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ))) β (π β Word (VtxβπΊ) β§ {(πβ0)} β (EdgβπΊ)))) |
26 | 6, 25 | bitrid 283 |
. . 3
β’
((β―βπ) =
1 β ((π β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β (π β Word (VtxβπΊ) β§ {(πβ0)} β (EdgβπΊ)))) |
27 | 26 | pm5.32ri 577 |
. 2
β’ (((π β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β§ {(lastSβπ), (πβ0)} β (EdgβπΊ)) β§ (β―βπ) = 1) β ((π β Word (VtxβπΊ) β§ {(πβ0)} β (EdgβπΊ)) β§ (β―βπ) = 1)) |
28 | | 3anass 1096 |
. . 3
β’
(((β―βπ)
= 1 β§ π β Word
(VtxβπΊ) β§ {(πβ0)} β
(EdgβπΊ)) β
((β―βπ) = 1
β§ (π β Word
(VtxβπΊ) β§ {(πβ0)} β
(EdgβπΊ)))) |
29 | | ancom 462 |
. . 3
β’
(((β―βπ)
= 1 β§ (π β Word
(VtxβπΊ) β§ {(πβ0)} β
(EdgβπΊ))) β
((π β Word
(VtxβπΊ) β§ {(πβ0)} β
(EdgβπΊ)) β§
(β―βπ) =
1)) |
30 | 28, 29 | bitr2i 276 |
. 2
β’ (((π β Word (VtxβπΊ) β§ {(πβ0)} β (EdgβπΊ)) β§ (β―βπ) = 1) β
((β―βπ) = 1
β§ π β Word
(VtxβπΊ) β§ {(πβ0)} β
(EdgβπΊ))) |
31 | 5, 27, 30 | 3bitri 297 |
1
β’ (π β (1 ClWWalksN πΊ) β ((β―βπ) = 1 β§ π β Word (VtxβπΊ) β§ {(πβ0)} β (EdgβπΊ))) |