Metamath Proof Explorer

Theorem wpthswwlks2on

Description: For two different vertices, a walk of length 2 between these vertices is a simple path of length 2 between these vertices in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 13-May-2021) (Revised by AV, 16-Mar-2022)

Ref Expression
Assertion wpthswwlks2on 
|- ( ( G e. USGraph /\ A =/= B ) -> ( A ( 2 WSPathsNOn G ) B ) = ( A ( 2 WWalksNOn G ) B ) )

Proof

Step Hyp Ref Expression
1 wwlknon 
 |-  ( w e. ( A ( 2 WWalksNOn G ) B ) <-> ( w e. ( 2 WWalksN G ) /\ ( w ` 0 ) = A /\ ( w ` 2 ) = B ) )
2 1 a1i 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( w e. ( A ( 2 WWalksNOn G ) B ) <-> ( w e. ( 2 WWalksN G ) /\ ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) )
3 2 anbi1d 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( ( w e. ( A ( 2 WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) <-> ( ( w e. ( 2 WWalksN G ) /\ ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) ) )
4 3anass 
 |-  ( ( w e. ( 2 WWalksN G ) /\ ( w ` 0 ) = A /\ ( w ` 2 ) = B ) <-> ( w e. ( 2 WWalksN G ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) )
5 4 anbi1i 
 |-  ( ( ( w e. ( 2 WWalksN G ) /\ ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) <-> ( ( w e. ( 2 WWalksN G ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) )
6 anass 
 |-  ( ( ( w e. ( 2 WWalksN G ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) <-> ( w e. ( 2 WWalksN G ) /\ ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) ) )
7 5 6 bitri 
 |-  ( ( ( w e. ( 2 WWalksN G ) /\ ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) <-> ( w e. ( 2 WWalksN G ) /\ ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) ) )
8 3 7 bitrdi 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( ( w e. ( A ( 2 WWalksNOn G ) B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) <-> ( w e. ( 2 WWalksN G ) /\ ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) ) ) )
9 8 rabbidva2 
 |-  ( ( G e. USGraph /\ A =/= B ) -> { w e. ( A ( 2 WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = { w e. ( 2 WWalksN G ) | ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) } )
10 usgrupgr 
 |-  ( G e. USGraph -> G e. UPGraph )
11 wlklnwwlknupgr 
 |-  ( G e. UPGraph -> ( E. f ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) <-> w e. ( 2 WWalksN G ) ) )
12 10 11 syl 
 |-  ( G e. USGraph -> ( E. f ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) <-> w e. ( 2 WWalksN G ) ) )
13 12 bicomd 
 |-  ( G e. USGraph -> ( w e. ( 2 WWalksN G ) <-> E. f ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) )
14 13 adantr 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( w e. ( 2 WWalksN G ) <-> E. f ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) )
15 simprl 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> f ( Walks ` G ) w )
16 simprl 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) -> ( w ` 0 ) = A )
17 16 adantr 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( w ` 0 ) = A )
18 fveq2 
 |-  ( ( # ` f ) = 2 -> ( w ` ( # ` f ) ) = ( w ` 2 ) )
19 18 ad2antll 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( w ` ( # ` f ) ) = ( w ` 2 ) )
20 simprr 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) -> ( w ` 2 ) = B )
21 20 adantr 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( w ` 2 ) = B )
22 19 21 eqtrd 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( w ` ( # ` f ) ) = B )
23 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
24 23 wlkp 
 |-  ( f ( Walks ` G ) w -> w : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) )
25 oveq2 
 |-  ( ( # ` f ) = 2 -> ( 0 ... ( # ` f ) ) = ( 0 ... 2 ) )
26 25 feq2d 
 |-  ( ( # ` f ) = 2 -> ( w : ( 0 ... ( # ` f ) ) --> ( Vtx ` G ) <-> w : ( 0 ... 2 ) --> ( Vtx ` G ) ) )
27 24 26 syl5ibcom 
 |-  ( f ( Walks ` G ) w -> ( ( # ` f ) = 2 -> w : ( 0 ... 2 ) --> ( Vtx ` G ) ) )
28 27 imp 
 |-  ( ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> w : ( 0 ... 2 ) --> ( Vtx ` G ) )
29 id 
 |-  ( w : ( 0 ... 2 ) --> ( Vtx ` G ) -> w : ( 0 ... 2 ) --> ( Vtx ` G ) )
30 2nn0 
 |-  2 e. NN0
31 0elfz 
 |-  ( 2 e. NN0 -> 0 e. ( 0 ... 2 ) )
32 30 31 mp1i 
 |-  ( w : ( 0 ... 2 ) --> ( Vtx ` G ) -> 0 e. ( 0 ... 2 ) )
33 29 32 ffvelcdmd 
 |-  ( w : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( w ` 0 ) e. ( Vtx ` G ) )
34 nn0fz0 
 |-  ( 2 e. NN0 <-> 2 e. ( 0 ... 2 ) )
35 30 34 mpbi 
 |-  2 e. ( 0 ... 2 )
36 35 a1i 
 |-  ( w : ( 0 ... 2 ) --> ( Vtx ` G ) -> 2 e. ( 0 ... 2 ) )
37 29 36 ffvelcdmd 
 |-  ( w : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( w ` 2 ) e. ( Vtx ` G ) )
38 33 37 jca 
 |-  ( w : ( 0 ... 2 ) --> ( Vtx ` G ) -> ( ( w ` 0 ) e. ( Vtx ` G ) /\ ( w ` 2 ) e. ( Vtx ` G ) ) )
39 28 38 syl 
 |-  ( ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> ( ( w ` 0 ) e. ( Vtx ` G ) /\ ( w ` 2 ) e. ( Vtx ` G ) ) )
40 eleq1 
 |-  ( ( w ` 0 ) = A -> ( ( w ` 0 ) e. ( Vtx ` G ) <-> A e. ( Vtx ` G ) ) )
41 eleq1 
 |-  ( ( w ` 2 ) = B -> ( ( w ` 2 ) e. ( Vtx ` G ) <-> B e. ( Vtx ` G ) ) )
42 40 41 bi2anan9 
 |-  ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) -> ( ( ( w ` 0 ) e. ( Vtx ` G ) /\ ( w ` 2 ) e. ( Vtx ` G ) ) <-> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) ) )
43 39 42 imbitrid 
 |-  ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) -> ( ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) ) )
44 43 adantl 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) -> ( ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) ) )
45 44 imp 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
46 vex 
 |-  f e. _V
47 vex 
 |-  w e. _V
48 46 47 pm3.2i 
 |-  ( f e. _V /\ w e. _V )
49 23 iswlkon 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( f e. _V /\ w e. _V ) ) -> ( f ( A ( WalksOn ` G ) B ) w <-> ( f ( Walks ` G ) w /\ ( w ` 0 ) = A /\ ( w ` ( # ` f ) ) = B ) ) )
50 45 48 49 sylancl 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( f ( A ( WalksOn ` G ) B ) w <-> ( f ( Walks ` G ) w /\ ( w ` 0 ) = A /\ ( w ` ( # ` f ) ) = B ) ) )
51 15 17 22 50 mpbir3and 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> f ( A ( WalksOn ` G ) B ) w )
52 simplll 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> G e. USGraph )
53 simprr 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( # ` f ) = 2 )
54 simpllr 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> A =/= B )
55 usgr2wlkspth 
 |-  ( ( G e. USGraph /\ ( # ` f ) = 2 /\ A =/= B ) -> ( f ( A ( WalksOn ` G ) B ) w <-> f ( A ( SPathsOn ` G ) B ) w ) )
56 52 53 54 55 syl3anc 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> ( f ( A ( WalksOn ` G ) B ) w <-> f ( A ( SPathsOn ` G ) B ) w ) )
57 51 56 mpbid 
 |-  ( ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) /\ ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) ) -> f ( A ( SPathsOn ` G ) B ) w )
58 57 ex 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) -> ( ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> f ( A ( SPathsOn ` G ) B ) w ) )
59 58 eximdv 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) -> ( E. f ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> E. f f ( A ( SPathsOn ` G ) B ) w ) )
60 59 ex 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) -> ( E. f ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> E. f f ( A ( SPathsOn ` G ) B ) w ) ) )
61 60 com23 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( E. f ( f ( Walks ` G ) w /\ ( # ` f ) = 2 ) -> ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) -> E. f f ( A ( SPathsOn ` G ) B ) w ) ) )
62 14 61 sylbid 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( w e. ( 2 WWalksN G ) -> ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) -> E. f f ( A ( SPathsOn ` G ) B ) w ) ) )
63 62 imp 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ w e. ( 2 WWalksN G ) ) -> ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) -> E. f f ( A ( SPathsOn ` G ) B ) w ) )
64 63 pm4.71d 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ w e. ( 2 WWalksN G ) ) -> ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) <-> ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) ) )
65 64 bicomd 
 |-  ( ( ( G e. USGraph /\ A =/= B ) /\ w e. ( 2 WWalksN G ) ) -> ( ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) <-> ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) ) )
66 65 rabbidva 
 |-  ( ( G e. USGraph /\ A =/= B ) -> { w e. ( 2 WWalksN G ) | ( ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) /\ E. f f ( A ( SPathsOn ` G ) B ) w ) } = { w e. ( 2 WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) } )
67 9 66 eqtrd 
 |-  ( ( G e. USGraph /\ A =/= B ) -> { w e. ( A ( 2 WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = { w e. ( 2 WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) } )
68 23 iswspthsnon 
 |-  ( A ( 2 WSPathsNOn G ) B ) = { w e. ( A ( 2 WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w }
69 23 iswwlksnon 
 |-  ( A ( 2 WWalksNOn G ) B ) = { w e. ( 2 WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` 2 ) = B ) }
70 67 68 69 3eqtr4g 
 |-  ( ( G e. USGraph /\ A =/= B ) -> ( A ( 2 WSPathsNOn G ) B ) = ( A ( 2 WWalksNOn G ) B ) )