Metamath Proof Explorer


Theorem elwwlks2ons3im

Description: A walk as word of length 2 between two vertices is a length 3 string and its second symbol is a vertex. (Contributed by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlks2onv.v V = Vtx G
Assertion elwwlks2ons3im W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V

Proof

Step Hyp Ref Expression
1 wwlks2onv.v V = Vtx G
2 1 wwlksonvtx W A 2 WWalksNOn G C A V C V
3 wwlknon W A 2 WWalksNOn G C W 2 WWalksN G W 0 = A W 2 = C
4 wwlknbp1 W 2 WWalksN G 2 0 W Word Vtx G W = 2 + 1
5 2p1e3 2 + 1 = 3
6 5 eqeq2i W = 2 + 1 W = 3
7 1ex 1 V
8 7 tpid2 1 0 1 2
9 fzo0to3tp 0 ..^ 3 = 0 1 2
10 8 9 eleqtrri 1 0 ..^ 3
11 oveq2 W = 3 0 ..^ W = 0 ..^ 3
12 10 11 eleqtrrid W = 3 1 0 ..^ W
13 wrdsymbcl W Word Vtx G 1 0 ..^ W W 1 Vtx G
14 12 13 sylan2 W Word Vtx G W = 3 W 1 Vtx G
15 14 3ad2ant1 W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G
16 simpl1r W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G W = 3
17 simpl W 0 = A W 2 = C W 0 = A
18 eqidd W 0 = A W 2 = C W 1 = W 1
19 simpr W 0 = A W 2 = C W 2 = C
20 17 18 19 3jca W 0 = A W 2 = C W 0 = A W 1 = W 1 W 2 = C
21 20 3ad2ant2 W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 0 = A W 1 = W 1 W 2 = C
22 21 adantr W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G W 0 = A W 1 = W 1 W 2 = C
23 1 eqcomi Vtx G = V
24 23 wrdeqi Word Vtx G = Word V
25 24 eleq2i W Word Vtx G W Word V
26 25 biimpi W Word Vtx G W Word V
27 26 adantr W Word Vtx G W = 3 W Word V
28 27 3ad2ant1 W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W Word V
29 28 adantr W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G W Word V
30 simpl3l W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G A V
31 23 eleq2i W 1 Vtx G W 1 V
32 31 biimpi W 1 Vtx G W 1 V
33 32 adantl W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G W 1 V
34 simpl3r W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G C V
35 eqwrds3 W Word V A V W 1 V C V W = ⟨“ A W 1 C ”⟩ W = 3 W 0 = A W 1 = W 1 W 2 = C
36 29 30 33 34 35 syl13anc W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G W = ⟨“ A W 1 C ”⟩ W = 3 W 0 = A W 1 = W 1 W 2 = C
37 16 22 36 mpbir2and W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G W = ⟨“ A W 1 C ”⟩
38 37 33 jca W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W 1 Vtx G W = ⟨“ A W 1 C ”⟩ W 1 V
39 15 38 mpdan W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W = ⟨“ A W 1 C ”⟩ W 1 V
40 39 3exp W Word Vtx G W = 3 W 0 = A W 2 = C A V C V W = ⟨“ A W 1 C ”⟩ W 1 V
41 6 40 sylan2b W Word Vtx G W = 2 + 1 W 0 = A W 2 = C A V C V W = ⟨“ A W 1 C ”⟩ W 1 V
42 41 3adant1 2 0 W Word Vtx G W = 2 + 1 W 0 = A W 2 = C A V C V W = ⟨“ A W 1 C ”⟩ W 1 V
43 4 42 syl W 2 WWalksN G W 0 = A W 2 = C A V C V W = ⟨“ A W 1 C ”⟩ W 1 V
44 43 3impib W 2 WWalksN G W 0 = A W 2 = C A V C V W = ⟨“ A W 1 C ”⟩ W 1 V
45 3 44 sylbi W A 2 WWalksNOn G C A V C V W = ⟨“ A W 1 C ”⟩ W 1 V
46 2 45 mpd W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V