Metamath Proof Explorer

Theorem crctcshwlkn0lem7

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s 
|- ( ph -> S e. ( 1 ..^ N ) )
crctcshwlkn0lem.q 
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
crctcshwlkn0lem.h 
|- H = ( F cyclShift S )
crctcshwlkn0lem.n 
|- N = ( # ` F )
crctcshwlkn0lem.f 
|- ( ph -> F e. Word A )
crctcshwlkn0lem.p 
|- ( ph -> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
crctcshwlkn0lem.e 
|- ( ph -> ( P ` N ) = ( P ` 0 ) )
Assertion crctcshwlkn0lem7 
|- ( ph -> A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s 
 |-  ( ph -> S e. ( 1 ..^ N ) )
2 crctcshwlkn0lem.q 
 |-  Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
3 crctcshwlkn0lem.h 
 |-  H = ( F cyclShift S )
4 crctcshwlkn0lem.n 
 |-  N = ( # ` F )
5 crctcshwlkn0lem.f 
 |-  ( ph -> F e. Word A )
6 crctcshwlkn0lem.p 
 |-  ( ph -> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
7 crctcshwlkn0lem.e 
 |-  ( ph -> ( P ` N ) = ( P ` 0 ) )
8 1 2 3 4 5 6 crctcshwlkn0lem4 
 |-  ( ph -> A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
9 eqidd 
 |-  ( ph -> ( N - S ) = ( N - S ) )
10 1 2 3 4 5 6 7 crctcshwlkn0lem6 
 |-  ( ( ph /\ ( N - S ) = ( N - S ) ) -> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) )
11 9 10 mpdan 
 |-  ( ph -> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) )
12 ovex 
 |-  ( N - S ) e. _V
13 wkslem1 
 |-  ( j = ( N - S ) -> ( if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) ) )
14 12 13 ralsn 
 |-  ( A. j e. { ( N - S ) } if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) )
15 11 14 sylibr 
 |-  ( ph -> A. j e. { ( N - S ) } if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
16 ralunb 
 |-  ( A. j e. ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> ( A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) /\ A. j e. { ( N - S ) } if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
17 8 15 16 sylanbrc 
 |-  ( ph -> A. j e. ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
18 elfzo1 
 |-  ( S e. ( 1 ..^ N ) <-> ( S e. NN /\ N e. NN /\ S < N ) )
19 nnz 
 |-  ( N e. NN -> N e. ZZ )
20 nnz 
 |-  ( S e. NN -> S e. ZZ )
21 zsubcl 
 |-  ( ( N e. ZZ /\ S e. ZZ ) -> ( N - S ) e. ZZ )
22 19 20 21 syl2anr 
 |-  ( ( S e. NN /\ N e. NN ) -> ( N - S ) e. ZZ )
23 22 3adant3 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. ZZ )
24 nnre 
 |-  ( S e. NN -> S e. RR )
25 nnre 
 |-  ( N e. NN -> N e. RR )
26 posdif 
 |-  ( ( S e. RR /\ N e. RR ) -> ( S < N <-> 0 < ( N - S ) ) )
27 0re 
 |-  0 e. RR
28 resubcl 
 |-  ( ( N e. RR /\ S e. RR ) -> ( N - S ) e. RR )
29 28 ancoms 
 |-  ( ( S e. RR /\ N e. RR ) -> ( N - S ) e. RR )
30 ltle 
 |-  ( ( 0 e. RR /\ ( N - S ) e. RR ) -> ( 0 < ( N - S ) -> 0 <_ ( N - S ) ) )
31 27 29 30 sylancr 
 |-  ( ( S e. RR /\ N e. RR ) -> ( 0 < ( N - S ) -> 0 <_ ( N - S ) ) )
32 26 31 sylbid 
 |-  ( ( S e. RR /\ N e. RR ) -> ( S < N -> 0 <_ ( N - S ) ) )
33 24 25 32 syl2an 
 |-  ( ( S e. NN /\ N e. NN ) -> ( S < N -> 0 <_ ( N - S ) ) )
34 33 3impia 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> 0 <_ ( N - S ) )
35 elnn0z 
 |-  ( ( N - S ) e. NN0 <-> ( ( N - S ) e. ZZ /\ 0 <_ ( N - S ) ) )
36 23 34 35 sylanbrc 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. NN0 )
37 elnn0uz 
 |-  ( ( N - S ) e. NN0 <-> ( N - S ) e. ( ZZ>= ` 0 ) )
38 36 37 sylib 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. ( ZZ>= ` 0 ) )
39 fzosplitsn 
 |-  ( ( N - S ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) )
40 38 39 syl 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) )
41 18 40 sylbi 
 |-  ( S e. ( 1 ..^ N ) -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) )
42 1 41 syl 
 |-  ( ph -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) )
43 42 raleqdv 
 |-  ( ph -> ( A. j e. ( 0 ..^ ( ( N - S ) + 1 ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> A. j e. ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
44 17 43 mpbird 
 |-  ( ph -> A. j e. ( 0 ..^ ( ( N - S ) + 1 ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
45 1 2 3 4 5 6 crctcshwlkn0lem5 
 |-  ( ph -> A. j e. ( ( ( N - S ) + 1 ) ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
46 ralunb 
 |-  ( A. j e. ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> ( A. j e. ( 0 ..^ ( ( N - S ) + 1 ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) /\ A. j e. ( ( ( N - S ) + 1 ) ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
47 44 45 46 sylanbrc 
 |-  ( ph -> A. j e. ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
48 nnsub 
 |-  ( ( S e. NN /\ N e. NN ) -> ( S < N <-> ( N - S ) e. NN ) )
49 48 biimp3a 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. NN )
50 nnnn0 
 |-  ( ( N - S ) e. NN -> ( N - S ) e. NN0 )
51 peano2nn0 
 |-  ( ( N - S ) e. NN0 -> ( ( N - S ) + 1 ) e. NN0 )
52 49 50 51 3syl 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) + 1 ) e. NN0 )
53 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
54 53 3ad2ant2 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> N e. NN0 )
55 25 anim1i 
 |-  ( ( N e. NN /\ S e. NN ) -> ( N e. RR /\ S e. NN ) )
56 55 ancoms 
 |-  ( ( S e. NN /\ N e. NN ) -> ( N e. RR /\ S e. NN ) )
57 crctcshwlkn0lem1 
 |-  ( ( N e. RR /\ S e. NN ) -> ( ( N - S ) + 1 ) <_ N )
58 56 57 syl 
 |-  ( ( S e. NN /\ N e. NN ) -> ( ( N - S ) + 1 ) <_ N )
59 58 3adant3 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) + 1 ) <_ N )
60 elfz2nn0 
 |-  ( ( ( N - S ) + 1 ) e. ( 0 ... N ) <-> ( ( ( N - S ) + 1 ) e. NN0 /\ N e. NN0 /\ ( ( N - S ) + 1 ) <_ N ) )
61 52 54 59 60 syl3anbrc 
 |-  ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) + 1 ) e. ( 0 ... N ) )
62 18 61 sylbi 
 |-  ( S e. ( 1 ..^ N ) -> ( ( N - S ) + 1 ) e. ( 0 ... N ) )
63 fzosplit 
 |-  ( ( ( N - S ) + 1 ) e. ( 0 ... N ) -> ( 0 ..^ N ) = ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) )
64 1 62 63 3syl 
 |-  ( ph -> ( 0 ..^ N ) = ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) )
65 64 raleqdv 
 |-  ( ph -> ( A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> A. j e. ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
66 47 65 mpbird 
 |-  ( ph -> A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )