Step | Hyp | Ref
| Expression |
1 | | simpl31 1252 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(WalksβπΊ)π) |
2 | | uhgrwkspthlem1 29277 |
. . . . . . . . . . . . . 14
β’ ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = 1) β Fun β‘πΉ) |
3 | 2 | expcom 412 |
. . . . . . . . . . . . 13
β’
((β―βπΉ) =
1 β (πΉ(WalksβπΊ)π β Fun β‘πΉ)) |
4 | 3 | 3ad2ant2 1132 |
. . . . . . . . . . . 12
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β (πΉ(WalksβπΊ)π β Fun β‘πΉ)) |
5 | 4 | com12 32 |
. . . . . . . . . . 11
β’ (πΉ(WalksβπΊ)π β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β Fun β‘πΉ)) |
6 | 5 | 3ad2ant1 1131 |
. . . . . . . . . 10
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β Fun β‘πΉ)) |
7 | 6 | 3ad2ant3 1133 |
. . . . . . . . 9
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β Fun β‘πΉ)) |
8 | 7 | imp 405 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β Fun β‘πΉ) |
9 | | istrl 29220 |
. . . . . . . 8
β’ (πΉ(TrailsβπΊ)π β (πΉ(WalksβπΊ)π β§ Fun β‘πΉ)) |
10 | 1, 8, 9 | sylanbrc 581 |
. . . . . . 7
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(TrailsβπΊ)π) |
11 | | 3simpc 1148 |
. . . . . . . . 9
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β ((β―βπΉ) = 1 β§ π΄ β π΅)) |
12 | 11 | adantl 480 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β ((β―βπΉ) = 1 β§ π΄ β π΅)) |
13 | | 3simpc 1148 |
. . . . . . . . . 10
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
14 | 13 | 3ad2ant3 1133 |
. . . . . . . . 9
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
15 | 14 | adantr 479 |
. . . . . . . 8
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
16 | | uhgrwkspthlem2 29278 |
. . . . . . . 8
β’ ((πΉ(WalksβπΊ)π β§ ((β―βπΉ) = 1 β§ π΄ β π΅) β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β Fun β‘π) |
17 | 1, 12, 15, 16 | syl3anc 1369 |
. . . . . . 7
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β Fun β‘π) |
18 | | isspth 29248 |
. . . . . . 7
β’ (πΉ(SPathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ Fun β‘π)) |
19 | 10, 17, 18 | sylanbrc 581 |
. . . . . 6
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(SPathsβπΊ)π) |
20 | | 3anass 1093 |
. . . . . 6
β’ ((πΉ(SPathsβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β (πΉ(SPathsβπΊ)π β§ ((πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
21 | 19, 15, 20 | sylanbrc 581 |
. . . . 5
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β (πΉ(SPathsβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) |
22 | | 3simpa 1146 |
. . . . . . 7
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V))) |
23 | 22 | adantr 479 |
. . . . . 6
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β ((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V))) |
24 | | eqid 2730 |
. . . . . . 7
β’
(VtxβπΊ) =
(VtxβπΊ) |
25 | 24 | isspthonpth 29273 |
. . . . . 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 256 |
. . . 4
β’ ((((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β§ (πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅)) β πΉ(π΄(SPathsOnβπΊ)π΅)π) |
28 | 27 | ex 411 |
. . 3
β’ (((π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β πΉ(π΄(SPathsOnβπΊ)π΅)π)) |
29 | 24 | wlkonprop 29182 |
. . . 4
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
30 | | 3simpc 1148 |
. . . . 5
β’ ((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β (π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ))) |
31 | 30 | 3anim1i 1150 |
. . . 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 29275 |
. . 3
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β πΉ(π΄(PathsOnβπΊ)π΅)π) |
35 | | pthontrlon 29271 |
. . 3
β’ (πΉ(π΄(PathsOnβπΊ)π΅)π β πΉ(π΄(TrailsOnβπΊ)π΅)π) |
36 | | trlsonwlkon 29234 |
. . 3
β’ (πΉ(π΄(TrailsOnβπΊ)π΅)π β πΉ(π΄(WalksOnβπΊ)π΅)π) |
37 | 34, 35, 36 | 3syl 18 |
. 2
β’ (πΉ(π΄(SPathsOnβπΊ)π΅)π β πΉ(π΄(WalksOnβπΊ)π΅)π) |
38 | 33, 37 | impbid1 224 |
1
β’ ((πΊ β π β§ (β―βπΉ) = 1 β§ π΄ β π΅) β (πΉ(π΄(WalksOnβπΊ)π΅)π β πΉ(π΄(SPathsOnβπΊ)π΅)π)) |