Metamath Proof Explorer

Theorem clwlkclwwlklem2a1

Description: Lemma 1 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem2a1 
|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
2 nn0cn 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. CC )
3 peano2cnm 
 |-  ( ( # ` P ) e. CC -> ( ( # ` P ) - 1 ) e. CC )
4 3 subid1d 
 |-  ( ( # ` P ) e. CC -> ( ( ( # ` P ) - 1 ) - 0 ) = ( ( # ` P ) - 1 ) )
5 4 oveq1d 
 |-  ( ( # ` P ) e. CC -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( ( # ` P ) - 1 ) - 1 ) )
6 sub1m1 
 |-  ( ( # ` P ) e. CC -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - 2 ) )
7 5 6 eqtrd 
 |-  ( ( # ` P ) e. CC -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( # ` P ) - 2 ) )
8 1 2 7 3syl 
 |-  ( P e. Word V -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( # ` P ) - 2 ) )
9 8 adantr 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( # ` P ) - 2 ) )
10 9 oveq2d 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) = ( 0 ..^ ( ( # ` P ) - 2 ) ) )
11 10 raleqdv 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> A. i e. ( 0 ..^ ( ( # ` P ) - 2 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
12 11 biimpcd 
 |-  ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 2 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
13 12 adantr 
 |-  ( ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) -> ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 2 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
14 13 adantl 
 |-  ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 2 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
15 14 impcom 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 2 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E )
16 lsw 
 |-  ( P e. Word V -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
17 2m1e1 
 |-  ( 2 - 1 ) = 1
18 17 a1i 
 |-  ( P e. Word V -> ( 2 - 1 ) = 1 )
19 18 eqcomd 
 |-  ( P e. Word V -> 1 = ( 2 - 1 ) )
20 19 oveq2d 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) = ( ( # ` P ) - ( 2 - 1 ) ) )
21 1 2 syl 
 |-  ( P e. Word V -> ( # ` P ) e. CC )
22 2cnd 
 |-  ( P e. Word V -> 2 e. CC )
23 1cnd 
 |-  ( P e. Word V -> 1 e. CC )
24 21 22 23 subsubd 
 |-  ( P e. Word V -> ( ( # ` P ) - ( 2 - 1 ) ) = ( ( ( # ` P ) - 2 ) + 1 ) )
25 20 24 eqtrd 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) = ( ( ( # ` P ) - 2 ) + 1 ) )
26 25 fveq2d 
 |-  ( P e. Word V -> ( P ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
27 16 26 eqtrd 
 |-  ( P e. Word V -> ( lastS ` P ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
28 27 adantr 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( lastS ` P ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
29 28 adantr 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( lastS ` P ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
30 eqeq1 
 |-  ( ( lastS ` P ) = ( P ` 0 ) -> ( ( lastS ` P ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) <-> ( P ` 0 ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) ) )
31 30 adantl 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( ( lastS ` P ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) <-> ( P ` 0 ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) ) )
32 29 31 mpbid 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( P ` 0 ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
33 32 preq2d 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } )
34 33 eleq1d 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) )
35 34 biimpd 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) )
36 35 ex 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( lastS ` P ) = ( P ` 0 ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) ) )
37 36 com13 
 |-  ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E -> ( ( lastS ` P ) = ( P ` 0 ) -> ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) ) )
38 37 adantl 
 |-  ( ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) -> ( ( lastS ` P ) = ( P ` 0 ) -> ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) ) )
39 38 impcom 
 |-  ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) )
40 39 impcom 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E )
41 ovexd 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) -> ( ( # ` P ) - 2 ) e. _V )
42 fveq2 
 |-  ( i = ( ( # ` P ) - 2 ) -> ( P ` i ) = ( P ` ( ( # ` P ) - 2 ) ) )
43 fvoveq1 
 |-  ( i = ( ( # ` P ) - 2 ) -> ( P ` ( i + 1 ) ) = ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) )
44 42 43 preq12d 
 |-  ( i = ( ( # ` P ) - 2 ) -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } )
45 44 eleq1d 
 |-  ( i = ( ( # ` P ) - 2 ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) )
46 45 ralunsn 
 |-  ( ( ( # ` P ) - 2 ) e. _V -> ( A. i e. ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> ( A. i e. ( 0 ..^ ( ( # ` P ) - 2 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) ) )
47 41 46 syl 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) -> ( A. i e. ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> ( A. i e. ( 0 ..^ ( ( # ` P ) - 2 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` ( ( ( # ` P ) - 2 ) + 1 ) ) } e. ran E ) ) )
48 15 40 47 mpbir2and 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) -> A. i e. ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E )
49 1e2m1 
 |-  1 = ( 2 - 1 )
50 49 a1i 
 |-  ( P e. Word V -> 1 = ( 2 - 1 ) )
51 50 oveq2d 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) = ( ( # ` P ) - ( 2 - 1 ) ) )
52 51 24 eqtrd 
 |-  ( P e. Word V -> ( ( # ` P ) - 1 ) = ( ( ( # ` P ) - 2 ) + 1 ) )
53 52 oveq2d 
 |-  ( P e. Word V -> ( 0 ..^ ( ( # ` P ) - 1 ) ) = ( 0 ..^ ( ( ( # ` P ) - 2 ) + 1 ) ) )
54 53 adantr 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( 0 ..^ ( ( # ` P ) - 1 ) ) = ( 0 ..^ ( ( ( # ` P ) - 2 ) + 1 ) ) )
55 nn0re 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
56 2re 
 |-  2 e. RR
57 56 a1i 
 |-  ( ( # ` P ) e. NN0 -> 2 e. RR )
58 55 57 subge0d 
 |-  ( ( # ` P ) e. NN0 -> ( 0 <_ ( ( # ` P ) - 2 ) <-> 2 <_ ( # ` P ) ) )
59 58 biimprd 
 |-  ( ( # ` P ) e. NN0 -> ( 2 <_ ( # ` P ) -> 0 <_ ( ( # ` P ) - 2 ) ) )
60 nn0z 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ )
61 2z 
 |-  2 e. ZZ
62 61 a1i 
 |-  ( ( # ` P ) e. NN0 -> 2 e. ZZ )
63 60 62 zsubcld 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. ZZ )
64 59 63 jctild 
 |-  ( ( # ` P ) e. NN0 -> ( 2 <_ ( # ` P ) -> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 <_ ( ( # ` P ) - 2 ) ) ) )
65 1 64 syl 
 |-  ( P e. Word V -> ( 2 <_ ( # ` P ) -> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 <_ ( ( # ` P ) - 2 ) ) ) )
66 65 imp 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 <_ ( ( # ` P ) - 2 ) ) )
67 elnn0z 
 |-  ( ( ( # ` P ) - 2 ) e. NN0 <-> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 <_ ( ( # ` P ) - 2 ) ) )
68 66 67 sylibr 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. NN0 )
69 elnn0uz 
 |-  ( ( ( # ` P ) - 2 ) e. NN0 <-> ( ( # ` P ) - 2 ) e. ( ZZ>= ` 0 ) )
70 68 69 sylib 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. ( ZZ>= ` 0 ) )
71 fzosplitsn 
 |-  ( ( ( # ` P ) - 2 ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( ( # ` P ) - 2 ) + 1 ) ) = ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) )
72 70 71 syl 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( 0 ..^ ( ( ( # ` P ) - 2 ) + 1 ) ) = ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) )
73 54 72 eqtrd 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( 0 ..^ ( ( # ` P ) - 1 ) ) = ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) )
74 73 adantr 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) -> ( 0 ..^ ( ( # ` P ) - 1 ) ) = ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) )
75 48 74 raleqtrrdv 
 |-  ( ( ( P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E )
76 75 ex 
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )