This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ewlkinedg

Description: The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i 
|- I = ( iEdg ` G )
Assertion ewlkinedg 
|- ( ( F e. ( G EdgWalks S ) /\ K e. ( 1 ..^ ( # ` F ) ) ) -> S <_ ( # ` ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ewlksfval.i 
 |-  I = ( iEdg ` G )
2 1 ewlkprop 
 |-  ( F e. ( G EdgWalks S ) -> ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) )
3 fvoveq1 
 |-  ( k = K -> ( F ` ( k - 1 ) ) = ( F ` ( K - 1 ) ) )
4 3 fveq2d 
 |-  ( k = K -> ( I ` ( F ` ( k - 1 ) ) ) = ( I ` ( F ` ( K - 1 ) ) ) )
5 2fveq3 
 |-  ( k = K -> ( I ` ( F ` k ) ) = ( I ` ( F ` K ) ) )
6 4 5 ineq12d 
 |-  ( k = K -> ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) = ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) )
7 6 fveq2d 
 |-  ( k = K -> ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) = ( # ` ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) ) )
8 7 breq2d 
 |-  ( k = K -> ( S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) <-> S <_ ( # ` ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) ) ) )
9 8 rspccv 
 |-  ( A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) -> ( K e. ( 1 ..^ ( # ` F ) ) -> S <_ ( # ` ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) ) ) )
10 9 3ad2ant3 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) -> ( K e. ( 1 ..^ ( # ` F ) ) -> S <_ ( # ` ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) ) ) )
11 2 10 syl 
 |-  ( F e. ( G EdgWalks S ) -> ( K e. ( 1 ..^ ( # ` F ) ) -> S <_ ( # ` ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) ) ) )
12 11 imp 
 |-  ( ( F e. ( G EdgWalks S ) /\ K e. ( 1 ..^ ( # ` F ) ) ) -> S <_ ( # ` ( ( I ` ( F ` ( K - 1 ) ) ) i^i ( I ` ( F ` K ) ) ) ) )