Theorem wlkdlem1

Description: Lemma 1 for wlkd . (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	wlkd.p	|- ( ph -> P e. Word _V )
	wlkd.f	|- ( ph -> F e. Word _V )
	wlkd.l	|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
	wlkdlem1.v	|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )
Assertion	wlkdlem1	|- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )

Proof

Step	Hyp	Ref	Expression
1		wlkd.p	|- ( ph -> P e. Word _V )
2		wlkd.f	|- ( ph -> F e. Word _V )
3		wlkd.l	|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
4		wlkdlem1.v	|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )
5		wrdf	|- ( P e. Word _V -> P : ( 0 ..^ ( # ` P ) ) --> _V )
6	1 5	syl	|- ( ph -> P : ( 0 ..^ ( # ` P ) ) --> _V )
7	3	oveq2d	|- ( ph -> ( 0 ..^ ( # ` P ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
8		lencl	|- ( F e. Word _V -> ( # ` F ) e. NN0 )
9	2 8	syl	|- ( ph -> ( # ` F ) e. NN0 )
10	9	nn0zd	|- ( ph -> ( # ` F ) e. ZZ )
11		fzval3	|- ( ( # ` F ) e. ZZ -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
12	10 11	syl	|- ( ph -> ( 0 ... ( # ` F ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
13	7 12	eqtr4d	|- ( ph -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( # ` F ) ) )
14	13	feq2d	|- ( ph -> ( P : ( 0 ..^ ( # ` P ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> _V ) )
15		ssv	|- V C_ _V
16		fcdmssb	|- ( ( V C_ _V /\ A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V ) -> ( P : ( 0 ... ( # ` F ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> V ) )
17	15 4 16	sylancr	|- ( ph -> ( P : ( 0 ... ( # ` F ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> V ) )
18	14 17	bitrd	|- ( ph -> ( P : ( 0 ..^ ( # ` P ) ) --> _V <-> P : ( 0 ... ( # ` F ) ) --> V ) )
19	6 18	mpbid	|- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )