Metamath Proof Explorer

Theorem wwlks2onv

Description: If a length 3 string represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Proof shortened by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlks2onv.v 
|- V = ( Vtx ` G )
Assertion wwlks2onv 
|- ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( A e. V /\ B e. V /\ C e. V ) )

Proof

Step Hyp Ref Expression
1 wwlks2onv.v 
 |-  V = ( Vtx ` G )
2 1 wwlksonvtx 
 |-  ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) -> ( A e. V /\ C e. V ) )
3 2 adantl 
 |-  ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( A e. V /\ C e. V ) )
4 simprl 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> A e. V )
5 wwlknon 
 |-  ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) <-> ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) )
6 wwlknbp1 
 |-  ( <" A B C "> e. ( 2 WWalksN G ) -> ( 2 e. NN0 /\ <" A B C "> e. Word ( Vtx ` G ) /\ ( # ` <" A B C "> ) = ( 2 + 1 ) ) )
7 s3fv1 
 |-  ( B e. U -> ( <" A B C "> ` 1 ) = B )
8 7 eqcomd 
 |-  ( B e. U -> B = ( <" A B C "> ` 1 ) )
9 8 adantl 
 |-  ( ( <" A B C "> e. Word ( Vtx ` G ) /\ B e. U ) -> B = ( <" A B C "> ` 1 ) )
10 1 eqcomi 
 |-  ( Vtx ` G ) = V
11 10 wrdeqi 
 |-  Word ( Vtx ` G ) = Word V
12 11 eleq2i 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) <-> <" A B C "> e. Word V )
13 12 biimpi 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) -> <" A B C "> e. Word V )
14 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
15 s3len 
 |-  ( # ` <" A B C "> ) = 3
16 15 oveq2i 
 |-  ( 0 ..^ ( # ` <" A B C "> ) ) = ( 0 ..^ 3 )
17 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
18 16 17 eqtri 
 |-  ( 0 ..^ ( # ` <" A B C "> ) ) = { 0 , 1 , 2 }
19 14 18 eleqtrri 
 |-  1 e. ( 0 ..^ ( # ` <" A B C "> ) )
20 wrdsymbcl 
 |-  ( ( <" A B C "> e. Word V /\ 1 e. ( 0 ..^ ( # ` <" A B C "> ) ) ) -> ( <" A B C "> ` 1 ) e. V )
21 13 19 20 sylancl 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) -> ( <" A B C "> ` 1 ) e. V )
22 21 adantr 
 |-  ( ( <" A B C "> e. Word ( Vtx ` G ) /\ B e. U ) -> ( <" A B C "> ` 1 ) e. V )
23 9 22 eqeltrd 
 |-  ( ( <" A B C "> e. Word ( Vtx ` G ) /\ B e. U ) -> B e. V )
24 23 ex 
 |-  ( <" A B C "> e. Word ( Vtx ` G ) -> ( B e. U -> B e. V ) )
25 24 3ad2ant2 
 |-  ( ( 2 e. NN0 /\ <" A B C "> e. Word ( Vtx ` G ) /\ ( # ` <" A B C "> ) = ( 2 + 1 ) ) -> ( B e. U -> B e. V ) )
26 6 25 syl 
 |-  ( <" A B C "> e. ( 2 WWalksN G ) -> ( B e. U -> B e. V ) )
27 26 3ad2ant1 
 |-  ( ( <" A B C "> e. ( 2 WWalksN G ) /\ ( <" A B C "> ` 0 ) = A /\ ( <" A B C "> ` 2 ) = C ) -> ( B e. U -> B e. V ) )
28 5 27 sylbi 
 |-  ( <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) -> ( B e. U -> B e. V ) )
29 28 impcom 
 |-  ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> B e. V )
30 29 adantr 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> B e. V )
31 simprr 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> C e. V )
32 4 30 31 3jca 
 |-  ( ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) /\ ( A e. V /\ C e. V ) ) -> ( A e. V /\ B e. V /\ C e. V ) )
33 3 32 mpdan 
 |-  ( ( B e. U /\ <" A B C "> e. ( A ( 2 WWalksNOn G ) C ) ) -> ( A e. V /\ B e. V /\ C e. V ) )