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 74 raleqdv
 |-  ( ( ( 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 <-> A. i e. ( ( 0 ..^ ( ( # ` P ) - 2 ) ) u. { ( ( # ` P ) - 2 ) } ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
76 48 75 mpbird
 |-  ( ( ( 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 )
77 76 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 ) )