Metamath Proof Explorer

Theorem wlkiswwlks2lem1

Description: Lemma 1 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

Ref Expression
Hypothesis wlkiswwlks2lem.f 
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )
Assertion wlkiswwlks2lem1 
|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )

Proof

Step Hyp Ref Expression
1 wlkiswwlks2lem.f 
 |-  F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )
2 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
3 elnnnn0c 
 |-  ( ( # ` P ) e. NN <-> ( ( # ` P ) e. NN0 /\ 1 <_ ( # ` P ) ) )
4 3 biimpri 
 |-  ( ( ( # ` P ) e. NN0 /\ 1 <_ ( # ` P ) ) -> ( # ` P ) e. NN )
5 2 4 sylan 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` P ) e. NN )
6 nnm1nn0 
 |-  ( ( # ` P ) e. NN -> ( ( # ` P ) - 1 ) e. NN0 )
7 5 6 syl 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. NN0 )
8 fvex 
 |-  ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. _V
9 8 1 fnmpti 
 |-  F Fn ( 0 ..^ ( ( # ` P ) - 1 ) )
10 ffzo0hash 
 |-  ( ( ( ( # ` P ) - 1 ) e. NN0 /\ F Fn ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
11 7 9 10 sylancl 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )