Metamath Proof Explorer

Theorem wlkdlem2

Description: Lemma 2 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 ) )
wlkd.e 
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
Assertion wlkdlem2 
|- ( ph -> ( ( ( # ` F ) e. NN -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) ) )

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 wlkd.e 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
5 fzo0end 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
6 fveq2 
 |-  ( k = ( ( # ` F ) - 1 ) -> ( P ` k ) = ( P ` ( ( # ` F ) - 1 ) ) )
7 fvoveq1 
 |-  ( k = ( ( # ` F ) - 1 ) -> ( P ` ( k + 1 ) ) = ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) )
8 6 7 preq12d 
 |-  ( k = ( ( # ` F ) - 1 ) -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } )
9 2fveq3 
 |-  ( k = ( ( # ` F ) - 1 ) -> ( I ` ( F ` k ) ) = ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) )
10 8 9 sseq12d 
 |-  ( k = ( ( # ` F ) - 1 ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) <-> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } C_ ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
11 10 rspcv 
 |-  ( ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } C_ ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
12 5 11 syl 
 |-  ( ( # ` F ) e. NN -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } C_ ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
13 fvex 
 |-  ( P ` ( ( # ` F ) - 1 ) ) e. _V
14 fvex 
 |-  ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) e. _V
15 13 14 prss 
 |-  ( ( ( P ` ( ( # ` F ) - 1 ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) /\ ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) <-> { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } C_ ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) )
16 nncn 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. CC )
17 npcan1 
 |-  ( ( # ` F ) e. CC -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
18 16 17 syl 
 |-  ( ( # ` F ) e. NN -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
19 18 fveq2d 
 |-  ( ( # ` F ) e. NN -> ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) = ( P ` ( # ` F ) ) )
20 19 eleq1d 
 |-  ( ( # ` F ) e. NN -> ( ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) <-> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
21 20 biimpd 
 |-  ( ( # ` F ) e. NN -> ( ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
22 21 adantld 
 |-  ( ( # ` F ) e. NN -> ( ( ( P ` ( ( # ` F ) - 1 ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) /\ ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
23 15 22 syl5bir 
 |-  ( ( # ` F ) e. NN -> ( { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` ( ( ( # ` F ) - 1 ) + 1 ) ) } C_ ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
24 12 23 syld 
 |-  ( ( # ` F ) e. NN -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
25 4 24 syl5com 
 |-  ( ph -> ( ( # ` F ) e. NN -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) )
26 fvex 
 |-  ( P ` k ) e. _V
27 fvex 
 |-  ( P ` ( k + 1 ) ) e. _V
28 26 27 prss 
 |-  ( ( ( P ` k ) e. ( I ` ( F ` k ) ) /\ ( P ` ( k + 1 ) ) e. ( I ` ( F ` k ) ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
29 simpl 
 |-  ( ( ( P ` k ) e. ( I ` ( F ` k ) ) /\ ( P ` ( k + 1 ) ) e. ( I ` ( F ` k ) ) ) -> ( P ` k ) e. ( I ` ( F ` k ) ) )
30 28 29 sylbir 
 |-  ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> ( P ` k ) e. ( I ` ( F ` k ) ) )
31 30 a1i 
 |-  ( ( ph /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> ( P ` k ) e. ( I ` ( F ` k ) ) ) )
32 31 ralimdva 
 |-  ( ph -> ( A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) ) )
33 4 32 mpd 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) )
34 25 33 jca 
 |-  ( ph -> ( ( ( # ` F ) e. NN -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) ) )