Step | Hyp | Ref
| Expression |
1 | | wlkv 28907 |
. 2
β’ (πΉ(WalksβπΊ)π β (πΊ β V β§ πΉ β V β§ π β V)) |
2 | | eqid 2732 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
3 | | eqid 2732 |
. . . 4
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
4 | 2, 3 | iswlk 28905 |
. . 3
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(WalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
5 | | fvex 6904 |
. . . . . . 7
β’ (πΌβ(πΉβ(π β 1))) β V |
6 | 5 | inex1 5317 |
. . . . . 6
β’ ((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))) β V |
7 | | fzo0ss1 13664 |
. . . . . . . . . . . 12
β’
(1..^(β―βπΉ)) β (0..^(β―βπΉ)) |
8 | 7 | sseli 3978 |
. . . . . . . . . . 11
β’ (π β
(1..^(β―βπΉ))
β π β
(0..^(β―βπΉ))) |
9 | | wkslem1 28902 |
. . . . . . . . . . . 12
β’ (π = π β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
10 | 9 | rspcv 3608 |
. . . . . . . . . . 11
β’ (π β
(0..^(β―βπΉ))
β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
11 | 8, 10 | syl 17 |
. . . . . . . . . 10
β’ (π β
(1..^(β―βπΉ))
β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
12 | 11 | imp 407 |
. . . . . . . . 9
β’ ((π β
(1..^(β―βπΉ))
β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) |
13 | | elfzofz 13650 |
. . . . . . . . . . 11
β’ (π β
(1..^(β―βπΉ))
β π β
(1...(β―βπΉ))) |
14 | | fz1fzo0m1 13682 |
. . . . . . . . . . 11
β’ (π β
(1...(β―βπΉ))
β (π β 1) β
(0..^(β―βπΉ))) |
15 | | wkslem1 28902 |
. . . . . . . . . . . 12
β’ (π = (π β 1) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))))) |
16 | 15 | rspcv 3608 |
. . . . . . . . . . 11
β’ ((π β 1) β
(0..^(β―βπΉ))
β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))))) |
17 | 13, 14, 16 | 3syl 18 |
. . . . . . . . . 10
β’ (π β
(1..^(β―βπΉ))
β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))))) |
18 | 17 | imp 407 |
. . . . . . . . 9
β’ ((π β
(1..^(β―βπΉ))
β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1))))) |
19 | | df-ifp 1062 |
. . . . . . . . . . . 12
β’
(if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β (((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
20 | | elfzoelz 13634 |
. . . . . . . . . . . . . . 15
β’ (π β
(1..^(β―βπΉ))
β π β
β€) |
21 | | zcn 12565 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β π β
β) |
22 | | eqidd 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π β 1) = (π β 1)) |
23 | | npcan1 11641 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π β 1) + 1) = π) |
24 | | wkslem2 28903 |
. . . . . . . . . . . . . . . 16
β’ (((π β 1) = (π β 1) β§ ((π β 1) + 1) = π) β (if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β if-((πβ(π β 1)) = (πβπ), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))))) |
25 | 22, 23, 24 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (π β β β
(if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β if-((πβ(π β 1)) = (πβπ), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))))) |
26 | 20, 21, 25 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β
(1..^(β―βπΉ))
β (if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β if-((πβ(π β 1)) = (πβπ), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))))) |
27 | | df-ifp 1062 |
. . . . . . . . . . . . . . 15
β’
(if-((πβ(π β 1)) = (πβπ), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β¨ (Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))))) |
28 | | sneq 4638 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πβ(π β 1)) = (πβπ) β {(πβ(π β 1))} = {(πβπ)}) |
29 | 28 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβ(π β 1)) = (πβπ) β (((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))} β ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)})) |
30 | | fvex 6904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πβπ) β V |
31 | 30 | snid 4664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πβπ) β {(πβπ)} |
32 | | wlk1walk.i |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ πΌ = (iEdgβπΊ) |
33 | 32 | fveq1i 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΌβ(πΉβ(π β 1))) = ((iEdgβπΊ)β(πΉβ(π β 1))) |
34 | 33 | eleq2i 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβπ) β (πΌβ(πΉβ(π β 1))) β (πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1)))) |
35 | | eleq2 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)} β ((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β (πβπ) β {(πβπ)})) |
36 | 34, 35 | bitrid 282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β (πβπ) β {(πβπ)})) |
37 | 31, 36 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)} β (πβπ) β (πΌβ(πΉβ(π β 1)))) |
38 | | eleq2 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β (πβπ) β {(πβπ)})) |
39 | 31, 38 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β (πβπ) β ((iEdgβπΊ)β(πΉβπ))) |
40 | 32 | fveq1i 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΌβ(πΉβπ)) = ((iEdgβπΊ)β(πΉβπ)) |
41 | 39, 40 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β (πβπ) β (πΌβ(πΉβπ))) |
42 | 37, 41 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)} β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))) |
43 | 42 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)} β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
44 | 29, 43 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβ(π β 1)) = (πβπ) β (((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))} β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))))) |
45 | 44 | imp 407 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
46 | 45 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
48 | | fvex 6904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πβ(π + 1)) β V |
49 | 30, 48 | prss 4823 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β§ (πβ(π + 1)) β ((iEdgβπΊ)β(πΉβπ))) β {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) |
50 | 32 | eqcomi 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(iEdgβπΊ) =
πΌ |
51 | 50 | fveq1i 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((iEdgβπΊ)β(πΉβπ)) = (πΌβ(πΉβπ)) |
52 | 51 | eleq2i 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β (πβπ) β (πΌβ(πΉβπ))) |
53 | 52 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β (πβπ) β (πΌβ(πΉβπ))) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β§ (πβ(π + 1)) β ((iEdgβπΊ)β(πΉβπ))) β (πβπ) β (πΌβ(πΉβπ))) |
55 | 49, 54 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ({(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)) β (πβπ) β (πΌβ(πΉβπ))) |
56 | 37, 55 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)} β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))) |
57 | 56 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβπ)} β ({(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
58 | 29, 57 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβ(π β 1)) = (πβπ) β (((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))} β ({(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))))) |
59 | 58 | imp 407 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β ({(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
60 | 59 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
β’ ({(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)) β (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((Β¬
(πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
62 | 47, 61 | jaoi 855 |
. . . . . . . . . . . . . . . . 17
β’ ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
63 | 62 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ (((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
64 | | fvex 6904 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πβ(π β 1)) β V |
65 | 64, 30 | prss 4823 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πβ(π β 1)) β ((iEdgβπΊ)β(πΉβ(π β 1))) β§ (πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1)))) β {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) |
66 | 50 | fveq1i 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((iEdgβπΊ)β(πΉβ(π β 1))) = (πΌβ(πΉβ(π β 1))) |
67 | 66 | eleq2i 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β (πβπ) β (πΌβ(πΉβ(π β 1)))) |
68 | 67 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β (πβπ) β (πΌβ(πΉβ(π β 1)))) |
69 | 40 | eleq2i 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβπ) β (πΌβ(πΉβπ)) β (πβπ) β ((iEdgβπΊ)β(πΉβπ))) |
70 | 69, 38 | bitrid 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβπ)) β (πβπ) β {(πβπ)})) |
71 | 31, 70 | mpbiri 257 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β (πβπ) β (πΌβ(πΉβπ))) |
72 | 68, 71 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))) |
73 | 72 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
74 | 73 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πβ(π β 1)) β ((iEdgβπΊ)β(πΉβ(π β 1))) β§ (πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1)))) β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
75 | 65, 74 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ({(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1))) β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Β¬
(πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
77 | 76 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
β’
(((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
78 | 77 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β ((Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
79 | 67, 52 | anbi12i 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β§ (πβπ) β ((iEdgβπΊ)β(πΉβπ))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))) |
80 | 79 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β§ (πβπ) β ((iEdgβπΊ)β(πΉβπ))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))) |
81 | 80 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1))) β ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πβ(π β 1)) β ((iEdgβπΊ)β(πΉβ(π β 1))) β§ (πβπ) β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
83 | 65, 82 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ({(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1))) β ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
84 | 83 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Β¬
(πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
85 | 84 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β ((Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβπ) β ((iEdgβπΊ)β(πΉβπ)) β§ (πβ(π + 1)) β ((iEdgβπΊ)β(πΉβπ))) β ((Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
87 | 49, 86 | sylbir 234 |
. . . . . . . . . . . . . . . . . . 19
β’ ({(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)) β ((Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((Β¬
(πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
89 | 78, 88 | jaoi 855 |
. . . . . . . . . . . . . . . . 17
β’ ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
90 | 89 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ ((Β¬
(πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
91 | 63, 90 | jaoi 855 |
. . . . . . . . . . . . . . 15
β’ ((((πβ(π β 1)) = (πβπ) β§ ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}) β¨ (Β¬ (πβ(π β 1)) = (πβπ) β§ {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1))))) β ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
92 | 27, 91 | sylbi 216 |
. . . . . . . . . . . . . 14
β’
(if-((πβ(π β 1)) = (πβπ), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβπ)} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))))) |
93 | 26, 92 | syl6bi 252 |
. . . . . . . . . . . . 13
β’ (π β
(1..^(β―βπΉ))
β (if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))))) |
94 | 93 | com3r 87 |
. . . . . . . . . . . 12
β’ ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β (π β (1..^(β―βπΉ)) β (if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))))) |
95 | 19, 94 | sylbi 216 |
. . . . . . . . . . 11
β’
(if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β (π β (1..^(β―βπΉ)) β (if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))))) |
96 | 95 | com12 32 |
. . . . . . . . . 10
β’ (π β
(1..^(β―βπΉ))
β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β (if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))))) |
97 | 96 | adantr 481 |
. . . . . . . . 9
β’ ((π β
(1..^(β―βπΉ))
β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β (if-((πβ(π β 1)) = (πβ((π β 1) + 1)), ((iEdgβπΊ)β(πΉβ(π β 1))) = {(πβ(π β 1))}, {(πβ(π β 1)), (πβ((π β 1) + 1))} β ((iEdgβπΊ)β(πΉβ(π β 1)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))))) |
98 | 12, 18, 97 | mp2d 49 |
. . . . . . . 8
β’ ((π β
(1..^(β―βπΉ))
β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))) |
99 | 98 | ancoms 459 |
. . . . . . 7
β’
((βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β§ π β (1..^(β―βπΉ))) β ((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ)))) |
100 | | inelcm 4464 |
. . . . . . 7
β’ (((πβπ) β (πΌβ(πΉβ(π β 1))) β§ (πβπ) β (πΌβ(πΉβπ))) β ((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))) β β
) |
101 | 99, 100 | syl 17 |
. . . . . 6
β’
((βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β§ π β (1..^(β―βπΉ))) β ((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))) β β
) |
102 | | hashge1 14351 |
. . . . . 6
β’ ((((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))) β V β§ ((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))) β β
) β 1 β€
(β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))))) |
103 | 6, 101, 102 | sylancr 587 |
. . . . 5
β’
((βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β§ π β (1..^(β―βπΉ))) β 1 β€ (β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))))) |
104 | 103 | ralrimiva 3146 |
. . . 4
β’
(βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β βπ β (1..^(β―βπΉ))1 β€ (β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))))) |
105 | 104 | 3ad2ant3 1135 |
. . 3
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β βπ β (1..^(β―βπΉ))1 β€ (β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))))) |
106 | 4, 105 | syl6bi 252 |
. 2
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(WalksβπΊ)π β βπ β (1..^(β―βπΉ))1 β€ (β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ)))))) |
107 | 1, 106 | mpcom 38 |
1
β’ (πΉ(WalksβπΊ)π β βπ β (1..^(β―βπΉ))1 β€ (β―β((πΌβ(πΉβ(π β 1))) β© (πΌβ(πΉβπ))))) |