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 ) ) ) ) )