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∈A2WWalksNOnGC→W=⟨“AW⁡1C”⟩∧W⁡1∈V

Proof

Step Hyp Ref Expression
1 wwlks2onv.v ⊢V=Vtx⁡G
2 1 wwlksonvtx ⊢W∈A2WWalksNOnGC→A∈V∧C∈V
3 wwlknon ⊢W∈A2WWalksNOnGC↔W∈2WWalksNG∧W⁡0=A∧W⁡2=C
4 wwlknbp1 ⊢W∈2WWalksNG→2∈ℕ0∧W∈WordVtx⁡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∈012
9 fzo0to3tp ⊢0..^3=012
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∈WordVtx⁡G∧1∈0..^W→W⁡1∈Vtx⁡G
14 12 13 sylan2 ⊢W∈WordVtx⁡G∧W=3→W⁡1∈Vtx⁡G
15 14 3ad2ant1 ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V→W⁡1∈Vtx⁡G
16 simpl1r ⊢W∈WordVtx⁡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∈WordVtx⁡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∈WordVtx⁡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 ⊢WordVtx⁡G=WordV
25 24 eleq2i ⊢W∈WordVtx⁡G↔W∈WordV
26 25 biimpi ⊢W∈WordVtx⁡G→W∈WordV
27 26 adantr ⊢W∈WordVtx⁡G∧W=3→W∈WordV
28 27 3ad2ant1 ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V→W∈WordV
29 28 adantr ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V∧W⁡1∈Vtx⁡G→W∈WordV
30 simpl3l ⊢W∈WordVtx⁡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∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V∧W⁡1∈Vtx⁡G→W⁡1∈V
34 simpl3r ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V∧W⁡1∈Vtx⁡G→C∈V
35 eqwrds3 ⊢W∈WordV∧A∈V∧W⁡1∈V∧C∈V→W=⟨“AW⁡1C”⟩↔W=3∧W⁡0=A∧W⁡1=W⁡1∧W⁡2=C
36 29 30 33 34 35 syl13anc ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V∧W⁡1∈Vtx⁡G→W=⟨“AW⁡1C”⟩↔W=3∧W⁡0=A∧W⁡1=W⁡1∧W⁡2=C
37 16 22 36 mpbir2and ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V∧W⁡1∈Vtx⁡G→W=⟨“AW⁡1C”⟩
38 37 33 jca ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V∧W⁡1∈Vtx⁡G→W=⟨“AW⁡1C”⟩∧W⁡1∈V
39 15 38 mpdan ⊢W∈WordVtx⁡G∧W=3∧W⁡0=A∧W⁡2=C∧A∈V∧C∈V→W=⟨“AW⁡1C”⟩∧W⁡1∈V
40 39 3exp ⊢W∈WordVtx⁡G∧W=3→W⁡0=A∧W⁡2=C→A∈V∧C∈V→W=⟨“AW⁡1C”⟩∧W⁡1∈V
41 6 40 sylan2b ⊢W∈WordVtx⁡G∧W=2+1→W⁡0=A∧W⁡2=C→A∈V∧C∈V→W=⟨“AW⁡1C”⟩∧W⁡1∈V
42 41 3adant1 ⊢2∈ℕ0∧W∈WordVtx⁡G∧W=2+1→W⁡0=A∧W⁡2=C→A∈V∧C∈V→W=⟨“AW⁡1C”⟩∧W⁡1∈V
43 4 42 syl ⊢W∈2WWalksNG→W⁡0=A∧W⁡2=C→A∈V∧C∈V→W=⟨“AW⁡1C”⟩∧W⁡1∈V
44 43 3impib ⊢W∈2WWalksNG∧W⁡0=A∧W⁡2=C→A∈V∧C∈V→W=⟨“AW⁡1C”⟩∧W⁡1∈V
45 3 44 sylbi ⊢W∈A2WWalksNOnGC→A∈V∧C∈V→W=⟨“AW⁡1C”⟩∧W⁡1∈V
46 2 45 mpd ⊢W∈A2WWalksNOnGC→W=⟨“AW⁡1C”⟩∧W⁡1∈V