Theorem clwlkclwwlklem2a3

Description: Lemma 3 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlklem2.f	|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )
2		lsw	|- ( P e. Word V -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
3	2	adantr	|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
4	1	clwlkclwwlklem2a2	|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
5	4	eqcomd	|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) = ( # ` F ) )
6	5	fveq2d	|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` ( # ` F ) ) )
7	3 6	eqtr2d	|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` ( # ` F ) ) = ( lastS ` P ) )