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 e. ( A ( 2 WWalksNOn G ) C ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) )

Proof

Step Hyp Ref Expression
1 wwlks2onv.v 
 |-  V = ( Vtx ` G )
2 1 wwlksonvtx 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) -> ( A e. V /\ C e. V ) )
3 wwlknon 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) <-> ( W e. ( 2 WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` 2 ) = C ) )
4 wwlknbp1 
 |-  ( W e. ( 2 WWalksN G ) -> ( 2 e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( 2 + 1 ) ) )
5 2p1e3 
 |-  ( 2 + 1 ) = 3
6 5 eqeq2i 
 |-  ( ( # ` W ) = ( 2 + 1 ) <-> ( # ` W ) = 3 )
7 1ex 
 |-  1 e. _V
8 7 tpid2 
 |-  1 e. { 0 , 1 , 2 }
9 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10 8 9 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
11 oveq2 
 |-  ( ( # ` W ) = 3 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 3 ) )
12 10 11 eleqtrrid 
 |-  ( ( # ` W ) = 3 -> 1 e. ( 0 ..^ ( # ` W ) ) )
13 wrdsymbcl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` 1 ) e. ( Vtx ` G ) )
14 12 13 sylan2 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) -> ( W ` 1 ) e. ( Vtx ` G ) )
15 14 3ad2ant1 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) -> ( W ` 1 ) e. ( Vtx ` G ) )
16 simpl1r 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( 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 e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) -> ( ( W ` 0 ) = A /\ ( W ` 1 ) = ( W ` 1 ) /\ ( W ` 2 ) = C ) )
22 21 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( 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 e. Word ( Vtx ` G ) <-> W e. Word V )
26 25 biimpi 
 |-  ( W e. Word ( Vtx ` G ) -> W e. Word V )
27 26 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) -> W e. Word V )
28 27 3ad2ant1 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) -> W e. Word V )
29 28 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( Vtx ` G ) ) -> W e. Word V )
30 simpl3l 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( Vtx ` G ) ) -> A e. V )
31 23 eleq2i 
 |-  ( ( W ` 1 ) e. ( Vtx ` G ) <-> ( W ` 1 ) e. V )
32 31 biimpi 
 |-  ( ( W ` 1 ) e. ( Vtx ` G ) -> ( W ` 1 ) e. V )
33 32 adantl 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( Vtx ` G ) ) -> ( W ` 1 ) e. V )
34 simpl3r 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( Vtx ` G ) ) -> C e. V )
35 eqwrds3 
 |-  ( ( W e. Word V /\ ( A e. V /\ ( W ` 1 ) e. V /\ C e. 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 e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( 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 e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( Vtx ` G ) ) -> W = <" A ( W ` 1 ) C "> )
38 37 33 jca 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) /\ ( W ` 1 ) e. ( Vtx ` G ) ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) )
39 15 38 mpdan 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) /\ ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) /\ ( A e. V /\ C e. V ) ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) )
40 39 3exp 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = 3 ) -> ( ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) -> ( ( A e. V /\ C e. V ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) ) ) )
41 6 40 sylan2b 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( 2 + 1 ) ) -> ( ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) -> ( ( A e. V /\ C e. V ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) ) ) )
42 41 3adant1 
 |-  ( ( 2 e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( 2 + 1 ) ) -> ( ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) -> ( ( A e. V /\ C e. V ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) ) ) )
43 4 42 syl 
 |-  ( W e. ( 2 WWalksN G ) -> ( ( ( W ` 0 ) = A /\ ( W ` 2 ) = C ) -> ( ( A e. V /\ C e. V ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) ) ) )
44 43 3impib 
 |-  ( ( W e. ( 2 WWalksN G ) /\ ( W ` 0 ) = A /\ ( W ` 2 ) = C ) -> ( ( A e. V /\ C e. V ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) ) )
45 3 44 sylbi 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) -> ( ( A e. V /\ C e. V ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) ) )
46 2 45 mpd 
 |-  ( W e. ( A ( 2 WWalksNOn G ) C ) -> ( W = <" A ( W ` 1 ) C "> /\ ( W ` 1 ) e. V ) )