Metamath Proof Explorer


Theorem clwlkclwwlklem2a

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

Ref Expression
Hypothesis clwlkclwwlklem2.f
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )
Assertion clwlkclwwlklem2a
|- ( ( E : dom E -1-1-> R /\ 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 ) ) -> ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f
 |-  F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )
2 simpl
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> x < ( ( # ` P ) - 2 ) )
3 f1f1orn
 |-  ( E : dom E -1-1-> R -> E : dom E -1-1-onto-> ran E )
4 3 3ad2ant1
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> E : dom E -1-1-onto-> ran E )
5 4 adantr
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) -> E : dom E -1-1-onto-> ran E )
6 5 ad2antrl
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> E : dom E -1-1-onto-> ran E )
7 elfzo0
 |-  ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) <-> ( x e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ x < ( ( # ` P ) - 1 ) ) )
8 lencl
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
9 simpl
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> x e. NN0 )
10 9 adantr
 |-  ( ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( x < ( ( # ` P ) - 2 ) /\ 2 <_ ( # ` P ) ) ) -> x e. NN0 )
11 elnn0z
 |-  ( x e. NN0 <-> ( x e. ZZ /\ 0 <_ x ) )
12 0red
 |-  ( ( x e. ZZ /\ ( # ` P ) e. NN0 ) -> 0 e. RR )
13 zre
 |-  ( x e. ZZ -> x e. RR )
14 13 adantr
 |-  ( ( x e. ZZ /\ ( # ` P ) e. NN0 ) -> x e. RR )
15 nn0re
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
16 2re
 |-  2 e. RR
17 16 a1i
 |-  ( ( # ` P ) e. NN0 -> 2 e. RR )
18 15 17 resubcld
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. RR )
19 18 adantl
 |-  ( ( x e. ZZ /\ ( # ` P ) e. NN0 ) -> ( ( # ` P ) - 2 ) e. RR )
20 lelttr
 |-  ( ( 0 e. RR /\ x e. RR /\ ( ( # ` P ) - 2 ) e. RR ) -> ( ( 0 <_ x /\ x < ( ( # ` P ) - 2 ) ) -> 0 < ( ( # ` P ) - 2 ) ) )
21 12 14 19 20 syl3anc
 |-  ( ( x e. ZZ /\ ( # ` P ) e. NN0 ) -> ( ( 0 <_ x /\ x < ( ( # ` P ) - 2 ) ) -> 0 < ( ( # ` P ) - 2 ) ) )
22 nn0z
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ )
23 2z
 |-  2 e. ZZ
24 23 a1i
 |-  ( ( # ` P ) e. NN0 -> 2 e. ZZ )
25 22 24 zsubcld
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. ZZ )
26 25 anim1i
 |-  ( ( ( # ` P ) e. NN0 /\ 0 < ( ( # ` P ) - 2 ) ) -> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 < ( ( # ` P ) - 2 ) ) )
27 elnnz
 |-  ( ( ( # ` P ) - 2 ) e. NN <-> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 < ( ( # ` P ) - 2 ) ) )
28 26 27 sylibr
 |-  ( ( ( # ` P ) e. NN0 /\ 0 < ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) - 2 ) e. NN )
29 nn0cn
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. CC )
30 peano2cnm
 |-  ( ( # ` P ) e. CC -> ( ( # ` P ) - 1 ) e. CC )
31 29 30 syl
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. CC )
32 31 subid1d
 |-  ( ( # ` P ) e. NN0 -> ( ( ( # ` P ) - 1 ) - 0 ) = ( ( # ` P ) - 1 ) )
33 32 oveq1d
 |-  ( ( # ` P ) e. NN0 -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( ( # ` P ) - 1 ) - 1 ) )
34 1cnd
 |-  ( ( # ` P ) e. NN0 -> 1 e. CC )
35 29 34 34 subsub4d
 |-  ( ( # ` P ) e. NN0 -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - ( 1 + 1 ) ) )
36 1p1e2
 |-  ( 1 + 1 ) = 2
37 36 a1i
 |-  ( ( # ` P ) e. NN0 -> ( 1 + 1 ) = 2 )
38 37 oveq2d
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - ( 1 + 1 ) ) = ( ( # ` P ) - 2 ) )
39 35 38 eqtrd
 |-  ( ( # ` P ) e. NN0 -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - 2 ) )
40 33 39 eqtrd
 |-  ( ( # ` P ) e. NN0 -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) = ( ( # ` P ) - 2 ) )
41 40 eleq1d
 |-  ( ( # ` P ) e. NN0 -> ( ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN <-> ( ( # ` P ) - 2 ) e. NN ) )
42 41 adantr
 |-  ( ( ( # ` P ) e. NN0 /\ 0 < ( ( # ` P ) - 2 ) ) -> ( ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN <-> ( ( # ` P ) - 2 ) e. NN ) )
43 28 42 mpbird
 |-  ( ( ( # ` P ) e. NN0 /\ 0 < ( ( # ` P ) - 2 ) ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN )
44 43 ex
 |-  ( ( # ` P ) e. NN0 -> ( 0 < ( ( # ` P ) - 2 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) )
45 44 adantl
 |-  ( ( x e. ZZ /\ ( # ` P ) e. NN0 ) -> ( 0 < ( ( # ` P ) - 2 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) )
46 21 45 syld
 |-  ( ( x e. ZZ /\ ( # ` P ) e. NN0 ) -> ( ( 0 <_ x /\ x < ( ( # ` P ) - 2 ) ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) )
47 46 exp4b
 |-  ( x e. ZZ -> ( ( # ` P ) e. NN0 -> ( 0 <_ x -> ( x < ( ( # ` P ) - 2 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) ) ) )
48 47 com23
 |-  ( x e. ZZ -> ( 0 <_ x -> ( ( # ` P ) e. NN0 -> ( x < ( ( # ` P ) - 2 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) ) ) )
49 48 imp
 |-  ( ( x e. ZZ /\ 0 <_ x ) -> ( ( # ` P ) e. NN0 -> ( x < ( ( # ` P ) - 2 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) ) )
50 11 49 sylbi
 |-  ( x e. NN0 -> ( ( # ` P ) e. NN0 -> ( x < ( ( # ` P ) - 2 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) ) )
51 50 imp
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) )
52 51 com12
 |-  ( x < ( ( # ` P ) - 2 ) -> ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) )
53 52 adantr
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ 2 <_ ( # ` P ) ) -> ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN ) )
54 53 impcom
 |-  ( ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( x < ( ( # ` P ) - 2 ) /\ 2 <_ ( # ` P ) ) ) -> ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN )
55 df-2
 |-  2 = ( 1 + 1 )
56 55 a1i
 |-  ( ( # ` P ) e. NN0 -> 2 = ( 1 + 1 ) )
57 56 oveq2d
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) = ( ( # ` P ) - ( 1 + 1 ) ) )
58 32 eqcomd
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) = ( ( ( # ` P ) - 1 ) - 0 ) )
59 58 oveq1d
 |-  ( ( # ` P ) e. NN0 -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) )
60 57 35 59 3eqtr2d
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) = ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) )
61 60 adantl
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( # ` P ) - 2 ) = ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) )
62 61 breq2d
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x < ( ( # ` P ) - 2 ) <-> x < ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) )
63 62 biimpcd
 |-  ( x < ( ( # ` P ) - 2 ) -> ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> x < ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) )
64 63 adantr
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ 2 <_ ( # ` P ) ) -> ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> x < ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) )
65 64 impcom
 |-  ( ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( x < ( ( # ` P ) - 2 ) /\ 2 <_ ( # ` P ) ) ) -> x < ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) )
66 elfzo0
 |-  ( x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) <-> ( x e. NN0 /\ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) e. NN /\ x < ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) )
67 10 54 65 66 syl3anbrc
 |-  ( ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) /\ ( x < ( ( # ` P ) - 2 ) /\ 2 <_ ( # ` P ) ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) )
68 67 exp32
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x < ( ( # ` P ) - 2 ) -> ( 2 <_ ( # ` P ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) )
69 68 a1d
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x < ( ( # ` P ) - 1 ) -> ( x < ( ( # ` P ) - 2 ) -> ( 2 <_ ( # ` P ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) )
70 69 com24
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( 2 <_ ( # ` P ) -> ( x < ( ( # ` P ) - 2 ) -> ( x < ( ( # ` P ) - 1 ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) )
71 70 ex
 |-  ( x e. NN0 -> ( ( # ` P ) e. NN0 -> ( 2 <_ ( # ` P ) -> ( x < ( ( # ` P ) - 2 ) -> ( x < ( ( # ` P ) - 1 ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) ) )
72 71 com25
 |-  ( x e. NN0 -> ( x < ( ( # ` P ) - 1 ) -> ( 2 <_ ( # ` P ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) ) )
73 72 imp
 |-  ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) -> ( 2 <_ ( # ` P ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) )
74 73 3adant2
 |-  ( ( x e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ x < ( ( # ` P ) - 1 ) ) -> ( 2 <_ ( # ` P ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) )
75 74 com14
 |-  ( ( # ` P ) e. NN0 -> ( 2 <_ ( # ` P ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( x e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ x < ( ( # ` P ) - 1 ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) )
76 8 75 syl
 |-  ( P e. Word V -> ( 2 <_ ( # ` P ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( x e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ x < ( ( # ` P ) - 1 ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) ) )
77 76 imp
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( x e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ x < ( ( # ` P ) - 1 ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) )
78 77 3adant1
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( x e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ x < ( ( # ` P ) - 1 ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) )
79 7 78 syl7bi
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( x < ( ( # ` P ) - 2 ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) )
80 79 com13
 |-  ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( x < ( ( # ` P ) - 2 ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) ) ) )
81 80 imp31
 |-  ( ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ x < ( ( # ` P ) - 2 ) ) /\ ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) ) -> x e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) )
82 fveq2
 |-  ( i = x -> ( P ` i ) = ( P ` x ) )
83 fvoveq1
 |-  ( i = x -> ( P ` ( i + 1 ) ) = ( P ` ( x + 1 ) ) )
84 82 83 preq12d
 |-  ( i = x -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = { ( P ` x ) , ( P ` ( x + 1 ) ) } )
85 84 eleq1d
 |-  ( i = x -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
86 85 adantl
 |-  ( ( ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ x < ( ( # ` P ) - 2 ) ) /\ ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) ) /\ i = x ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
87 81 86 rspcdv
 |-  ( ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ x < ( ( # ` P ) - 2 ) ) /\ ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) ) -> ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
88 87 ex
 |-  ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ x < ( ( # ` P ) - 2 ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) ) )
89 88 com13
 |-  ( A. i e. ( 0 ..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ x < ( ( # ` P ) - 2 ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) ) )
90 89 ad2antrl
 |-  ( ( ( 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 ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ x < ( ( # ` P ) - 2 ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) ) )
91 90 impcom
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) -> ( ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) /\ x < ( ( # ` P ) - 2 ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
92 91 expdimp
 |-  ( ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( x < ( ( # ` P ) - 2 ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) )
93 92 impcom
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E )
94 f1ocnvdm
 |-  ( ( E : dom E -1-1-onto-> ran E /\ { ( P ` x ) , ( P ` ( x + 1 ) ) } e. ran E ) -> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E )
95 6 93 94 syl2anc
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E )
96 2 95 jca
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E ) )
97 96 orcd
 |-  ( ( x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( ( x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E ) \/ ( -. x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. dom E ) ) )
98 simpl
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> -. x < ( ( # ` P ) - 2 ) )
99 5 ad2antrl
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> E : dom E -1-1-onto-> ran E )
100 nn0z
 |-  ( x e. NN0 -> x e. ZZ )
101 peano2zm
 |-  ( ( # ` P ) e. ZZ -> ( ( # ` P ) - 1 ) e. ZZ )
102 22 101 syl
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. ZZ )
103 100 102 anim12i
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x e. ZZ /\ ( ( # ` P ) - 1 ) e. ZZ ) )
104 zltlem1
 |-  ( ( x e. ZZ /\ ( ( # ` P ) - 1 ) e. ZZ ) -> ( x < ( ( # ` P ) - 1 ) <-> x <_ ( ( ( # ` P ) - 1 ) - 1 ) ) )
105 103 104 syl
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x < ( ( # ` P ) - 1 ) <-> x <_ ( ( ( # ` P ) - 1 ) - 1 ) ) )
106 39 adantl
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( ( # ` P ) - 1 ) - 1 ) = ( ( # ` P ) - 2 ) )
107 106 breq2d
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x <_ ( ( ( # ` P ) - 1 ) - 1 ) <-> x <_ ( ( # ` P ) - 2 ) ) )
108 107 biimpd
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x <_ ( ( ( # ` P ) - 1 ) - 1 ) -> x <_ ( ( # ` P ) - 2 ) ) )
109 105 108 sylbid
 |-  ( ( x e. NN0 /\ ( # ` P ) e. NN0 ) -> ( x < ( ( # ` P ) - 1 ) -> x <_ ( ( # ` P ) - 2 ) ) )
110 109 impancom
 |-  ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> x <_ ( ( # ` P ) - 2 ) ) )
111 110 imp
 |-  ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) -> x <_ ( ( # ` P ) - 2 ) )
112 nn0re
 |-  ( x e. NN0 -> x e. RR )
113 112 adantr
 |-  ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) -> x e. RR )
114 113 18 anim12i
 |-  ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) -> ( x e. RR /\ ( ( # ` P ) - 2 ) e. RR ) )
115 lenlt
 |-  ( ( x e. RR /\ ( ( # ` P ) - 2 ) e. RR ) -> ( x <_ ( ( # ` P ) - 2 ) <-> -. ( ( # ` P ) - 2 ) < x ) )
116 114 115 syl
 |-  ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) -> ( x <_ ( ( # ` P ) - 2 ) <-> -. ( ( # ` P ) - 2 ) < x ) )
117 111 116 mpbid
 |-  ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) -> -. ( ( # ` P ) - 2 ) < x )
118 117 anim1i
 |-  ( ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) /\ -. x < ( ( # ` P ) - 2 ) ) -> ( -. ( ( # ` P ) - 2 ) < x /\ -. x < ( ( # ` P ) - 2 ) ) )
119 114 ancomd
 |-  ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) -> ( ( ( # ` P ) - 2 ) e. RR /\ x e. RR ) )
120 119 adantr
 |-  ( ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) /\ -. x < ( ( # ` P ) - 2 ) ) -> ( ( ( # ` P ) - 2 ) e. RR /\ x e. RR ) )
121 lttri3
 |-  ( ( ( ( # ` P ) - 2 ) e. RR /\ x e. RR ) -> ( ( ( # ` P ) - 2 ) = x <-> ( -. ( ( # ` P ) - 2 ) < x /\ -. x < ( ( # ` P ) - 2 ) ) ) )
122 120 121 syl
 |-  ( ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) /\ -. x < ( ( # ` P ) - 2 ) ) -> ( ( ( # ` P ) - 2 ) = x <-> ( -. ( ( # ` P ) - 2 ) < x /\ -. x < ( ( # ` P ) - 2 ) ) ) )
123 118 122 mpbird
 |-  ( ( ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) /\ ( # ` P ) e. NN0 ) /\ -. x < ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) - 2 ) = x )
124 123 exp31
 |-  ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> ( -. x < ( ( # ` P ) - 2 ) -> ( ( # ` P ) - 2 ) = x ) ) )
125 124 com23
 |-  ( ( x e. NN0 /\ x < ( ( # ` P ) - 1 ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) = x ) ) )
126 125 3adant2
 |-  ( ( x e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ x < ( ( # ` P ) - 1 ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) = x ) ) )
127 7 126 sylbi
 |-  ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) = x ) ) )
128 127 impcom
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) = x ) )
129 8 128 syl5com
 |-  ( P e. Word V -> ( ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( # ` P ) - 2 ) = x ) )
130 129 3ad2ant2
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( # ` P ) - 2 ) = x ) )
131 130 imp
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( ( # ` P ) - 2 ) = x )
132 131 fveq2d
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( P ` ( ( # ` P ) - 2 ) ) = ( P ` x ) )
133 132 preq1d
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } = { ( P ` x ) , ( P ` 0 ) } )
134 133 eleq1d
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E <-> { ( P ` x ) , ( P ` 0 ) } e. ran E ) )
135 134 biimpd
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( -. x < ( ( # ` P ) - 2 ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) )
136 135 exp32
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) ) ) )
137 136 com12
 |-  ( -. x < ( ( # ` P ) - 2 ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) ) ) )
138 137 com14
 |-  ( { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) ) ) )
139 138 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 ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) ) ) )
140 139 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 ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) ) ) )
141 140 com12
 |-  ( ( E : dom E -1-1-> R /\ 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 ) ) -> ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) ) ) )
142 141 imp31
 |-  ( ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( -. x < ( ( # ` P ) - 2 ) -> { ( P ` x ) , ( P ` 0 ) } e. ran E ) )
143 142 impcom
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> { ( P ` x ) , ( P ` 0 ) } e. ran E )
144 f1ocnvdm
 |-  ( ( E : dom E -1-1-onto-> ran E /\ { ( P ` x ) , ( P ` 0 ) } e. ran E ) -> ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. dom E )
145 99 143 144 syl2anc
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. dom E )
146 98 145 jca
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( -. x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. dom E ) )
147 146 olcd
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) ) -> ( ( x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E ) \/ ( -. x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. dom E ) ) )
148 97 147 pm2.61ian
 |-  ( ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( ( x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E ) \/ ( -. x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. dom E ) ) )
149 ifel
 |-  ( if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) e. dom E <-> ( ( x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. dom E ) \/ ( -. x < ( ( # ` P ) - 2 ) /\ ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. dom E ) ) )
150 148 149 sylibr
 |-  ( ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) /\ x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) e. dom E )
151 150 1 fmptd
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) -> F : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom E )
152 iswrdi
 |-  ( F : ( 0 ..^ ( ( # ` P ) - 1 ) ) --> dom E -> F e. Word dom E )
153 151 152 syl
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) -> F e. Word dom E )
154 wrdf
 |-  ( P e. Word V -> P : ( 0 ..^ ( # ` P ) ) --> V )
155 154 adantr
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> P : ( 0 ..^ ( # ` P ) ) --> V )
156 1 clwlkclwwlklem2a2
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
157 fzoval
 |-  ( ( # ` P ) e. ZZ -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) )
158 8 22 157 3syl
 |-  ( P e. Word V -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( ( # ` P ) - 1 ) ) )
159 oveq2
 |-  ( ( ( # ` P ) - 1 ) = ( # ` F ) -> ( 0 ... ( ( # ` P ) - 1 ) ) = ( 0 ... ( # ` F ) ) )
160 159 eqcoms
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( 0 ... ( ( # ` P ) - 1 ) ) = ( 0 ... ( # ` F ) ) )
161 158 160 sylan9eq
 |-  ( ( P e. Word V /\ ( # ` F ) = ( ( # ` P ) - 1 ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( # ` F ) ) )
162 156 161 syldan
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( 0 ..^ ( # ` P ) ) = ( 0 ... ( # ` F ) ) )
163 162 feq2d
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P : ( 0 ..^ ( # ` P ) ) --> V <-> P : ( 0 ... ( # ` F ) ) --> V ) )
164 155 163 mpbid
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
165 164 3adant1
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
166 165 adantr
 |-  ( ( ( E : dom E -1-1-> R /\ 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 : ( 0 ... ( # ` F ) ) --> V )
167 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 ) )
168 167 3adant1
 |-  ( ( E : dom E -1-1-> R /\ 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 ) )
169 168 imp
 |-  ( ( ( E : dom E -1-1-> R /\ 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 )
170 156 3adant1
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
171 170 adantr
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
172 1 clwlkclwwlklem2a4
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
173 172 impl
 |-  ( ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) /\ i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
174 173 ralimdva
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
175 oveq2
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ ( ( # ` P ) - 1 ) ) )
176 175 raleqdv
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } <-> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
177 176 imbi2d
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) <-> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
178 174 177 syl5ibr
 |-  ( ( # ` F ) = ( ( # ` P ) - 1 ) -> ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) )
179 171 178 mpcom
 |-  ( ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) /\ ( lastS ` P ) = ( P ` 0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
180 179 adantrr
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
181 169 180 mpd
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } )
182 153 166 181 3jca
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) -> ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) )
183 1 clwlkclwwlklem2a3
 |-  ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` ( # ` F ) ) = ( lastS ` P ) )
184 183 3adant1
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` ( # ` F ) ) = ( lastS ` P ) )
185 184 eqcomd
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( lastS ` P ) = ( P ` ( # ` F ) ) )
186 185 eqeq2d
 |-  ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( P ` 0 ) = ( lastS ` P ) <-> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
187 186 biimpcd
 |-  ( ( P ` 0 ) = ( lastS ` P ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
188 187 eqcoms
 |-  ( ( lastS ` P ) = ( P ` 0 ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
189 188 adantr
 |-  ( ( ( 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 ) ) -> ( ( E : dom E -1-1-> R /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
190 189 impcom
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ` 0 ) = ( P ` ( # ` F ) ) )
191 182 190 jca
 |-  ( ( ( E : dom E -1-1-> R /\ 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 ) ) ) -> ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
192 191 ex
 |-  ( ( E : dom E -1-1-> R /\ 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 ) ) -> ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )