Step | Hyp | Ref
| Expression |
1 | | simpl31 1255 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(WalksβπΊ)π) |
2 | | uhgrwkspthlem1 29010 |
. . . . . . . . . . . . . 14
β’ ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = 1) β Fun β‘πΉ) |
3 | 2 | expcom 415 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
1 β (πΉ(WalksβπΊ)π β Fun β‘πΉ)) |
4 | 3 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β (πΉ(WalksβπΊ)π β Fun β‘πΉ)) |
5 | 4 | com12 32 |
. . . . . . . . . . 11
β’ (πΉ(WalksβπΊ)π β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β Fun β‘πΉ)) |
6 | 5 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β Fun β‘πΉ)) |
7 | 6 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β Fun β‘πΉ)) |
8 | 7 | imp 408 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β Fun β‘πΉ) |
9 | | istrl 28953 |
. . . . . . . 8
β’ (πΉ(TrailsβπΊ)π β (πΉ(WalksβπΊ)π β§ Fun β‘πΉ)) |
10 | 1, 8, 9 | sylanbrc 584 |
. . . . . . 7
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(TrailsβπΊ)π) |
11 | | 3simpc 1151 |
. . . . . . . . 9
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β ((β―βπΉ) = 1 β§ π΄ β π΅)) |
12 | 11 | adantl 483 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β ((β―βπΉ) = 1 β§ π΄ β π΅)) |
13 | | 3simpc 1151 |
. . . . . . . . . 10
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
14 | 13 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
16 | | uhgrwkspthlem2 29011 |
. . . . . . . 8
β’ ((πΉ(WalksβπΊ)π β§ ((β―βπΉ) = 1 β§ π΄ β π΅) β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β Fun β‘π) |
17 | 1, 12, 15, 16 | syl3anc 1372 |
. . . . . . 7
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β Fun β‘π) |
18 | | isspth 28981 |
. . . . . . 7
β’ (πΉ(SPathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘π)) |
19 | 10, 17, 18 | sylanbrc 584 |
. . . . . 6
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(SPathsβπΊ)π) |
20 | | 3anass 1096 |
. . . . . 6
β’ ((πΉ(SPathsβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πΉ(SPathsβπΊ)π β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
21 | 19, 15, 20 | sylanbrc 584 |
. . . . 5
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β (πΉ(SPathsβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
22 | | 3simpa 1149 |
. . . . . . 7
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V))) |
23 | 22 | adantr 482 |
. . . . . 6
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V))) |
24 | | eqid 2733 |
. . . . . . 7
β’
(VtxβπΊ) =
(VtxβπΊ) |
25 | 24 | isspthonpth 29006 |
. . . . . 6
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V)) β (πΉ(π΄(SPathsOnβπΊ)π΅)π β (πΉ(SPathsβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
26 | 23, 25 | syl 17 |
. . . . 5
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β (πΉ(π΄(SPathsOnβπΊ)π΅)π β (πΉ(SPathsβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
27 | 21, 26 | mpbird 257 |
. . . 4
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(π΄(SPathsOnβπΊ)π΅)π) |
28 | 27 | ex 414 |
. . 3
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β πΉ(π΄(SPathsOnβπΊ)π΅)π)) |
29 | 24 | wlkonprop 28915 |
. . . 4
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
30 | | 3simpc 1151 |
. . . . 5
β’ ((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ))) |
31 | 30 | 3anim1i 1153 |
. . . 4
β’ (((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
32 | 29, 31 | syl 17 |
. . 3
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
33 | 28, 32 | syl11 33 |
. 2
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β (πΉ(π΄(WalksOnβπΊ)π΅)π β πΉ(π΄(SPathsOnβπΊ)π΅)π)) |
34 | | spthonpthon 29008 |
. . 3
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β πΉ(π΄(PathsOnβπΊ)π΅)π) |
35 | | pthontrlon 29004 |
. . 3
β’ (πΉ(π΄(PathsOnβπΊ)π΅)π β πΉ(π΄(TrailsOnβπΊ)π΅)π) |
36 | | trlsonwlkon 28967 |
. . 3
β’ (πΉ(π΄(TrailsOnβπΊ)π΅)π β πΉ(π΄(WalksOnβπΊ)π΅)π) |
37 | 34, 35, 36 | 3syl 18 |
. 2
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β πΉ(π΄(WalksOnβπΊ)π΅)π) |
38 | 33, 37 | impbid1 224 |
1
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β (πΉ(π΄(WalksOnβπΊ)π΅)π β πΉ(π΄(SPathsOnβπΊ)π΅)π)) |