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 imbitrrid 
 |-  ( ( # ` 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 ) ) ) ) )