Theorem wlkiswwlks2lem3

Description: Lemma 3 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	wlkiswwlks2lem3	|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )

Proof

Step	Hyp	Ref	Expression
1		wlkiswwlks2lem.f	|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) )
2	1	wlkiswwlks2lem1	|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
3		wrdf	|- ( P e. Word V -> P : ( 0 ..^ ( # ` P ) ) --> V )
4		lencl	|- ( P e. Word V -> ( # ` P ) e. NN0 )
5		nn0z	|- ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ )
6		fzoval	|- ( ( # ` P ) e. ZZ -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) )
7	5 6	syl	|- ( ( # ` P ) e. NN0 -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) )
8		oveq2	|- ( ( ( # ` P ) - 1 ) = ( # ` F ) -> ( 0 ... ( ( # ` P ) - 1 ) ) = ( 0 ... ( # ` F ) ) )
9	8	eqcoms	|- ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( 0 ... ( ( # ` P ) - 1 ) ) = ( 0 ... ( # ` F ) ) )
10	7 9	sylan9eq	|- ( ( ( # ` P ) e. NN0 /\ ( # ` F ) = ( ( # ` P ) - 1 ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( # ` F ) ) )
11	10	feq2d	|- ( ( ( # ` P ) e. NN0 /\ ( # ` F ) = ( ( # ` P ) - 1 ) ) -> ( P : ( 0 ..^ ( # ` P ) ) --> V <-> P : ( 0 ... ( # ` F ) ) --> V ) )
12	11	biimpcd	|- ( P : ( 0 ..^ ( # ` P ) ) --> V -> ( ( ( # ` P ) e. NN0 /\ ( # ` F ) = ( ( # ` P ) - 1 ) ) -> P : ( 0 ... ( # ` F ) ) --> V ) )
13	12	expd	|- ( P : ( 0 ..^ ( # ` P ) ) --> V -> ( ( # ` P ) e. NN0 -> ( ( # ` F ) = ( ( # ` P ) - 1 ) -> P : ( 0 ... ( # ` F ) ) --> V ) ) )
14	3 4 13	sylc	|- ( P e. Word V -> ( ( # ` F ) = ( ( # ` P ) - 1 ) -> P : ( 0 ... ( # ` F ) ) --> V ) )
15	14	adantr	|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( # ` F ) = ( ( # ` P ) - 1 ) -> P : ( 0 ... ( # ` F ) ) --> V ) )
16	2 15	mpd	|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )