Metamath Proof Explorer

Theorem 1ewlk

Description: A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021)

Ref Expression
Assertion 1ewlk 
|- ( ( G e. _V /\ S e. NN0* /\ I e. dom ( iEdg ` G ) ) -> <" I "> e. ( G EdgWalks S ) )

Proof

Step Hyp Ref Expression
1 s1cl 
 |-  ( I e. dom ( iEdg ` G ) -> <" I "> e. Word dom ( iEdg ` G ) )
2 1 3ad2ant3 
 |-  ( ( G e. _V /\ S e. NN0* /\ I e. dom ( iEdg ` G ) ) -> <" I "> e. Word dom ( iEdg ` G ) )
3 ral0 
 |-  A. k e. (/) S <_ ( # ` ( ( ( iEdg ` G ) ` ( <" I "> ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( <" I "> ` k ) ) ) )
4 s1len 
 |-  ( # ` <" I "> ) = 1
5 4 oveq2i 
 |-  ( 1 ..^ ( # ` <" I "> ) ) = ( 1 ..^ 1 )
6 fzo0 
 |-  ( 1 ..^ 1 ) = (/)
7 5 6 eqtri 
 |-  ( 1 ..^ ( # ` <" I "> ) ) = (/)
8 7 a1i 
 |-  ( I e. dom ( iEdg ` G ) -> ( 1 ..^ ( # ` <" I "> ) ) = (/) )
9 8 raleqdv 
 |-  ( I e. dom ( iEdg ` G ) -> ( A. k e. ( 1 ..^ ( # ` <" I "> ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( <" I "> ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( <" I "> ` k ) ) ) ) <-> A. k e. (/) S <_ ( # ` ( ( ( iEdg ` G ) ` ( <" I "> ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( <" I "> ` k ) ) ) ) ) )
10 3 9 mpbiri 
 |-  ( I e. dom ( iEdg ` G ) -> A. k e. ( 1 ..^ ( # ` <" I "> ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( <" I "> ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( <" I "> ` k ) ) ) ) )
11 10 3ad2ant3 
 |-  ( ( G e. _V /\ S e. NN0* /\ I e. dom ( iEdg ` G ) ) -> A. k e. ( 1 ..^ ( # ` <" I "> ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( <" I "> ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( <" I "> ` k ) ) ) ) )
12 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
13 12 isewlk 
 |-  ( ( G e. _V /\ S e. NN0* /\ <" I "> e. Word dom ( iEdg ` G ) ) -> ( <" I "> e. ( G EdgWalks S ) <-> ( <" I "> e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` <" I "> ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( <" I "> ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( <" I "> ` k ) ) ) ) ) ) )
14 1 13 syl3an3 
 |-  ( ( G e. _V /\ S e. NN0* /\ I e. dom ( iEdg ` G ) ) -> ( <" I "> e. ( G EdgWalks S ) <-> ( <" I "> e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` <" I "> ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( <" I "> ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( <" I "> ` k ) ) ) ) ) ) )
15 2 11 14 mpbir2and 
 |-  ( ( G e. _V /\ S e. NN0* /\ I e. dom ( iEdg ` G ) ) -> <" I "> e. ( G EdgWalks S ) )