Step | Hyp | Ref
| Expression |
1 | | wlkcpr 28883 |
. . 3
β’ (π β (WalksβπΊ) β (1st
βπ)(WalksβπΊ)(2nd βπ)) |
2 | | eqid 2732 |
. . . . . 6
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
3 | 2 | wlkf 28868 |
. . . . 5
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (1st βπ) β Word dom
(iEdgβπΊ)) |
4 | | eqid 2732 |
. . . . . 6
β’
(VtxβπΊ) =
(VtxβπΊ) |
5 | 4 | wlkp 28870 |
. . . . 5
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (2nd βπ):(0...(β―β(1st
βπ)))βΆ(VtxβπΊ)) |
6 | 3, 5 | jca 512 |
. . . 4
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β ((1st βπ) β Word dom
(iEdgβπΊ) β§
(2nd βπ):(0...(β―β(1st
βπ)))βΆ(VtxβπΊ))) |
7 | | feq3 6700 |
. . . . . . 7
β’
((VtxβπΊ) =
β
β ((2nd βπ):(0...(β―β(1st
βπ)))βΆ(VtxβπΊ) β (2nd βπ):(0...(β―β(1st
βπ)))βΆβ
)) |
8 | | f00 6773 |
. . . . . . 7
β’
((2nd βπ):(0...(β―β(1st
βπ)))βΆβ
β ((2nd βπ) = β
β§
(0...(β―β(1st βπ))) = β
)) |
9 | 7, 8 | bitrdi 286 |
. . . . . 6
β’
((VtxβπΊ) =
β
β ((2nd βπ):(0...(β―β(1st
βπ)))βΆ(VtxβπΊ) β ((2nd βπ) = β
β§
(0...(β―β(1st βπ))) = β
))) |
10 | | 0z 12568 |
. . . . . . . . . . . . 13
β’ 0 β
β€ |
11 | | nn0z 12582 |
. . . . . . . . . . . . 13
β’
((β―β(1st βπ)) β β0 β
(β―β(1st βπ)) β β€) |
12 | | fzn 13516 |
. . . . . . . . . . . . 13
β’ ((0
β β€ β§ (β―β(1st βπ)) β β€) β
((β―β(1st βπ)) < 0 β
(0...(β―β(1st βπ))) = β
)) |
13 | 10, 11, 12 | sylancr 587 |
. . . . . . . . . . . 12
β’
((β―β(1st βπ)) β β0 β
((β―β(1st βπ)) < 0 β
(0...(β―β(1st βπ))) = β
)) |
14 | | nn0nlt0 12497 |
. . . . . . . . . . . . 13
β’
((β―β(1st βπ)) β β0 β Β¬
(β―β(1st βπ)) < 0) |
15 | 14 | pm2.21d 121 |
. . . . . . . . . . . 12
β’
((β―β(1st βπ)) β β0 β
((β―β(1st βπ)) < 0 β (1st
βπ) =
β
)) |
16 | 13, 15 | sylbird 259 |
. . . . . . . . . . 11
β’
((β―β(1st βπ)) β β0 β
((0...(β―β(1st βπ))) = β
β (1st
βπ) =
β
)) |
17 | 16 | com12 32 |
. . . . . . . . . 10
β’
((0...(β―β(1st βπ))) = β
β
((β―β(1st βπ)) β β0 β
(1st βπ) =
β
)) |
18 | 17 | adantl 482 |
. . . . . . . . 9
β’
(((2nd βπ) = β
β§
(0...(β―β(1st βπ))) = β
) β
((β―β(1st βπ)) β β0 β
(1st βπ) =
β
)) |
19 | | lencl 14482 |
. . . . . . . . 9
β’
((1st βπ) β Word dom (iEdgβπΊ) β
(β―β(1st βπ)) β
β0) |
20 | 18, 19 | impel 506 |
. . . . . . . 8
β’
((((2nd βπ) = β
β§
(0...(β―β(1st βπ))) = β
) β§ (1st
βπ) β Word dom
(iEdgβπΊ)) β
(1st βπ) =
β
) |
21 | | simpll 765 |
. . . . . . . 8
β’
((((2nd βπ) = β
β§
(0...(β―β(1st βπ))) = β
) β§ (1st
βπ) β Word dom
(iEdgβπΊ)) β
(2nd βπ) =
β
) |
22 | 20, 21 | jca 512 |
. . . . . . 7
β’
((((2nd βπ) = β
β§
(0...(β―β(1st βπ))) = β
) β§ (1st
βπ) β Word dom
(iEdgβπΊ)) β
((1st βπ)
= β
β§ (2nd βπ) = β
)) |
23 | 22 | ex 413 |
. . . . . 6
β’
(((2nd βπ) = β
β§
(0...(β―β(1st βπ))) = β
) β ((1st
βπ) β Word dom
(iEdgβπΊ) β
((1st βπ)
= β
β§ (2nd βπ) = β
))) |
24 | 9, 23 | syl6bi 252 |
. . . . 5
β’
((VtxβπΊ) =
β
β ((2nd βπ):(0...(β―β(1st
βπ)))βΆ(VtxβπΊ) β ((1st βπ) β Word dom
(iEdgβπΊ) β
((1st βπ)
= β
β§ (2nd βπ) = β
)))) |
25 | 24 | impcomd 412 |
. . . 4
β’
((VtxβπΊ) =
β
β (((1st βπ) β Word dom (iEdgβπΊ) β§ (2nd
βπ):(0...(β―β(1st
βπ)))βΆ(VtxβπΊ)) β ((1st βπ) = β
β§
(2nd βπ) =
β
))) |
26 | 6, 25 | syl5 34 |
. . 3
β’
((VtxβπΊ) =
β
β ((1st βπ)(WalksβπΊ)(2nd βπ) β ((1st βπ) = β
β§
(2nd βπ) =
β
))) |
27 | 1, 26 | biimtrid 241 |
. 2
β’
((VtxβπΊ) =
β
β (π β
(WalksβπΊ) β
((1st βπ)
= β
β§ (2nd βπ) = β
))) |
28 | 27 | imp 407 |
1
β’
(((VtxβπΊ) =
β
β§ π β
(WalksβπΊ)) β
((1st βπ)
= β
β§ (2nd βπ) = β
)) |