Metamath Proof Explorer


Theorem elwspths2spth

Description: A simple path of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 28-Feb-2018) (Revised by AV, 18-May-2021) (Proof shortened by AV, 16-Mar-2022)

Ref Expression
Hypothesis elwwlks2.v V = Vtx G
Assertion elwspths2spth G UPGraph W 2 WSPathsN G a V b V c V W = ⟨“ abc ”⟩ f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2

Proof

Step Hyp Ref Expression
1 elwwlks2.v V = Vtx G
2 1 wspthsnwspthsnon W 2 WSPathsN G a V c V W a 2 WSPathsNOn G c
3 2 a1i G UPGraph W 2 WSPathsN G a V c V W a 2 WSPathsNOn G c
4 1 elwspths2on G UPGraph a V c V W a 2 WSPathsNOn G c b V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c
5 4 3expb G UPGraph a V c V W a 2 WSPathsNOn G c b V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c
6 5 2rexbidva G UPGraph a V c V W a 2 WSPathsNOn G c a V c V b V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c
7 rexcom c V b V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c b V c V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c
8 wspthnon ⟨“ abc ”⟩ a 2 WSPathsNOn G c ⟨“ abc ”⟩ a 2 WWalksNOn G c f f a SPathsOn G c ⟨“ abc ”⟩
9 ancom ⟨“ abc ”⟩ a 2 WWalksNOn G c f f a SPathsOn G c ⟨“ abc ”⟩ f f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c
10 19.41v f f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c f f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c
11 9 10 bitr4i ⟨“ abc ”⟩ a 2 WWalksNOn G c f f a SPathsOn G c ⟨“ abc ”⟩ f f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c
12 simpr G UPGraph a V a V
13 simpr b V c V c V
14 12 13 anim12i G UPGraph a V b V c V a V c V
15 vex f V
16 s3cli ⟨“ abc ”⟩ Word V
17 15 16 pm3.2i f V ⟨“ abc ”⟩ Word V
18 1 isspthonpth a V c V f V ⟨“ abc ”⟩ Word V f a SPathsOn G c ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c
19 14 17 18 sylancl G UPGraph a V b V c V f a SPathsOn G c ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c
20 wwlknon ⟨“ abc ”⟩ a 2 WWalksNOn G c ⟨“ abc ”⟩ 2 WWalksN G ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
21 2nn0 2 0
22 iswwlksn 2 0 ⟨“ abc ”⟩ 2 WWalksN G ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1
23 21 22 mp1i G UPGraph a V b V c V ⟨“ abc ”⟩ 2 WWalksN G ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1
24 23 3anbi1d G UPGraph a V b V c V ⟨“ abc ”⟩ 2 WWalksN G ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
25 20 24 syl5bb G UPGraph a V b V c V ⟨“ abc ”⟩ a 2 WWalksNOn G c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
26 19 25 anbi12d G UPGraph a V b V c V f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
27 26 adantr G UPGraph a V b V c V W = ⟨“ abc ”⟩ f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
28 16 a1i G UPGraph a V b V c V ⟨“ abc ”⟩ Word V
29 simprl1 G UPGraph a V b V c V p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f SPaths G ⟨“ abc ”⟩
30 spthiswlk f SPaths G ⟨“ abc ”⟩ f Walks G ⟨“ abc ”⟩
31 wlklenvm1 f Walks G ⟨“ abc ”⟩ f = ⟨“ abc ”⟩ 1
32 simpl f = ⟨“ abc ”⟩ 1 ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f = ⟨“ abc ”⟩ 1
33 oveq1 ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 1 = 2 + 1 - 1
34 2cn 2
35 pncan1 2 2 + 1 - 1 = 2
36 34 35 ax-mp 2 + 1 - 1 = 2
37 33 36 syl6eq ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 1 = 2
38 37 adantl ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 1 = 2
39 38 3ad2ant1 ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c ⟨“ abc ”⟩ 1 = 2
40 39 adantl f = ⟨“ abc ”⟩ 1 ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c ⟨“ abc ”⟩ 1 = 2
41 32 40 eqtrd f = ⟨“ abc ”⟩ 1 ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f = 2
42 41 ex f = ⟨“ abc ”⟩ 1 ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f = 2
43 30 31 42 3syl f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f = 2
44 43 3ad2ant1 f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f = 2
45 44 imp f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f = 2
46 45 adantl G UPGraph a V b V c V p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f = 2
47 s3fv0 a V ⟨“ abc ”⟩ 0 = a
48 47 elv ⟨“ abc ”⟩ 0 = a
49 48 eqcomi a = ⟨“ abc ”⟩ 0
50 s3fv1 b V ⟨“ abc ”⟩ 1 = b
51 50 elv ⟨“ abc ”⟩ 1 = b
52 51 eqcomi b = ⟨“ abc ”⟩ 1
53 s3fv2 c V ⟨“ abc ”⟩ 2 = c
54 53 elv ⟨“ abc ”⟩ 2 = c
55 54 eqcomi c = ⟨“ abc ”⟩ 2
56 49 52 55 3pm3.2i a = ⟨“ abc ”⟩ 0 b = ⟨“ abc ”⟩ 1 c = ⟨“ abc ”⟩ 2
57 56 a1i G UPGraph a V b V c V p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c a = ⟨“ abc ”⟩ 0 b = ⟨“ abc ”⟩ 1 c = ⟨“ abc ”⟩ 2
58 29 46 57 3jca G UPGraph a V b V c V p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f SPaths G ⟨“ abc ”⟩ f = 2 a = ⟨“ abc ”⟩ 0 b = ⟨“ abc ”⟩ 1 c = ⟨“ abc ”⟩ 2
59 breq2 p = ⟨“ abc ”⟩ f SPaths G p f SPaths G ⟨“ abc ”⟩
60 fveq1 p = ⟨“ abc ”⟩ p 0 = ⟨“ abc ”⟩ 0
61 60 eqeq2d p = ⟨“ abc ”⟩ a = p 0 a = ⟨“ abc ”⟩ 0
62 fveq1 p = ⟨“ abc ”⟩ p 1 = ⟨“ abc ”⟩ 1
63 62 eqeq2d p = ⟨“ abc ”⟩ b = p 1 b = ⟨“ abc ”⟩ 1
64 fveq1 p = ⟨“ abc ”⟩ p 2 = ⟨“ abc ”⟩ 2
65 64 eqeq2d p = ⟨“ abc ”⟩ c = p 2 c = ⟨“ abc ”⟩ 2
66 61 63 65 3anbi123d p = ⟨“ abc ”⟩ a = p 0 b = p 1 c = p 2 a = ⟨“ abc ”⟩ 0 b = ⟨“ abc ”⟩ 1 c = ⟨“ abc ”⟩ 2
67 59 66 3anbi13d p = ⟨“ abc ”⟩ f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 f SPaths G ⟨“ abc ”⟩ f = 2 a = ⟨“ abc ”⟩ 0 b = ⟨“ abc ”⟩ 1 c = ⟨“ abc ”⟩ 2
68 67 ad2antlr G UPGraph a V b V c V p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 f SPaths G ⟨“ abc ”⟩ f = 2 a = ⟨“ abc ”⟩ 0 b = ⟨“ abc ”⟩ 1 c = ⟨“ abc ”⟩ 2
69 58 68 mpbird G UPGraph a V b V c V p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
70 69 ex G UPGraph a V b V c V p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
71 28 70 spcimedv G UPGraph a V b V c V f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
72 spthiswlk f SPaths G p f Walks G p
73 wlklenvp1 f Walks G p p = f + 1
74 oveq1 f = 2 f + 1 = 2 + 1
75 2p1e3 2 + 1 = 3
76 74 75 syl6eq f = 2 f + 1 = 3
77 76 eqeq2d f = 2 p = f + 1 p = 3
78 77 biimpcd p = f + 1 f = 2 p = 3
79 72 73 78 3syl f SPaths G p f = 2 p = 3
80 79 imp f SPaths G p f = 2 p = 3
81 80 3adant3 f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = 3
82 81 adantl G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = 3
83 eqcom a = p 0 p 0 = a
84 eqcom b = p 1 p 1 = b
85 eqcom c = p 2 p 2 = c
86 83 84 85 3anbi123i a = p 0 b = p 1 c = p 2 p 0 = a p 1 = b p 2 = c
87 86 biimpi a = p 0 b = p 1 c = p 2 p 0 = a p 1 = b p 2 = c
88 87 3ad2ant3 f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p 0 = a p 1 = b p 2 = c
89 88 adantl G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p 0 = a p 1 = b p 2 = c
90 82 89 jca G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = 3 p 0 = a p 1 = b p 2 = c
91 1 wlkpwrd f Walks G p p Word V
92 72 91 syl f SPaths G p p Word V
93 92 3ad2ant1 f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p Word V
94 12 anim1i G UPGraph a V b V c V a V b V c V
95 3anass a V b V c V a V b V c V
96 94 95 sylibr G UPGraph a V b V c V a V b V c V
97 eqwrds3 p Word V a V b V c V p = ⟨“ abc ”⟩ p = 3 p 0 = a p 1 = b p 2 = c
98 93 96 97 syl2anr G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ p = 3 p 0 = a p 1 = b p 2 = c
99 90 98 mpbird G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩
100 59 biimpcd f SPaths G p p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩
101 100 3ad2ant1 f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩
102 101 adantl G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩
103 102 imp G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩
104 48 a1i G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a
105 fveq2 f = 2 ⟨“ abc ”⟩ f = ⟨“ abc ”⟩ 2
106 105 54 syl6eq f = 2 ⟨“ abc ”⟩ f = c
107 106 3ad2ant2 f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 ⟨“ abc ”⟩ f = c
108 107 ad2antlr G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ f = c
109 103 104 108 3jca G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c
110 wlkiswwlks1 G UPGraph f Walks G p p WWalks G
111 110 adantr G UPGraph a V f Walks G p p WWalks G
112 111 adantr G UPGraph a V b V c V f Walks G p p WWalks G
113 72 112 syl5com f SPaths G p G UPGraph a V b V c V p WWalks G
114 113 3ad2ant1 f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 G UPGraph a V b V c V p WWalks G
115 114 impcom G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p WWalks G
116 115 adantr G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ p WWalks G
117 eleq1 p = ⟨“ abc ”⟩ p WWalks G ⟨“ abc ”⟩ WWalks G
118 117 bicomd p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ WWalks G p WWalks G
119 118 adantl G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ WWalks G p WWalks G
120 116 119 mpbird G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ WWalks G
121 s3len ⟨“ abc ”⟩ = 3
122 df-3 3 = 2 + 1
123 121 122 eqtri ⟨“ abc ”⟩ = 2 + 1
124 120 123 jctir G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1
125 54 a1i G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ 2 = c
126 124 104 125 3jca G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
127 109 126 jca G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
128 99 127 mpdan G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
129 128 ex G UPGraph a V b V c V f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
130 129 exlimdv G UPGraph a V b V c V p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2 f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c
131 71 130 impbid G UPGraph a V b V c V f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
132 131 adantr G UPGraph a V b V c V W = ⟨“ abc ”⟩ f SPaths G ⟨“ abc ”⟩ ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ f = c ⟨“ abc ”⟩ WWalks G ⟨“ abc ”⟩ = 2 + 1 ⟨“ abc ”⟩ 0 = a ⟨“ abc ”⟩ 2 = c p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
133 27 132 bitrd G UPGraph a V b V c V W = ⟨“ abc ”⟩ f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
134 133 exbidv G UPGraph a V b V c V W = ⟨“ abc ”⟩ f f a SPathsOn G c ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
135 11 134 syl5bb G UPGraph a V b V c V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WWalksNOn G c f f a SPathsOn G c ⟨“ abc ”⟩ f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
136 8 135 syl5bb G UPGraph a V b V c V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
137 136 pm5.32da G UPGraph a V b V c V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c W = ⟨“ abc ”⟩ f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
138 137 2rexbidva G UPGraph a V b V c V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c b V c V W = ⟨“ abc ”⟩ f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
139 7 138 syl5bb G UPGraph a V c V b V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c b V c V W = ⟨“ abc ”⟩ f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
140 139 rexbidva G UPGraph a V c V b V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ a 2 WSPathsNOn G c a V b V c V W = ⟨“ abc ”⟩ f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2
141 3 6 140 3bitrd G UPGraph W 2 WSPathsN G a V b V c V W = ⟨“ abc ”⟩ f p f SPaths G p f = 2 a = p 0 b = p 1 c = p 2