Step | Hyp | Ref
| Expression |
1 | | wlkn0 28867 |
. 2
β’ (πΉ(WalksβπΊ)π β π β β
) |
2 | | eqid 2732 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
3 | | eqid 2732 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
4 | 2, 3 | upgriswlk 28887 |
. . 3
β’ (πΊ β UPGraph β (πΉ(WalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
5 | | simpr 485 |
. . . . . 6
β’ (((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β§ π β β
) β π β β
) |
6 | | ffz0iswrd 14487 |
. . . . . . . 8
β’ (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β π β Word (VtxβπΊ)) |
7 | 6 | 3ad2ant2 1134 |
. . . . . . 7
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β π β Word (VtxβπΊ)) |
8 | 7 | ad2antlr 725 |
. . . . . 6
β’ (((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β§ π β β
) β π β Word (VtxβπΊ)) |
9 | | upgruhgr 28351 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β UPGraph β πΊ β
UHGraph) |
10 | 3 | uhgrfun 28315 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β UHGraph β Fun
(iEdgβπΊ)) |
11 | | funfn 6575 |
. . . . . . . . . . . . . . . . . . 19
β’ (Fun
(iEdgβπΊ) β
(iEdgβπΊ) Fn dom
(iEdgβπΊ)) |
12 | 11 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’ (Fun
(iEdgβπΊ) β
(iEdgβπΊ) Fn dom
(iEdgβπΊ)) |
13 | 9, 10, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β UPGraph β
(iEdgβπΊ) Fn dom
(iEdgβπΊ)) |
14 | 13 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΊ β UPGraph) β§ π β (0..^(β―βπΉ))) β (iEdgβπΊ) Fn dom (iEdgβπΊ)) |
15 | | wrdsymbcl 14473 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π β
(0..^(β―βπΉ)))
β (πΉβπ) β dom (iEdgβπΊ)) |
16 | 15 | ad4ant14 750 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΊ β UPGraph) β§ π β (0..^(β―βπΉ))) β (πΉβπ) β dom (iEdgβπΊ)) |
17 | | fnfvelrn 7079 |
. . . . . . . . . . . . . . . 16
β’
(((iEdgβπΊ) Fn
dom (iEdgβπΊ) β§
(πΉβπ) β dom (iEdgβπΊ)) β ((iEdgβπΊ)β(πΉβπ)) β ran (iEdgβπΊ)) |
18 | 14, 16, 17 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΊ β UPGraph) β§ π β (0..^(β―βπΉ))) β ((iEdgβπΊ)β(πΉβπ)) β ran (iEdgβπΊ)) |
19 | | edgval 28298 |
. . . . . . . . . . . . . . 15
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
20 | 18, 19 | eleqtrrdi 2844 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΊ β UPGraph) β§ π β (0..^(β―βπΉ))) β ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) |
21 | | eleq1 2821 |
. . . . . . . . . . . . . . 15
β’ ({(πβπ), (πβ(π + 1))} = ((iEdgβπΊ)β(πΉβπ)) β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ))) |
22 | 21 | eqcoms 2740 |
. . . . . . . . . . . . . 14
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β ({(πβπ), (πβ(π + 1))} β (EdgβπΊ) β ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ))) |
23 | 20, 22 | syl5ibrcom 246 |
. . . . . . . . . . . . 13
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΊ β UPGraph) β§ π β (0..^(β―βπΉ))) β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β {(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
24 | 23 | ralimdva 3167 |
. . . . . . . . . . . 12
β’ (((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ πΊ β UPGraph) β (βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
25 | 24 | ex 413 |
. . . . . . . . . . 11
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (πΊ β UPGraph β (βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)))) |
26 | 25 | com23 86 |
. . . . . . . . . 10
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))} β (πΊ β UPGraph β βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)))) |
27 | 26 | 3impia 1117 |
. . . . . . . . 9
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (πΊ β UPGraph β βπ β
(0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
28 | 27 | impcom 408 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) |
29 | | lencl 14479 |
. . . . . . . . . . . . . 14
β’ (πΉ β Word dom
(iEdgβπΊ) β
(β―βπΉ) β
β0) |
30 | | ffz0hash 14402 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπΉ)
β β0 β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (β―βπ) = ((β―βπΉ) + 1)) |
31 | 30 | ex 413 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ)
β β0 β (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β (β―βπ) = ((β―βπΉ) + 1))) |
32 | | oveq1 7412 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
((β―βπΉ) + 1)
β ((β―βπ)
β 1) = (((β―βπΉ) + 1) β 1)) |
33 | | nn0cn 12478 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπΉ)
β β0 β (β―βπΉ) β β) |
34 | | pncan1 11634 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπΉ)
β β β (((β―βπΉ) + 1) β 1) = (β―βπΉ)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπΉ)
β β0 β (((β―βπΉ) + 1) β 1) = (β―βπΉ)) |
36 | 32, 35 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπΉ)
β β0 β§ (β―βπ) = ((β―βπΉ) + 1)) β ((β―βπ) β 1) =
(β―βπΉ)) |
37 | 36 | ex 413 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ)
β β0 β ((β―βπ) = ((β―βπΉ) + 1) β ((β―βπ) β 1) =
(β―βπΉ))) |
38 | 31, 37 | syld 47 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ)
β β0 β (π:(0...(β―βπΉ))βΆ(VtxβπΊ) β ((β―βπ) β 1) = (β―βπΉ))) |
39 | 29, 38 | syl 17 |
. . . . . . . . . . . . 13
β’ (πΉ β Word dom
(iEdgβπΊ) β
(π:(0...(β―βπΉ))βΆ(VtxβπΊ) β ((β―βπ) β 1) = (β―βπΉ))) |
40 | 39 | imp 407 |
. . . . . . . . . . . 12
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β ((β―βπ) β 1) =
(β―βπΉ)) |
41 | 40 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β
(0..^((β―βπ)
β 1)) = (0..^(β―βπΉ))) |
42 | 41 | raleqdv 3325 |
. . . . . . . . . 10
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
43 | 42 | 3adant3 1132 |
. . . . . . . . 9
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
44 | 43 | adantl 482 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ) β βπ β (0..^(β―βπΉ)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
45 | 28, 44 | mpbird 256 |
. . . . . . 7
β’ ((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) |
46 | 45 | adantr 481 |
. . . . . 6
β’ (((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β§ π β β
) β βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) |
47 | | eqid 2732 |
. . . . . . 7
β’
(EdgβπΊ) =
(EdgβπΊ) |
48 | 2, 47 | iswwlks 29079 |
. . . . . 6
β’ (π β (WWalksβπΊ) β (π β β
β§ π β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
49 | 5, 8, 46, 48 | syl3anbrc 1343 |
. . . . 5
β’ (((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β§ π β β
) β π β (WWalksβπΊ)) |
50 | 49 | ex 413 |
. . . 4
β’ ((πΊ β UPGraph β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) β (π β β
β π β (WWalksβπΊ))) |
51 | 50 | ex 413 |
. . 3
β’ (πΊ β UPGraph β ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β (π β β
β π β (WWalksβπΊ)))) |
52 | 4, 51 | sylbid 239 |
. 2
β’ (πΊ β UPGraph β (πΉ(WalksβπΊ)π β (π β β
β π β (WWalksβπΊ)))) |
53 | 1, 52 | mpdi 45 |
1
β’ (πΊ β UPGraph β (πΉ(WalksβπΊ)π β π β (WWalksβπΊ))) |