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 USGraph A B A 2 WSPathsNOn G B = A 2 WWalksNOn G B

Proof

Step Hyp Ref Expression
1 wwlknon w A 2 WWalksNOn G B w 2 WWalksN G w 0 = A w 2 = B
2 1 a1i G USGraph A B w A 2 WWalksNOn G B w 2 WWalksN G w 0 = A w 2 = B
3 2 anbi1d G USGraph A B w A 2 WWalksNOn G B f f A SPathsOn G B w w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w
4 3anass w 2 WWalksN G w 0 = A w 2 = B w 2 WWalksN G w 0 = A w 2 = B
5 4 anbi1i w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w
6 anass w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w
7 5 6 bitri w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w
8 3 7 bitrdi G USGraph A B w A 2 WWalksNOn G B f f A SPathsOn G B w w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w
9 8 rabbidva2 G USGraph A B w A 2 WWalksNOn G B | f f A SPathsOn G B w = w 2 WWalksN G | w 0 = A w 2 = B f f A SPathsOn G B w
10 usgrupgr G USGraph G UPGraph
11 wlklnwwlknupgr G UPGraph f f Walks G w f = 2 w 2 WWalksN G
12 10 11 syl G USGraph f f Walks G w f = 2 w 2 WWalksN G
13 12 bicomd G USGraph w 2 WWalksN G f f Walks G w f = 2
14 13 adantr G USGraph A B w 2 WWalksN G f f Walks G w f = 2
15 simprl G USGraph A B w 0 = A w 2 = B f Walks G w f = 2 f Walks G w
16 simprl G USGraph A B w 0 = A w 2 = B w 0 = A
17 16 adantr G 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 USGraph A B w 0 = A w 2 = B f Walks G w f = 2 w f = w 2
20 simprr G USGraph A B w 0 = A w 2 = B w 2 = B
21 20 adantr G USGraph A B w 0 = A w 2 = B f Walks G w f = 2 w 2 = B
22 19 21 eqtrd G 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 0
31 0elfz 2 0 0 0 2
32 30 31 mp1i w : 0 2 Vtx G 0 0 2
33 29 32 ffvelrnd w : 0 2 Vtx G w 0 Vtx G
34 nn0fz0 2 0 2 0 2
35 30 34 mpbi 2 0 2
36 35 a1i w : 0 2 Vtx G 2 0 2
37 29 36 ffvelrnd w : 0 2 Vtx G w 2 Vtx G
38 33 37 jca w : 0 2 Vtx G w 0 Vtx G w 2 Vtx G
39 28 38 syl f Walks G w f = 2 w 0 Vtx G w 2 Vtx G
40 eleq1 w 0 = A w 0 Vtx G A Vtx G
41 eleq1 w 2 = B w 2 Vtx G B Vtx G
42 40 41 bi2anan9 w 0 = A w 2 = B w 0 Vtx G w 2 Vtx G A Vtx G B Vtx G
43 39 42 syl5ib w 0 = A w 2 = B f Walks G w f = 2 A Vtx G B Vtx G
44 43 adantl G USGraph A B w 0 = A w 2 = B f Walks G w f = 2 A Vtx G B Vtx G
45 44 imp G USGraph A B w 0 = A w 2 = B f Walks G w f = 2 A Vtx G B Vtx G
46 vex f V
47 vex w V
48 46 47 pm3.2i f V w V
49 23 iswlkon A Vtx G B Vtx G f V w V f A WalksOn G B w f Walks G w w 0 = A w f = B
50 45 48 49 sylancl G 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 USGraph A B w 0 = A w 2 = B f Walks G w f = 2 f A WalksOn G B w
52 simplll G USGraph A B w 0 = A w 2 = B f Walks G w f = 2 G USGraph
53 simprr G USGraph A B w 0 = A w 2 = B f Walks G w f = 2 f = 2
54 simpllr G USGraph A B w 0 = A w 2 = B f Walks G w f = 2 A B
55 usgr2wlkspth G USGraph f = 2 A B f A WalksOn G B w f A SPathsOn G B w
56 52 53 54 55 syl3anc G 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 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 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 USGraph A B w 0 = A w 2 = B f f Walks G w f = 2 f f A SPathsOn G B w
60 59 ex G USGraph A B w 0 = A w 2 = B f f Walks G w f = 2 f f A SPathsOn G B w
61 60 com23 G USGraph A B f f Walks G w f = 2 w 0 = A w 2 = B f f A SPathsOn G B w
62 14 61 sylbid G USGraph A B w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w
63 62 imp G USGraph A B w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w
64 63 pm4.71d G USGraph A B w 2 WWalksN G w 0 = A w 2 = B w 0 = A w 2 = B f f A SPathsOn G B w
65 64 bicomd G USGraph A B w 2 WWalksN G w 0 = A w 2 = B f f A SPathsOn G B w w 0 = A w 2 = B
66 65 rabbidva G USGraph A B w 2 WWalksN G | w 0 = A w 2 = B f f A SPathsOn G B w = w 2 WWalksN G | w 0 = A w 2 = B
67 9 66 eqtrd G USGraph A B w A 2 WWalksNOn G B | f f A SPathsOn G B w = w 2 WWalksN G | w 0 = A w 2 = B
68 23 iswspthsnon A 2 WSPathsNOn G B = w A 2 WWalksNOn G B | f f A SPathsOn G B w
69 23 iswwlksnon A 2 WWalksNOn G B = w 2 WWalksN G | w 0 = A w 2 = B
70 67 68 69 3eqtr4g G USGraph A B A 2 WSPathsNOn G B = A 2 WWalksNOn G B