Step | Hyp | Ref
| Expression |
1 | | iswspthn 29647 |
. 2
β’ (π β (π WSPathsN πΊ) β (π β (π WWalksN πΊ) β§ βπ π(SPathsβπΊ)π)) |
2 | | wwlksnwwlksnon.v |
. . . . 5
β’ π = (VtxβπΊ) |
3 | 2 | wwlksnwwlksnon 29713 |
. . . 4
β’ (π β (π WWalksN πΊ) β βπ β π βπ β π π β (π(π WWalksNOn πΊ)π)) |
4 | 3 | anbi1i 623 |
. . 3
β’ ((π β (π WWalksN πΊ) β§ βπ π(SPathsβπΊ)π) β (βπ β π βπ β π π β (π(π WWalksNOn πΊ)π) β§ βπ π(SPathsβπΊ)π)) |
5 | | r19.41vv 3219 |
. . 3
β’
(βπ β
π βπ β π (π β (π(π WWalksNOn πΊ)π) β§ βπ π(SPathsβπΊ)π) β (βπ β π βπ β π π β (π(π WWalksNOn πΊ)π) β§ βπ π(SPathsβπΊ)π)) |
6 | 4, 5 | bitr4i 278 |
. 2
β’ ((π β (π WWalksN πΊ) β§ βπ π(SPathsβπΊ)π) β βπ β π βπ β π (π β (π(π WWalksNOn πΊ)π) β§ βπ π(SPathsβπΊ)π)) |
7 | | 3anass 1093 |
. . . . . . . 8
β’ ((π(SPathsβπΊ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π) β (π(SPathsβπΊ)π β§ ((πβ0) = π β§ (πβ(β―βπ)) = π))) |
8 | 7 | a1i 11 |
. . . . . . 7
β’ (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β ((π(SPathsβπΊ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π) β (π(SPathsβπΊ)π β§ ((πβ0) = π β§ (πβ(β―βπ)) = π)))) |
9 | | vex 3473 |
. . . . . . . 8
β’ π β V |
10 | 2 | isspthonpth 29550 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ (π β V β§ π β (π(π WWalksNOn πΊ)π))) β (π(π(SPathsOnβπΊ)π)π β (π(SPathsβπΊ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π))) |
11 | 9, 10 | mpanr1 702 |
. . . . . . 7
β’ (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β (π(π(SPathsOnβπΊ)π)π β (π(SPathsβπΊ)π β§ (πβ0) = π β§ (πβ(β―βπ)) = π))) |
12 | | spthiswlk 29529 |
. . . . . . . . . 10
β’ (π(SPathsβπΊ)π β π(WalksβπΊ)π) |
13 | | wlklenvm1 29423 |
. . . . . . . . . 10
β’ (π(WalksβπΊ)π β (β―βπ) = ((β―βπ) β 1)) |
14 | | wwlknon 29655 |
. . . . . . . . . . . . 13
β’ (π β (π(π WWalksNOn πΊ)π) β (π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π)) |
15 | | simpl2 1190 |
. . . . . . . . . . . . . . 15
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β (πβ0) = π) |
16 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β (β―βπ) = ((β―βπ) β 1)) |
17 | | wwlknbp1 29642 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π WWalksN πΊ) β (π β β0 β§ π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1))) |
18 | | oveq1 7421 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ) =
(π + 1) β
((β―βπ) β
1) = ((π + 1) β
1)) |
19 | 18 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β0
β§ π β Word
(VtxβπΊ) β§
(β―βπ) = (π + 1)) β
((β―βπ) β
1) = ((π + 1) β
1)) |
20 | | nn0cn 12504 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β0
β π β
β) |
21 | | pncan1 11660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β ((π + 1) β 1) = π) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β0
β ((π + 1) β 1)
= π) |
23 | 22 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β0
β§ π β Word
(VtxβπΊ) β§
(β―βπ) = (π + 1)) β ((π + 1) β 1) = π) |
24 | 19, 23 | eqtrd 2767 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β0
β§ π β Word
(VtxβπΊ) β§
(β―βπ) = (π + 1)) β
((β―βπ) β
1) = π) |
25 | 17, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π WWalksN πΊ) β ((β―βπ) β 1) = π) |
26 | 25 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β ((β―βπ) β 1) = π) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β ((β―βπ) β 1) = π) |
28 | 16, 27 | eqtrd 2767 |
. . . . . . . . . . . . . . . . 17
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β (β―βπ) = π) |
29 | 28 | fveq2d 6895 |
. . . . . . . . . . . . . . . 16
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β (πβ(β―βπ)) = (πβπ)) |
30 | | simpl3 1191 |
. . . . . . . . . . . . . . . 16
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β (πβπ) = π) |
31 | 29, 30 | eqtrd 2767 |
. . . . . . . . . . . . . . 15
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β (πβ(β―βπ)) = π) |
32 | 15, 31 | jca 511 |
. . . . . . . . . . . . . 14
β’ (((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β§ (β―βπ) = ((β―βπ) β 1)) β ((πβ0) = π β§ (πβ(β―βπ)) = π)) |
33 | 32 | ex 412 |
. . . . . . . . . . . . 13
β’ ((π β (π WWalksN πΊ) β§ (πβ0) = π β§ (πβπ) = π) β ((β―βπ) = ((β―βπ) β 1) β ((πβ0) = π β§ (πβ(β―βπ)) = π))) |
34 | 14, 33 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β (π(π WWalksNOn πΊ)π) β ((β―βπ) = ((β―βπ) β 1) β ((πβ0) = π β§ (πβ(β―βπ)) = π))) |
35 | 34 | adantl 481 |
. . . . . . . . . . 11
β’ (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β ((β―βπ) = ((β―βπ) β 1) β ((πβ0) = π β§ (πβ(β―βπ)) = π))) |
36 | 35 | com12 32 |
. . . . . . . . . 10
β’
((β―βπ) =
((β―βπ) β
1) β (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β ((πβ0) = π β§ (πβ(β―βπ)) = π))) |
37 | 12, 13, 36 | 3syl 18 |
. . . . . . . . 9
β’ (π(SPathsβπΊ)π β (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β ((πβ0) = π β§ (πβ(β―βπ)) = π))) |
38 | 37 | com12 32 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β (π(SPathsβπΊ)π β ((πβ0) = π β§ (πβ(β―βπ)) = π))) |
39 | 38 | pm4.71d 561 |
. . . . . . 7
β’ (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β (π(SPathsβπΊ)π β (π(SPathsβπΊ)π β§ ((πβ0) = π β§ (πβ(β―βπ)) = π)))) |
40 | 8, 11, 39 | 3bitr4rd 312 |
. . . . . 6
β’ (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β (π(SPathsβπΊ)π β π(π(SPathsOnβπΊ)π)π)) |
41 | 40 | exbidv 1917 |
. . . . 5
β’ (((π β π β§ π β π) β§ π β (π(π WWalksNOn πΊ)π)) β (βπ π(SPathsβπΊ)π β βπ π(π(SPathsOnβπΊ)π)π)) |
42 | 41 | pm5.32da 578 |
. . . 4
β’ ((π β π β§ π β π) β ((π β (π(π WWalksNOn πΊ)π) β§ βπ π(SPathsβπΊ)π) β (π β (π(π WWalksNOn πΊ)π) β§ βπ π(π(SPathsOnβπΊ)π)π))) |
43 | | wspthnon 29656 |
. . . 4
β’ (π β (π(π WSPathsNOn πΊ)π) β (π β (π(π WWalksNOn πΊ)π) β§ βπ π(π(SPathsOnβπΊ)π)π)) |
44 | 42, 43 | bitr4di 289 |
. . 3
β’ ((π β π β§ π β π) β ((π β (π(π WWalksNOn πΊ)π) β§ βπ π(SPathsβπΊ)π) β π β (π(π WSPathsNOn πΊ)π))) |
45 | 44 | 2rexbiia 3210 |
. 2
β’
(βπ β
π βπ β π (π β (π(π WWalksNOn πΊ)π) β§ βπ π(SPathsβπΊ)π) β βπ β π βπ β π π β (π(π WSPathsNOn πΊ)π)) |
46 | 1, 6, 45 | 3bitri 297 |
1
β’ (π β (π WSPathsN πΊ) β βπ β π βπ β π π β (π(π WSPathsNOn πΊ)π)) |