Metamath Proof Explorer


Theorem elwwlks2

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

Ref Expression
Hypothesis elwwlks2.v V = Vtx G
Assertion elwwlks2 G UPGraph W 2 WWalksN G a V b V c V W = ⟨“ abc ”⟩ f p f Walks 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 wwlksnwwlksnon W 2 WWalksN G a V c V W a 2 WWalksNOn G c
3 2 a1i G UPGraph W 2 WWalksN G a V c V W a 2 WWalksNOn G c
4 1 elwwlks2on G UPGraph a V c V W a 2 WWalksNOn G c b V W = ⟨“ abc ”⟩ f f Walks G W f = 2
5 4 3expb G UPGraph a V c V W a 2 WWalksNOn G c b V W = ⟨“ abc ”⟩ f f Walks G W f = 2
6 5 2rexbidva G UPGraph a V c V W a 2 WWalksNOn G c a V c V b V W = ⟨“ abc ”⟩ f f Walks G W f = 2
7 rexcom c V b V W = ⟨“ abc ”⟩ f f Walks G W f = 2 b V c V W = ⟨“ abc ”⟩ f f Walks G W f = 2
8 s3cli ⟨“ abc ”⟩ Word V
9 8 a1i G UPGraph a V b V c V W = ⟨“ abc ”⟩ ⟨“ abc ”⟩ Word V
10 simplr G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ W = ⟨“ abc ”⟩
11 simpr G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩
12 10 11 eqtr4d G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ W = p
13 12 breq2d G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G W f Walks G p
14 13 biimpd G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G W f Walks G p
15 14 com12 f Walks G W G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G p
16 15 adantr f Walks G W f = 2 G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G p
17 16 impcom G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G W f = 2 f Walks G p
18 simprr G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G W f = 2 f = 2
19 vex a V
20 s3fv0 a V ⟨“ abc ”⟩ 0 = a
21 20 eqcomd a V a = ⟨“ abc ”⟩ 0
22 19 21 mp1i p = ⟨“ abc ”⟩ a = ⟨“ abc ”⟩ 0
23 fveq1 p = ⟨“ abc ”⟩ p 0 = ⟨“ abc ”⟩ 0
24 22 23 eqtr4d p = ⟨“ abc ”⟩ a = p 0
25 vex b V
26 s3fv1 b V ⟨“ abc ”⟩ 1 = b
27 26 eqcomd b V b = ⟨“ abc ”⟩ 1
28 25 27 mp1i p = ⟨“ abc ”⟩ b = ⟨“ abc ”⟩ 1
29 fveq1 p = ⟨“ abc ”⟩ p 1 = ⟨“ abc ”⟩ 1
30 28 29 eqtr4d p = ⟨“ abc ”⟩ b = p 1
31 vex c V
32 s3fv2 c V ⟨“ abc ”⟩ 2 = c
33 32 eqcomd c V c = ⟨“ abc ”⟩ 2
34 31 33 mp1i p = ⟨“ abc ”⟩ c = ⟨“ abc ”⟩ 2
35 fveq1 p = ⟨“ abc ”⟩ p 2 = ⟨“ abc ”⟩ 2
36 34 35 eqtr4d p = ⟨“ abc ”⟩ c = p 2
37 24 30 36 3jca p = ⟨“ abc ”⟩ a = p 0 b = p 1 c = p 2
38 37 adantl G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ a = p 0 b = p 1 c = p 2
39 38 adantr G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G W f = 2 a = p 0 b = p 1 c = p 2
40 17 18 39 3jca G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G W f = 2 f Walks G p f = 2 a = p 0 b = p 1 c = p 2
41 40 ex G UPGraph a V b V c V W = ⟨“ abc ”⟩ p = ⟨“ abc ”⟩ f Walks G W f = 2 f Walks G p f = 2 a = p 0 b = p 1 c = p 2
42 9 41 spcimedv G UPGraph a V b V c V W = ⟨“ abc ”⟩ f Walks G W f = 2 p f Walks G p f = 2 a = p 0 b = p 1 c = p 2
43 wlklenvp1 f Walks G p p = f + 1
44 simpl p = f + 1 f = 2 p = f + 1
45 oveq1 f = 2 f + 1 = 2 + 1
46 45 adantl p = f + 1 f = 2 f + 1 = 2 + 1
47 44 46 eqtrd p = f + 1 f = 2 p = 2 + 1
48 47 adantl f Walks G p p = f + 1 f = 2 p = 2 + 1
49 2p1e3 2 + 1 = 3
50 48 49 syl6eq f Walks G p p = f + 1 f = 2 p = 3
51 50 exp32 f Walks G p p = f + 1 f = 2 p = 3
52 43 51 mpd f Walks G p f = 2 p = 3
53 52 adantr f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 p = 3
54 53 imp f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 p = 3
55 eqcom a = p 0 p 0 = a
56 55 biimpi a = p 0 p 0 = a
57 eqcom b = p 1 p 1 = b
58 57 biimpi b = p 1 p 1 = b
59 eqcom c = p 2 p 2 = c
60 59 biimpi c = p 2 p 2 = c
61 56 58 60 3anim123i a = p 0 b = p 1 c = p 2 p 0 = a p 1 = b p 2 = c
62 54 61 anim12i f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 p = 3 p 0 = a p 1 = b p 2 = c
63 1 wlkpwrd f Walks G p p Word V
64 simpr G UPGraph a V a V
65 64 anim1i G UPGraph a V b V c V a V b V c V
66 3anass a V b V c V a V b V c V
67 65 66 sylibr G UPGraph a V b V c V a V b V c V
68 67 adantr G UPGraph a V b V c V W = ⟨“ abc ”⟩ a V b V c V
69 63 68 anim12i f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ p Word V a V b V c V
70 69 ad2antrr f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 p Word V a V b V c V
71 eqwrds3 p Word V a V b V c V p = ⟨“ abc ”⟩ p = 3 p 0 = a p 1 = b p 2 = c
72 70 71 syl f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩ p = 3 p 0 = a p 1 = b p 2 = c
73 62 72 mpbird f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 p = ⟨“ abc ”⟩
74 simprr f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ W = ⟨“ abc ”⟩
75 74 ad2antrr f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 W = ⟨“ abc ”⟩
76 73 75 eqtr4d f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 p = W
77 76 breq2d f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 f Walks G p f Walks G W
78 77 biimpd f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 f Walks G p f Walks G W
79 simplr f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 f = 2
80 78 79 jctird f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 f Walks G p f Walks G W f = 2
81 80 exp41 f Walks G p G UPGraph a V b V c V W = ⟨“ abc ”⟩ f = 2 a = p 0 b = p 1 c = p 2 f Walks G p f Walks G W f = 2
82 81 com25 f Walks G p f Walks G p f = 2 a = p 0 b = p 1 c = p 2 G UPGraph a V b V c V W = ⟨“ abc ”⟩ f Walks G W f = 2
83 82 pm2.43i f Walks G p f = 2 a = p 0 b = p 1 c = p 2 G UPGraph a V b V c V W = ⟨“ abc ”⟩ f Walks G W f = 2
84 83 3imp f Walks G p f = 2 a = p 0 b = p 1 c = p 2 G UPGraph a V b V c V W = ⟨“ abc ”⟩ f Walks G W f = 2
85 84 com12 G UPGraph a V b V c V W = ⟨“ abc ”⟩ f Walks G p f = 2 a = p 0 b = p 1 c = p 2 f Walks G W f = 2
86 85 exlimdv G UPGraph a V b V c V W = ⟨“ abc ”⟩ p f Walks G p f = 2 a = p 0 b = p 1 c = p 2 f Walks G W f = 2
87 42 86 impbid G UPGraph a V b V c V W = ⟨“ abc ”⟩ f Walks G W f = 2 p f Walks G p f = 2 a = p 0 b = p 1 c = p 2
88 87 exbidv G UPGraph a V b V c V W = ⟨“ abc ”⟩ f f Walks G W f = 2 f p f Walks G p f = 2 a = p 0 b = p 1 c = p 2
89 88 pm5.32da G UPGraph a V b V c V W = ⟨“ abc ”⟩ f f Walks G W f = 2 W = ⟨“ abc ”⟩ f p f Walks G p f = 2 a = p 0 b = p 1 c = p 2
90 89 2rexbidva G UPGraph a V b V c V W = ⟨“ abc ”⟩ f f Walks G W f = 2 b V c V W = ⟨“ abc ”⟩ f p f Walks G p f = 2 a = p 0 b = p 1 c = p 2
91 7 90 syl5bb G UPGraph a V c V b V W = ⟨“ abc ”⟩ f f Walks G W f = 2 b V c V W = ⟨“ abc ”⟩ f p f Walks G p f = 2 a = p 0 b = p 1 c = p 2
92 91 rexbidva G UPGraph a V c V b V W = ⟨“ abc ”⟩ f f Walks G W f = 2 a V b V c V W = ⟨“ abc ”⟩ f p f Walks G p f = 2 a = p 0 b = p 1 c = p 2
93 3 6 92 3bitrd G UPGraph W 2 WWalksN G a V b V c V W = ⟨“ abc ”⟩ f p f Walks G p f = 2 a = p 0 b = p 1 c = p 2