Step | Hyp | Ref
| Expression |
1 | | wlkv 29136 |
. . . . 5
β’ (πΉ(WalksβπΊ)π β (πΊ β V β§ πΉ β V β§ π β V)) |
2 | | simp3l 1199 |
. . . . . . . . 9
β’ ((πΊ β V β§ πΉ(WalksβπΊ)π β§ (Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1)))) β Fun (iEdgβπΊ)) |
3 | | simp2 1135 |
. . . . . . . . 9
β’ ((πΊ β V β§ πΉ(WalksβπΊ)π β§ (Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1)))) β πΉ(WalksβπΊ)π) |
4 | | c0ex 11212 |
. . . . . . . . . . . . 13
β’ 0 β
V |
5 | 4 | snid 4663 |
. . . . . . . . . . . 12
β’ 0 β
{0} |
6 | | oveq2 7419 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
1 β (0..^(β―βπΉ)) = (0..^1)) |
7 | | fzo01 13718 |
. . . . . . . . . . . . 13
β’ (0..^1) =
{0} |
8 | 6, 7 | eqtrdi 2786 |
. . . . . . . . . . . 12
β’
((β―βπΉ) =
1 β (0..^(β―βπΉ)) = {0}) |
9 | 5, 8 | eleqtrrid 2838 |
. . . . . . . . . . 11
β’
((β―βπΉ) =
1 β 0 β (0..^(β―βπΉ))) |
10 | 9 | ad2antrl 724 |
. . . . . . . . . 10
β’ ((Fun
(iEdgβπΊ) β§
((β―βπΉ) = 1
β§ (πβ0) = (πβ1))) β 0 β
(0..^(β―βπΉ))) |
11 | 10 | 3ad2ant3 1133 |
. . . . . . . . 9
β’ ((πΊ β V β§ πΉ(WalksβπΊ)π β§ (Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1)))) β 0 β
(0..^(β―βπΉ))) |
12 | | eqid 2730 |
. . . . . . . . . 10
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
13 | 12 | iedginwlk 29161 |
. . . . . . . . 9
β’ ((Fun
(iEdgβπΊ) β§ πΉ(WalksβπΊ)π β§ 0 β (0..^(β―βπΉ))) β ((iEdgβπΊ)β(πΉβ0)) β ran (iEdgβπΊ)) |
14 | 2, 3, 11, 13 | syl3anc 1369 |
. . . . . . . 8
β’ ((πΊ β V β§ πΉ(WalksβπΊ)π β§ (Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1)))) β ((iEdgβπΊ)β(πΉβ0)) β ran (iEdgβπΊ)) |
15 | | eqid 2730 |
. . . . . . . . . . 11
β’
(VtxβπΊ) =
(VtxβπΊ) |
16 | 15, 12 | iswlkg 29137 |
. . . . . . . . . 10
β’ (πΊ β V β (πΉ(WalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
17 | 8 | raleqdv 3323 |
. . . . . . . . . . . . . . 15
β’
((β―βπΉ) =
1 β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β βπ β {0}if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
18 | | oveq1 7418 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (π + 1) = (0 + 1)) |
19 | | 0p1e1 12338 |
. . . . . . . . . . . . . . . . . 18
β’ (0 + 1) =
1 |
20 | 18, 19 | eqtrdi 2786 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (π + 1) = 1) |
21 | | wkslem2 29132 |
. . . . . . . . . . . . . . . . 17
β’ ((π = 0 β§ (π + 1) = 1) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0))))) |
22 | 20, 21 | mpdan 683 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0))))) |
23 | 4, 22 | ralsn 4684 |
. . . . . . . . . . . . . . 15
β’
(βπ β
{0}if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0)))) |
24 | 17, 23 | bitrdi 286 |
. . . . . . . . . . . . . 14
β’
((β―βπΉ) =
1 β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0))))) |
25 | 24 | ad2antrl 724 |
. . . . . . . . . . . . 13
β’ ((Fun
(iEdgβπΊ) β§
((β―βπΉ) = 1
β§ (πβ0) = (πβ1))) β
(βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0))))) |
26 | | ifptru 1072 |
. . . . . . . . . . . . . . . . 17
β’ ((πβ0) = (πβ1) β (if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0))) β ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)})) |
27 | 26 | biimpa 475 |
. . . . . . . . . . . . . . . 16
β’ (((πβ0) = (πβ1) β§ if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0)))) β ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}) |
28 | 27 | eqcomd 2736 |
. . . . . . . . . . . . . . 15
β’ (((πβ0) = (πβ1) β§ if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0)))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0))) |
29 | 28 | ex 411 |
. . . . . . . . . . . . . 14
β’ ((πβ0) = (πβ1) β (if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0)))) |
30 | 29 | ad2antll 725 |
. . . . . . . . . . . . 13
β’ ((Fun
(iEdgβπΊ) β§
((β―βπΉ) = 1
β§ (πβ0) = (πβ1))) β (if-((πβ0) = (πβ1), ((iEdgβπΊ)β(πΉβ0)) = {(πβ0)}, {(πβ0), (πβ1)} β ((iEdgβπΊ)β(πΉβ0))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0)))) |
31 | 25, 30 | sylbid 239 |
. . . . . . . . . . . 12
β’ ((Fun
(iEdgβπΊ) β§
((β―βπΉ) = 1
β§ (πβ0) = (πβ1))) β
(βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0)))) |
32 | 31 | com12 32 |
. . . . . . . . . . 11
β’
(βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0)))) |
33 | 32 | 3ad2ant3 1133 |
. . . . . . . . . 10
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0)))) |
34 | 16, 33 | syl6bi 252 |
. . . . . . . . 9
β’ (πΊ β V β (πΉ(WalksβπΊ)π β ((Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0))))) |
35 | 34 | 3imp 1109 |
. . . . . . . 8
β’ ((πΊ β V β§ πΉ(WalksβπΊ)π β§ (Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1)))) β {(πβ0)} = ((iEdgβπΊ)β(πΉβ0))) |
36 | | edgval 28576 |
. . . . . . . . 9
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
37 | 36 | a1i 11 |
. . . . . . . 8
β’ ((πΊ β V β§ πΉ(WalksβπΊ)π β§ (Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1)))) β (EdgβπΊ) = ran (iEdgβπΊ)) |
38 | 14, 35, 37 | 3eltr4d 2846 |
. . . . . . 7
β’ ((πΊ β V β§ πΉ(WalksβπΊ)π β§ (Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1)))) β {(πβ0)} β (EdgβπΊ)) |
39 | 38 | 3exp 1117 |
. . . . . 6
β’ (πΊ β V β (πΉ(WalksβπΊ)π β ((Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} β (EdgβπΊ)))) |
40 | 39 | 3ad2ant1 1131 |
. . . . 5
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(WalksβπΊ)π β ((Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} β (EdgβπΊ)))) |
41 | 1, 40 | mpcom 38 |
. . . 4
β’ (πΉ(WalksβπΊ)π β ((Fun (iEdgβπΊ) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} β (EdgβπΊ))) |
42 | 41 | expd 414 |
. . 3
β’ (πΉ(WalksβπΊ)π β (Fun (iEdgβπΊ) β (((β―βπΉ) = 1 β§ (πβ0) = (πβ1)) β {(πβ0)} β (EdgβπΊ)))) |
43 | 42 | impcom 406 |
. 2
β’ ((Fun
(iEdgβπΊ) β§ πΉ(WalksβπΊ)π) β (((β―βπΉ) = 1 β§ (πβ0) = (πβ1)) β {(πβ0)} β (EdgβπΊ))) |
44 | 43 | imp 405 |
1
β’ (((Fun
(iEdgβπΊ) β§ πΉ(WalksβπΊ)π) β§ ((β―βπΉ) = 1 β§ (πβ0) = (πβ1))) β {(πβ0)} β (EdgβπΊ)) |