Metamath Proof Explorer


Theorem wspthsnwspthsnon

Description: A simple path of fixed length is a simple path of fixed length between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 16-May-2021) (Revised by AV, 13-Mar-2022)

Ref Expression
Hypothesis wwlksnwwlksnon.v V = Vtx G
Assertion wspthsnwspthsnon W N WSPathsN G a V b V W a N WSPathsNOn G b

Proof

Step Hyp Ref Expression
1 wwlksnwwlksnon.v V = Vtx G
2 iswspthn W N WSPathsN G W N WWalksN G f f SPaths G W
3 1 wwlksnwwlksnon W N WWalksN G a V b V W a N WWalksNOn G b
4 3 anbi1i W N WWalksN G f f SPaths G W a V b V W a N WWalksNOn G b f f SPaths G W
5 r19.41vv a V b V W a N WWalksNOn G b f f SPaths G W a V b V W a N WWalksNOn G b f f SPaths G W
6 4 5 bitr4i W N WWalksN G f f SPaths G W a V b V W a N WWalksNOn G b f f SPaths G W
7 3anass f SPaths G W W 0 = a W f = b f SPaths G W W 0 = a W f = b
8 7 a1i a V b V W a N WWalksNOn G b f SPaths G W W 0 = a W f = b f SPaths G W W 0 = a W f = b
9 vex f V
10 1 isspthonpth a V b V f V W a N WWalksNOn G b f a SPathsOn G b W f SPaths G W W 0 = a W f = b
11 9 10 mpanr1 a V b V W a N WWalksNOn G b f a SPathsOn G b W f SPaths G W W 0 = a W f = b
12 spthiswlk f SPaths G W f Walks G W
13 wlklenvm1 f Walks G W f = W 1
14 wwlknon W a N WWalksNOn G b W N WWalksN G W 0 = a W N = b
15 simpl2 W N WWalksN G W 0 = a W N = b f = W 1 W 0 = a
16 simpr W N WWalksN G W 0 = a W N = b f = W 1 f = W 1
17 wwlknbp1 W N WWalksN G N 0 W Word Vtx G W = N + 1
18 oveq1 W = N + 1 W 1 = N + 1 - 1
19 18 3ad2ant3 N 0 W Word Vtx G W = N + 1 W 1 = N + 1 - 1
20 nn0cn N 0 N
21 pncan1 N N + 1 - 1 = N
22 20 21 syl N 0 N + 1 - 1 = N
23 22 3ad2ant1 N 0 W Word Vtx G W = N + 1 N + 1 - 1 = N
24 19 23 eqtrd N 0 W Word Vtx G W = N + 1 W 1 = N
25 17 24 syl W N WWalksN G W 1 = N
26 25 3ad2ant1 W N WWalksN G W 0 = a W N = b W 1 = N
27 26 adantr W N WWalksN G W 0 = a W N = b f = W 1 W 1 = N
28 16 27 eqtrd W N WWalksN G W 0 = a W N = b f = W 1 f = N
29 28 fveq2d W N WWalksN G W 0 = a W N = b f = W 1 W f = W N
30 simpl3 W N WWalksN G W 0 = a W N = b f = W 1 W N = b
31 29 30 eqtrd W N WWalksN G W 0 = a W N = b f = W 1 W f = b
32 15 31 jca W N WWalksN G W 0 = a W N = b f = W 1 W 0 = a W f = b
33 32 ex W N WWalksN G W 0 = a W N = b f = W 1 W 0 = a W f = b
34 14 33 sylbi W a N WWalksNOn G b f = W 1 W 0 = a W f = b
35 34 adantl a V b V W a N WWalksNOn G b f = W 1 W 0 = a W f = b
36 35 com12 f = W 1 a V b V W a N WWalksNOn G b W 0 = a W f = b
37 12 13 36 3syl f SPaths G W a V b V W a N WWalksNOn G b W 0 = a W f = b
38 37 com12 a V b V W a N WWalksNOn G b f SPaths G W W 0 = a W f = b
39 38 pm4.71d a V b V W a N WWalksNOn G b f SPaths G W f SPaths G W W 0 = a W f = b
40 8 11 39 3bitr4rd a V b V W a N WWalksNOn G b f SPaths G W f a SPathsOn G b W
41 40 exbidv a V b V W a N WWalksNOn G b f f SPaths G W f f a SPathsOn G b W
42 41 pm5.32da a V b V W a N WWalksNOn G b f f SPaths G W W a N WWalksNOn G b f f a SPathsOn G b W
43 wspthnon W a N WSPathsNOn G b W a N WWalksNOn G b f f a SPathsOn G b W
44 42 43 bitr4di a V b V W a N WWalksNOn G b f f SPaths G W W a N WSPathsNOn G b
45 44 2rexbiia a V b V W a N WWalksNOn G b f f SPaths G W a V b V W a N WSPathsNOn G b
46 2 6 45 3bitri W N WSPathsN G a V b V W a N WSPathsNOn G b