Metamath Proof Explorer


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 frnssb
 |-  ( ( 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 )