Metamath Proof Explorer

Theorem 3wlkond

Description: A walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021) (Revised by AV, 24-Mar-2021)

Ref Expression
Hypotheses 3wlkd.p 
|- P = <" A B C D ">
3wlkd.f 
|- F = <" J K L ">
3wlkd.s 
|- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
3wlkd.n 
|- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
3wlkd.e 
|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )
3wlkd.v 
|- V = ( Vtx ` G )
3wlkd.i 
|- I = ( iEdg ` G )
Assertion 3wlkond 
|- ( ph -> F ( A ( WalksOn ` G ) D ) P )

Proof

Step Hyp Ref Expression
1 3wlkd.p 
 |-  P = <" A B C D ">
2 3wlkd.f 
 |-  F = <" J K L ">
3 3wlkd.s 
 |-  ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
4 3wlkd.n 
 |-  ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
5 3wlkd.e 
 |-  ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )
6 3wlkd.v 
 |-  V = ( Vtx ` G )
7 3wlkd.i 
 |-  I = ( iEdg ` G )
8 1 2 3 4 5 6 7 3wlkd 
 |-  ( ph -> F ( Walks ` G ) P )
9 8 wlkonwlk1l 
 |-  ( ph -> F ( ( P ` 0 ) ( WalksOn ` G ) ( lastS ` P ) ) P )
10 1 2 3 3wlkdlem3 
 |-  ( ph -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) )
11 simpll 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( P ` 0 ) = A )
12 11 eqcomd 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> A = ( P ` 0 ) )
13 10 12 syl 
 |-  ( ph -> A = ( P ` 0 ) )
14 1 fveq2i 
 |-  ( lastS ` P ) = ( lastS ` <" A B C D "> )
15 fvex 
 |-  ( P ` 3 ) e. _V
16 eleq1 
 |-  ( ( P ` 3 ) = D -> ( ( P ` 3 ) e. _V <-> D e. _V ) )
17 15 16 mpbii 
 |-  ( ( P ` 3 ) = D -> D e. _V )
18 lsws4 
 |-  ( D e. _V -> ( lastS ` <" A B C D "> ) = D )
19 17 18 syl 
 |-  ( ( P ` 3 ) = D -> ( lastS ` <" A B C D "> ) = D )
20 14 19 eqtr2id 
 |-  ( ( P ` 3 ) = D -> D = ( lastS ` P ) )
21 20 ad2antll 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> D = ( lastS ` P ) )
22 10 21 syl 
 |-  ( ph -> D = ( lastS ` P ) )
23 13 22 oveq12d 
 |-  ( ph -> ( A ( WalksOn ` G ) D ) = ( ( P ` 0 ) ( WalksOn ` G ) ( lastS ` P ) ) )
24 23 breqd 
 |-  ( ph -> ( F ( A ( WalksOn ` G ) D ) P <-> F ( ( P ` 0 ) ( WalksOn ` G ) ( lastS ` P ) ) P ) )
25 9 24 mpbird 
 |-  ( ph -> F ( A ( WalksOn ` G ) D ) P )